
  0 | module Data.Category.NaturalTransformation
  1 | 
  2 | import public Data.Category.Functor
  3 | 
  4 | %unbound_implicits off
  5 | 
  6 | public export
  7 | record (==>>) {0 cObj, dObj : Type} {0 c : Category cObj} {0 d : Category dObj}
  8 |               (f, g : Functor c d) where
  9 |   constructor MkNT
 10 |   comp : (v : cObj) -> (f.F v) ~> (g.F v)
 11 | 
 12 |   --                η x
 13 |   --   x      F x ───────> G x
 14 |   --   │       │             │
 15 |   --  m│   F m │             │ G m
 16 |   --   │       │             │
 17 |   --   v       v             v
 18 |   --   y      F y ───────> G y
 19 |   --                η y
 20 |   0 commutes : (0 x, y : cObj) -> (m : x ~> y) ->
 21 |       let 0 top : f.F x ~> g.F x
 22 |           top = comp x
 23 | 
 24 |           0 bot : f.F y ~> g.F y
 25 |           bot = comp y
 26 | 
 27 |           0 left : f.F x ~> f.F y
 28 |           left = f.F' _ _ m
 29 | 
 30 |           0 right : g.F x ~> g.F y
 31 |           right = g.F' _ _ m
 32 | 
 33 |           0 comp1 : f.F x ~> g.F y
 34 |           comp1 = top |> right
 35 | 
 36 |           0 comp2 : f.F x ~> g.F y
 37 |           comp2 = left |> bot
 38 | 
 39 |       in comp1 === comp2
 40 | 
 41 |