
  0 | module Data.Category.Functor
  1 | 
  2 | import public Data.Category
  3 | 
  4 | %hide Prelude.Functor
  5 | 
  6 | %unbound_implicits off
  7 | 
  8 | public export
  9 | record Functor {0 o1, o2 : Type} (cat1 : Category o1) (cat2 : Category o2) where
 10 |   constructor MkFunctor
 11 | 
 12 |   -- a way to map objects
 13 |   F : o1 -> o2
 14 | 
 15 |   -- a way to map morphisms
 16 |   -- For each morphism in cat1 between objects a and b
 17 |   -- we get a morphism in cat2 between the corresponding objects a and b
 18 |   -- but mapped to their counterparts in cat2
 19 |   F' : (0 a, b : o1) -> a ~> b -> F a ~> F b
 20 | 
 21 |   -- mapping the identity morphism in cat1 results in the identity morphism in cat2
 22 |   0 presId : (v : o1) -> F' v v (id cat1 v) = id cat2 (F v)
 23 | 
 24 |   -- composition of hom-sets
 25 |   0 presComp : (a, b, c : o1) ->
 26 |                (f : a ~> b) ->
 27 |                (g : b ~> c) ->
 28 |                F' a c ((|:>) cat1 {a, b, c} f g)
 29 |              = ((|:>) cat2) {a=F a, b=F b, c=F c} (F' a b f) (F' b c g)
 30 | 
 31 | -- composition of functors
 32 | public export
 33 | (*>) : {0 o1, o2, o3 : Type} -> {0 a : Category o1} -> {0 b : Category o2} -> {0 c : Category o3} ->
 34 |       Functor a b -> Functor b c -> Functor a c
 35 | (*>) f1 f2 = MkFunctor
 36 |   (f2.F . f1.F)
 37 |   (\a, b, m => f2.F' (f1.F a) (f1.F b) (f1.F' a b m))
 38 |   (\x => cong (f2.F' (f1.F x) (f1.F x)) (f1.presId x) `trans` f2.presId (f1.F x))
 39 |   (\a, b, c, h, j => cong (f2.F' (f1.F _) (f1.F _)) (f1.presComp _ _ _ h j) `trans`
 40 |                           f2.presComp _ _ _ (f1.F' _ _ h) (f1.F' _ _ j))
 41 | 
 42 | public export
 43 | idF : {0 o : Type} -> (0 c : Category o) -> Functor c c
 44 | idF c = MkFunctor id (\_, _ => id) (\_ => Refl) (\_, _, _, _, _ => Refl)
 45 | 
 46 |