とりあえず書いてみたところまで(結局endまで出来てない)

End.hs

{-# LANGUAGE GADTs, RankNTypes, MultiParamTypeClasses, FlexibleInstances #-}

module End where

import qualified Prelude
import Control.Category
import Data.Monoid
import Data.Functor.Identity

type Hask = (->)

data Arrow c a b where
  Arrow :: (Category cat) => cat a b -> Arrow cat a b

class Subdivision sub where
  sdom :: (Category cat) => cat a b -> sub (Arrow cat a a) (Arrow cat a b)
  scod :: (Category cat) => cat a b -> sub (Arrow cat b b) (Arrow cat a b)

instance Subdivision Hask where 
  sdom f (Arrow g) = Arrow (f . g)
  scod f (Arrow g) = Arrow (g . f)
  
class (Category cat) => Subdivision' cat sub where
  sdom' :: cat a b -> sub (Arrow cat a a) (Arrow cat a b)
  scod' :: cat a b -> sub (Arrow cat b b) (Arrow cat a b)
  
instance (Category cat) => Subdivision' cat Hask where
  sdom' f (Arrow g) = Arrow (f . g)
  scod' f (Arrow g) = Arrow (g . f)

class (Category c, Category d) => Functor f c d where
  fmap :: c a b -> d (f a) (f b)
  
instance (Prelude.Functor f) => Functor f Hask Hask where
--fmap :: (a -> b) -> f a -> f b
  fmap = Prelude.fmap

class (Category c, Category c', Category d) => Bifunctor f c c' d where
  bimap :: c a b -> c' a' b' -> d (f a b) (f a' b')
  
data Hom c c' x where
  Hom :: (Category c, Category c', Category x) => c a b -> c' a b -> Hom c c' x

main = Prelude.undefined

• S :: C x C^op -> X のendを integral c (S c c) みたいな感じで実装したい(cの任意性が型へのforallとして効いてくる(？)).
• integral c (* c c) はMonoid
• endの自然な同型がYoneda lemmaそのもの
• \int_c S(c,c) ~= Lim S^$ (S^$ :: C^$ -> X)