Mercurial > hg > Members > kono > Proof > category
changeset 480:08f9c8a59ff4
add Comma1
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 10 Mar 2017 18:56:21 +0900 |
| parents | a5034bdf6f38 |
| children | 65e6906782bb |
| files | Comma.agda Comma1.agda |
| diffstat | 2 files changed, 173 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/Comma.agda Thu Mar 09 14:16:03 2017 +0900 +++ b/Comma.agda Fri Mar 10 18:56:21 2017 +0900 @@ -102,8 +102,8 @@ } } -_↓_ : Category (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ -_↓_ = record { Obj = CommaObj +CommaCategory : Category (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ +CommaCategory = record { Obj = CommaObj ; Hom = CommaHom ; _o_ = _∙_ ; _≈_ = _⋍_ @@ -111,4 +111,3 @@ ; isCategory = isCommaCategory } -
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Comma1.agda Fri Mar 10 18:56:21 2017 +0900 @@ -0,0 +1,171 @@ +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 )