Mercurial > hg > Members > kono > Proof > category
annotate Comma1.agda @ 643:5eb746702732
add more lemma
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 03 Jul 2017 12:20:26 +0900 |
| parents | 65e6906782bb |
| children |
| rev | line source |
|---|---|
| 477 | 1 open import Level |
| 2 open import Category | |
| 480 | 3 module Comma1 {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {C : Category c₁' c₂' ℓ'} |
| 4 ( F : Functor A C ) ( G : Functor A C ) where | |
| 477 | 5 |
| 6 open import HomReasoning | |
| 7 open import cat-utility | |
| 8 | |
| 478 | 9 -- |
| 10 -- F G | |
| 480 | 11 -- A -> C <- A |
| 478 | 12 -- |
| 477 | 13 |
| 14 open Functor | |
| 15 | |
| 16 record CommaObj : Set ( c₁ ⊔ c₂' ) where | |
| 17 field | |
| 18 obj : Obj A | |
| 480 | 19 hom : Hom C ( FObj F obj ) ( FObj G obj ) |
| 477 | 20 |
| 21 open CommaObj | |
| 22 | |
| 23 record CommaHom ( a b : CommaObj ) : Set ( c₂ ⊔ ℓ' ) where | |
| 24 field | |
| 25 arrow : Hom A ( obj a ) ( obj b ) | |
| 480 | 26 comm : C [ C [ FMap G arrow o hom a ] ≈ C [ hom b o FMap F arrow ] ] |
| 477 | 27 |
| 28 open CommaHom | |
| 29 | |
| 30 _∙_ : {a b c : CommaObj } → CommaHom b c → CommaHom a b → CommaHom a c | |
| 31 _∙_ {a} {b} {c} f g = record { | |
| 32 arrow = A [ arrow f o arrow g ] ; | |
| 33 comm = comm1 | |
| 34 } where | |
| 480 | 35 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 ]) ] ] |
| 478 | 36 comm1 = let open ≈-Reasoning C in begin |
| 480 | 37 FMap G (A [ arrow f o arrow g ] ) o hom a |
| 478 | 38 ≈⟨ car ( distr G ) ⟩ |
| 480 | 39 ( FMap G (arrow f) o FMap G (arrow g )) o hom a |
| 478 | 40 ≈↑⟨ assoc ⟩ |
| 480 | 41 FMap G (arrow f) o ( FMap G (arrow g ) o hom a ) |
| 478 | 42 ≈⟨ cdr ( comm g ) ⟩ |
| 480 | 43 FMap G (arrow f) o ( hom b o FMap F (arrow g ) ) |
| 478 | 44 ≈⟨ assoc ⟩ |
| 480 | 45 ( FMap G (arrow f) o hom b) o FMap F (arrow g ) |
| 478 | 46 ≈⟨ car ( comm f ) ⟩ |
| 47 ( hom c o FMap F (arrow f) ) o FMap F (arrow g ) | |
| 48 ≈↑⟨ assoc ⟩ | |
| 49 hom c o ( FMap F (arrow f) o FMap F (arrow g ) ) | |
| 50 ≈↑⟨ cdr ( distr F) ⟩ | |
| 51 hom c o FMap F (A [ arrow f o arrow g ]) | |
| 52 ∎ | |
| 477 | 53 |
| 54 CommaId : { a : CommaObj } → CommaHom a a | |
| 55 CommaId {a} = record { arrow = id1 A ( obj a ) ; | |
| 56 comm = comm2 } where | |
| 480 | 57 comm2 : C [ C [ FMap G (id1 A (obj a)) o hom a ] ≈ C [ hom a o FMap F (id1 A (obj a)) ] ] |
| 478 | 58 comm2 = let open ≈-Reasoning C in begin |
| 480 | 59 FMap G (id1 A (obj a)) o hom a |
| 478 | 60 ≈⟨ car ( IsFunctor.identity ( isFunctor G ) ) ⟩ |
| 480 | 61 id1 C (FObj G (obj a)) o hom a |
| 478 | 62 ≈⟨ idL ⟩ |
| 63 hom a | |
| 64 ≈↑⟨ idR ⟩ | |
| 65 hom a o id1 C (FObj F (obj a)) | |
| 66 ≈↑⟨ cdr ( IsFunctor.identity ( isFunctor F ) )⟩ | |
| 67 hom a o FMap F (id1 A (obj a)) | |
| 68 ∎ | |
| 480 | 69 |
| 70 _⋍_ : { a b : CommaObj } ( f g : CommaHom a b ) → Set ℓ | |
| 71 f ⋍ g = A [ arrow f ≈ arrow g ] | |
| 72 | |
| 73 | |
| 477 | 74 isCommaCategory : IsCategory CommaObj CommaHom _⋍_ _∙_ CommaId |
| 75 isCommaCategory = record { | |
| 480 | 76 isEquivalence = record { refl = let open ≈-Reasoning (A) in refl-hom ; |
| 77 sym = let open ≈-Reasoning (A) in sym ; | |
| 78 trans = let open ≈-Reasoning (A) in trans-hom | |
| 79 } | |
| 80 ; identityL = let open ≈-Reasoning (A) in idL | |
| 81 ; identityR = let open ≈-Reasoning (A) in idR | |
| 82 ; o-resp-≈ = IsCategory.o-resp-≈ ( Category.isCategory A ) | |
| 83 ; associative = IsCategory.associative ( Category.isCategory A ) | |
|
479
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
478
diff
changeset
|
84 } |
| 478 | 85 |
| 480 | 86 CommaCategory : Category (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ |
| 87 CommaCategory = record { Obj = CommaObj | |
| 478 | 88 ; Hom = CommaHom |
| 89 ; _o_ = _∙_ | |
| 90 ; _≈_ = _⋍_ | |
| 91 ; Id = CommaId | |
| 92 ; isCategory = isCommaCategory | |
| 93 } | |
| 477 | 94 |
| 480 | 95 open NTrans |
| 477 | 96 |
| 480 | 97 nat-lemma : NTrans A C F G → Functor A CommaCategory |
| 98 nat-lemma n = record { | |
| 99 FObj = λ x → fobj x ; | |
| 100 FMap = λ {a} {b} f → fmap {a} {b} f ; | |
| 101 isFunctor = record { | |
| 102 identity = λ{x} → identity x | |
| 103 ; distr = λ {a} {b} {c} {f} {g} → distr1 {a} {b} {c} {f} {g} | |
| 104 ; ≈-cong = λ {a} {b} {c} {f} → ≈-cong {a} {b} {c} {f} | |
| 105 } | |
| 106 } where | |
| 107 fobj : Obj A → Obj CommaCategory | |
| 108 fobj x = record { obj = x ; hom = TMap n x } | |
| 109 fmap : {a b : Obj A } → Hom A a b → Hom CommaCategory (fobj a) (fobj b ) | |
| 110 fmap f = record { arrow = f ; comm = IsNTrans.commute (isNTrans n ) } | |
| 111 ≈-cong : {a : Obj A} {b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → CommaCategory [ fmap f ≈ fmap g ] | |
| 112 ≈-cong {a} {b} {f} {g} f=g = f=g | |
| 113 identity : (x : Obj A ) -> CommaCategory [ fmap (id1 A x) ≈ id1 CommaCategory (fobj x) ] | |
| 114 identity x = let open ≈-Reasoning (A) in begin | |
| 115 arrow (fmap (id1 A x)) | |
| 116 ≈⟨⟩ | |
| 117 id1 A x | |
| 118 ≈⟨⟩ | |
| 119 arrow (id1 CommaCategory (fobj x)) | |
| 120 ∎ | |
| 121 distr1 : {a : Obj A} {b : Obj A} {c : Obj A} {f : Hom A a b} {g : Hom A b c} → | |
| 122 CommaCategory [ fmap (A [ g o f ]) ≈ CommaCategory [ fmap g o fmap f ] ] | |
| 123 distr1 = let open ≈-Reasoning (A) in refl-hom | |
| 124 | |
| 125 nat-f : Functor A C → Functor A CommaCategory → Functor A C | |
| 126 nat-f F N = record { | |
| 127 FObj = λ x → FObj F ( obj ( FObj N x )) ; | |
| 128 FMap = λ {a} {b} f → FMap F (arrow (FMap N f)) ; | |
| 129 isFunctor = record { | |
| 130 identity = λ{x} → identity x | |
| 131 ; distr = λ {a} {b} {c} {f} {g} → distr1 {a} {b} {c} {f} {g} | |
| 132 ; ≈-cong = λ {a} {b} {f} {g} → ≈-cong {a} {b} {f} {g} | |
| 133 } | |
| 134 } where | |
| 135 identity : (x : Obj A ) -> C [ FMap F (arrow (FMap N (id1 A x))) ≈ id1 C (FObj F (obj (FObj N x))) ] | |
| 136 identity x = let open ≈-Reasoning (C) in begin | |
| 137 FMap F (arrow (FMap N (id1 A x))) | |
| 138 ≈⟨ fcong F ( IsFunctor.identity ( isFunctor N) ) ⟩ | |
| 139 FMap F (id1 A (obj (FObj N x))) | |
| 140 ≈⟨ IsFunctor.identity ( isFunctor F ) ⟩ | |
| 141 id1 C (FObj F (obj (FObj N x))) | |
| 142 ∎ | |
| 143 distr1 : {a : Obj A} {b : Obj A} {c : Obj A} {f : Hom A a b} {g : Hom A b c} → | |
| 144 C [ FMap F (arrow (FMap N (A [ g o f ]))) ≈ | |
| 145 C [ FMap F (arrow (FMap N g)) o FMap F (arrow (FMap N f)) ] ] | |
| 146 distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (C) in begin | |
| 147 FMap F (arrow (FMap N (A [ g o f ]))) | |
| 148 ≈⟨ fcong F ( IsFunctor.distr ( isFunctor N) ) ⟩ | |
| 149 FMap F (A [ arrow (FMap N g ) o arrow (FMap N f ) ] ) | |
| 150 ≈⟨ ( IsFunctor.distr ( isFunctor F ) ) ⟩ | |
| 151 FMap F (arrow (FMap N g)) o FMap F (arrow (FMap N f)) | |
| 152 ∎ | |
| 153 ≈-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)) ] | |
| 154 ≈-cong {a} {b} {f} {g} f=g = let open ≈-Reasoning (C) in begin | |
| 155 FMap F (arrow (FMap N f)) | |
| 156 ≈⟨ fcong F (( IsFunctor.≈-cong ( isFunctor N) ) f=g ) ⟩ | |
| 157 FMap F (arrow (FMap N g)) | |
| 158 ∎ | |
| 159 | |
| 160 nat-lemma← : ( N : Functor A CommaCategory ) → NTrans A C (nat-f F N) (nat-f G N) | |
| 161 nat-lemma← N = record { | |
| 162 TMap = λ (a : Obj A ) → tmap1 a | |
| 163 ; isNTrans = record { | |
| 164 commute = λ {a} {b} {f} → commute2 {a} {b} {f} | |
| 165 } | |
| 166 } where | |
| 167 tmap1 : (a : Obj A ) → Hom C (FObj F (obj ( FObj N a))) (FObj G (obj ( FObj N a))) | |
| 168 tmap1 a = hom (FObj N a) | |
| 169 commute2 : {a b : Obj A } {f : Hom A a b } → | |
| 170 C [ C [ FMap G ( arrow ( FMap N f)) o tmap1 a ] ≈ C [ tmap1 b o FMap F ( arrow ( FMap N f )) ] ] | |
| 171 commute2 {a} {b} {f} = comm ( FMap N f ) | |
|
481
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
480
diff
changeset
|
172 |
|
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
480
diff
changeset
|
173 |