# HG changeset patch # User Shinji KONO # Date 1489036563 -32400 # Node ID a5034bdf6f38b22938690bd5f6934aef415110a1 # Parent dc24ac6ebdb3c138097da33863a73d55e5480a68 Comma Category with A B C diff -r dc24ac6ebdb3 -r a5034bdf6f38 Comma.agda --- a/Comma.agda Thu Mar 09 09:03:07 2017 +0900 +++ b/Comma.agda Thu Mar 09 14:16:03 2017 +0900 @@ -1,6 +1,7 @@ open import Level open import Category -module Comma {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁ c₂ ℓ} {C : Category c₁' c₂' ℓ'} ( F G : Functor A C ) where +module Comma {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁ c₂ ℓ} {C : Category c₁' c₂' ℓ'} + ( F : Functor A C ) ( G : Functor B C ) where open import HomReasoning open import cat-utility @@ -9,43 +10,48 @@ -- F G -- A -> C <- B -- --- this a special case A = B open Functor record CommaObj : Set ( c₁ ⊔ c₂' ) where field obj : Obj A - hom : Hom C ( FObj F obj ) ( FObj G obj ) + objb : Obj B + hom : Hom C ( FObj F obj ) ( FObj G objb ) 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 ] ] + arrowg : Hom B ( objb a ) ( objb b ) + comm : C [ C [ FMap G arrowg o hom a ] ≈ C [ hom b o FMap F arrow ] ] open CommaHom -_⋍_ : { a b : CommaObj } ( f g : CommaHom a b ) → Set ℓ -_⋍_ f g = A [ arrow f ≈ arrow g ] +record _⋍_ { a b : CommaObj } ( f g : CommaHom a b ) : Set ℓ where + field + eqa : A [ arrow f ≈ arrow g ] + eqb : B [ arrowg f ≈ arrowg g ] + +open _⋍_ _∙_ : {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 : C [ C [ FMap G (B [ arrowg f o arrowg 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 + FMap G (B [ arrowg f o arrowg g ] ) o hom a ≈⟨ car ( distr G ) ⟩ - ( FMap G (arrow f) o FMap G (arrow g )) o hom a + ( FMap G (arrowg f) o FMap G (arrowg g )) o hom a ≈↑⟨ assoc ⟩ - FMap G (arrow f) o ( FMap G (arrow g ) o hom a ) + FMap G (arrowg f) o ( FMap G (arrowg g ) o hom a ) ≈⟨ cdr ( comm g ) ⟩ - FMap G (arrow f) o ( hom b o FMap F (arrow g ) ) + FMap G (arrowg f) o ( hom b o FMap F (arrow g ) ) ≈⟨ assoc ⟩ - ( FMap G (arrow f) o hom b) o FMap F (arrow g ) + ( FMap G (arrowg 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 ⟩ @@ -57,11 +63,11 @@ 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 : C [ C [ FMap G (id1 B (objb 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 + FMap G (id1 B (objb a)) o hom a ≈⟨ car ( IsFunctor.identity ( isFunctor G ) ) ⟩ - id1 C (FObj G (obj a)) o hom a + id1 C (FObj G (objb a)) o hom a ≈⟨ idL ⟩ hom a ≈↑⟨ idR ⟩ @@ -72,24 +78,29 @@ isCommaCategory : IsCategory CommaObj CommaHom _⋍_ _∙_ CommaId isCommaCategory = record { - isEquivalence = let open ≈-Reasoning (A) in record {refl = refl-hom ; - sym = sym ; - trans = trans-hom } - ; identityL = λ{a b f} → identityL {a} {b} {f} - ; identityR = λ{a b f} → let open ≈-Reasoning A in idR - ; o-resp-≈ = IsCategory.o-resp-≈ ( Category.isCategory A ) - ; associative = IsCategory.associative (Category.isCategory A) - } where - identityL : {a : CommaObj} {b : CommaObj} {f : CommaHom a b} → (CommaId ∙ f) ⋍ f - identityL {a} {b} {f} = let open ≈-Reasoning A in begin - arrow (CommaId ∙ f) - ≈⟨⟩ - arrow (CommaId {b} ) o arrow f - ≈⟨⟩ - id1 A (obj b) o arrow f - ≈⟨ idL ⟩ - arrow f - ∎ + isEquivalence = record { refl = record { eqa = let open ≈-Reasoning (A) in refl-hom ; eqb = let open ≈-Reasoning (B) in refl-hom } ; + sym = λ {f} {g} f=g → record { eqa = let open ≈-Reasoning (A) in sym ( eqa f=g) ; eqb = let open ≈-Reasoning (B) in sym ( eqb f=g ) } ; + trans = λ {f} {g} {h} f=g g=h → record { + eqa = let open ≈-Reasoning (A) in trans-hom (eqa f=g) (eqa g=h) + ; eqb = let open ≈-Reasoning (B) in trans-hom (eqb f=g) (eqb g=h) + } } + ; identityL = λ{a b f} → record { + eqa = let open ≈-Reasoning (A) in idL {obj a} {obj b} {arrow f} + ; eqb = let open ≈-Reasoning (B) in idL {objb a} {objb b} {arrowg f} + } + ; identityR = λ{a b f} → record { + eqa = let open ≈-Reasoning (A) in idR {obj a} {obj b} {arrow f} + ; eqb = let open ≈-Reasoning (B) in idR {objb a} {objb b} {arrowg f} + } + ; o-resp-≈ = λ {a b c } {f g } {h i } f=g h=i → record { + eqa = IsCategory.o-resp-≈ (Category.isCategory A) (eqa f=g) (eqa h=i ) + ; eqb = IsCategory.o-resp-≈ (Category.isCategory B) (eqb f=g) (eqb h=i ) + } + ; associative = λ {a b c d} {f} {g} {h} → record { + eqa = IsCategory.associative (Category.isCategory A) + ; eqb = IsCategory.associative (Category.isCategory B) + } + } _↓_ : Category (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ _↓_ = record { Obj = CommaObj diff -r dc24ac6ebdb3 -r a5034bdf6f38 HomReasoning.agda --- a/HomReasoning.agda Thu Mar 09 09:03:07 2017 +0900 +++ b/HomReasoning.agda Thu Mar 09 14:16:03 2017 +0900 @@ -64,7 +64,7 @@ id : (a : Obj A ) → Hom A a a id a = (Id {_} {_} {_} {A} a) - idL : {a b : Obj A } { f : Hom A b a } → id a o f ≈ f + idL : {a b : Obj A } { f : Hom A a b } → id b o f ≈ f idL = IsCategory.identityL (Category.isCategory A) idR : {a b : Obj A } { f : Hom A a b } → f o id a ≈ f