open import Level open import Category module Comma1 {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {C : Category c₁' c₂' ℓ'} ( F : Functor A C ) ( G : Functor A C ) where open import HomReasoning open import cat-utility -- -- F G -- A -> C <- A -- open Functor record CommaObj : Set ( c₁ ⊔ c₂' ) where field obj : Obj A hom : Hom C ( FObj F obj ) ( FObj G obj ) open CommaObj record CommaHom ( a b : CommaObj ) : Set ( c₂ ⊔ ℓ' ) where field arrow : Hom A ( obj a ) ( obj b ) comm : C [ C [ FMap G arrow o hom a ] ≈ C [ hom b o FMap F arrow ] ] open CommaHom _∙_ : {a b c : CommaObj } → CommaHom b c → CommaHom a b → CommaHom a c _∙_ {a} {b} {c} f g = record { arrow = A [ arrow f o arrow g ] ; comm = comm1 } where comm1 : C [ C [ FMap G (A [ arrow f o arrow g ] ) o hom a ] ≈ C [ hom c o FMap F (A [ arrow f o arrow g ]) ] ] comm1 = let open ≈-Reasoning C in begin FMap G (A [ arrow f o arrow g ] ) o hom a ≈⟨ car ( distr G ) ⟩ ( FMap G (arrow f) o FMap G (arrow g )) o hom a ≈↑⟨ assoc ⟩ FMap G (arrow f) o ( FMap G (arrow g ) o hom a ) ≈⟨ cdr ( comm g ) ⟩ FMap G (arrow f) o ( hom b o FMap F (arrow g ) ) ≈⟨ assoc ⟩ ( FMap G (arrow f) o hom b) o FMap F (arrow g ) ≈⟨ car ( comm f ) ⟩ ( hom c o FMap F (arrow f) ) o FMap F (arrow g ) ≈↑⟨ assoc ⟩ hom c o ( FMap F (arrow f) o FMap F (arrow g ) ) ≈↑⟨ cdr ( distr F) ⟩ hom c o FMap F (A [ arrow f o arrow g ]) ∎ CommaId : { a : CommaObj } → CommaHom a a CommaId {a} = record { arrow = id1 A ( obj a ) ; comm = comm2 } where comm2 : C [ C [ FMap G (id1 A (obj a)) o hom a ] ≈ C [ hom a o FMap F (id1 A (obj a)) ] ] comm2 = let open ≈-Reasoning C in begin FMap G (id1 A (obj a)) o hom a ≈⟨ car ( IsFunctor.identity ( isFunctor G ) ) ⟩ id1 C (FObj G (obj a)) o hom a ≈⟨ idL ⟩ hom a ≈↑⟨ idR ⟩ hom a o id1 C (FObj F (obj a)) ≈↑⟨ cdr ( IsFunctor.identity ( isFunctor F ) )⟩ hom a o FMap F (id1 A (obj a)) ∎ _⋍_ : { a b : CommaObj } ( f g : CommaHom a b ) → Set ℓ f ⋍ g = A [ arrow f ≈ arrow g ] isCommaCategory : IsCategory CommaObj CommaHom _⋍_ _∙_ CommaId isCommaCategory = record { isEquivalence = record { refl = let open ≈-Reasoning (A) in refl-hom ; sym = let open ≈-Reasoning (A) in sym ; trans = let open ≈-Reasoning (A) in trans-hom } ; identityL = let open ≈-Reasoning (A) in idL ; identityR = let open ≈-Reasoning (A) in idR ; o-resp-≈ = IsCategory.o-resp-≈ ( Category.isCategory A ) ; associative = IsCategory.associative ( Category.isCategory A ) } CommaCategory : Category (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ CommaCategory = record { Obj = CommaObj ; Hom = CommaHom ; _o_ = _∙_ ; _≈_ = _⋍_ ; Id = CommaId ; isCategory = isCommaCategory } open NTrans nat-lemma : NTrans A C F G → Functor A CommaCategory nat-lemma n = record { FObj = λ x → fobj x ; FMap = λ {a} {b} f → fmap {a} {b} f ; isFunctor = record { identity = λ{x} → identity x ; distr = λ {a} {b} {c} {f} {g} → distr1 {a} {b} {c} {f} {g} ; ≈-cong = λ {a} {b} {c} {f} → ≈-cong {a} {b} {c} {f} } } where fobj : Obj A → Obj CommaCategory fobj x = record { obj = x ; hom = TMap n x } fmap : {a b : Obj A } → Hom A a b → Hom CommaCategory (fobj a) (fobj b ) fmap f = record { arrow = f ; comm = IsNTrans.commute (isNTrans n ) } ≈-cong : {a : Obj A} {b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → CommaCategory [ fmap f ≈ fmap g ] ≈-cong {a} {b} {f} {g} f=g = f=g identity : (x : Obj A ) -> CommaCategory [ fmap (id1 A x) ≈ id1 CommaCategory (fobj x) ] identity x = let open ≈-Reasoning (A) in begin arrow (fmap (id1 A x)) ≈⟨⟩ id1 A x ≈⟨⟩ arrow (id1 CommaCategory (fobj x)) ∎ distr1 : {a : Obj A} {b : Obj A} {c : Obj A} {f : Hom A a b} {g : Hom A b c} → CommaCategory [ fmap (A [ g o f ]) ≈ CommaCategory [ fmap g o fmap f ] ] distr1 = let open ≈-Reasoning (A) in refl-hom nat-f : Functor A C → Functor A CommaCategory → Functor A C nat-f F N = record { FObj = λ x → FObj F ( obj ( FObj N x )) ; FMap = λ {a} {b} f → FMap F (arrow (FMap N f)) ; isFunctor = record { identity = λ{x} → identity x ; distr = λ {a} {b} {c} {f} {g} → distr1 {a} {b} {c} {f} {g} ; ≈-cong = λ {a} {b} {f} {g} → ≈-cong {a} {b} {f} {g} } } where identity : (x : Obj A ) -> C [ FMap F (arrow (FMap N (id1 A x))) ≈ id1 C (FObj F (obj (FObj N x))) ] identity x = let open ≈-Reasoning (C) in begin FMap F (arrow (FMap N (id1 A x))) ≈⟨ fcong F ( IsFunctor.identity ( isFunctor N) ) ⟩ FMap F (id1 A (obj (FObj N x))) ≈⟨ IsFunctor.identity ( isFunctor F ) ⟩ id1 C (FObj F (obj (FObj N x))) ∎ distr1 : {a : Obj A} {b : Obj A} {c : Obj A} {f : Hom A a b} {g : Hom A b c} → C [ FMap F (arrow (FMap N (A [ g o f ]))) ≈ C [ FMap F (arrow (FMap N g)) o FMap F (arrow (FMap N f)) ] ] distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (C) in begin FMap F (arrow (FMap N (A [ g o f ]))) ≈⟨ fcong F ( IsFunctor.distr ( isFunctor N) ) ⟩ FMap F (A [ arrow (FMap N g ) o arrow (FMap N f ) ] ) ≈⟨ ( IsFunctor.distr ( isFunctor F ) ) ⟩ FMap F (arrow (FMap N g)) o FMap F (arrow (FMap N f)) ∎ ≈-cong : {a : Obj A} {b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → C [ FMap F (arrow (FMap N f)) ≈ FMap F (arrow (FMap N g)) ] ≈-cong {a} {b} {f} {g} f=g = let open ≈-Reasoning (C) in begin FMap F (arrow (FMap N f)) ≈⟨ fcong F (( IsFunctor.≈-cong ( isFunctor N) ) f=g ) ⟩ FMap F (arrow (FMap N g)) ∎ nat-lemma← : ( N : Functor A CommaCategory ) → NTrans A C (nat-f F N) (nat-f G N) nat-lemma← N = record { TMap = λ (a : Obj A ) → tmap1 a ; isNTrans = record { commute = λ {a} {b} {f} → commute2 {a} {b} {f} } } where tmap1 : (a : Obj A ) → Hom C (FObj F (obj ( FObj N a))) (FObj G (obj ( FObj N a))) tmap1 a = hom (FObj N a) commute2 : {a b : Obj A } {f : Hom A a b } → C [ C [ FMap G ( arrow ( FMap N f)) o tmap1 a ] ≈ C [ tmap1 b o FMap F ( arrow ( FMap N f )) ] ] commute2 {a} {b} {f} = comm ( FMap N f )