8
open Functor using (Functor)
12
open Functor.Projections using (Map; map)
14
data _⊢_ {ℂ ⅅ : Cat}(F : Functor ℂ ⅅ)(G : Functor ⅅ ℂ) : Set1 where
16
(_* : {X : Obj ℂ}{Y : Obj ⅅ} -> Map F X ─→ Y -> X ─→ Map G Y)
17
(_# : {X : Obj ℂ}{Y : Obj ⅅ} -> X ─→ Map G Y -> Map F X ─→ Y)
18
(inv₁ : {X : Obj ℂ}{Y : Obj ⅅ}(g : X ─→ Map G Y) -> g # * == g)
19
(inv₂ : {X : Obj ℂ}{Y : Obj ⅅ}(f : Map F X ─→ Y) -> f * # == f)
20
(nat₁ : {X₁ X₂ : Obj ℂ}{Y₁ Y₂ : Obj ⅅ}
21
(f : Y₁ ─→ Y₂)(g : X₂ ─→ X₁)(h : Map F X₁ ─→ Y₁) ->
22
(f ∘ h ∘ map F g) * == map G f ∘ (h *) ∘ g
24
(nat₂ : {X₁ X₂ : Obj ℂ}{Y₁ Y₂ : Obj ⅅ}
25
(f : Y₁ ─→ Y₂)(g : X₂ ─→ X₁)(h : X₁ ─→ Map G Y₁) ->
26
(map G f ∘ h ∘ g) # == f ∘ (h #) ∘ map F g