Mercurial > hg > Members > kono > Proof > category
annotate pullback.agda @ 692:3ca3b5a4ab45
fix comment
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 12 Nov 2017 10:01:06 +0900 |
| parents | 917e51be9bbf |
| children | 984518c56e96 |
| rev | line source |
|---|---|
| 260 | 1 -- Pullback from product and equalizer |
| 2 -- | |
| 3 -- | |
| 4 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp> | |
| 5 ---- | |
| 6 | |
| 7 open import Category -- https://github.com/konn/category-agda | |
| 8 open import Level | |
| 266 | 9 module pullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ') ( Γ : Functor I A ) where |
| 260 | 10 |
| 11 open import HomReasoning | |
| 12 open import cat-utility | |
| 13 | |
| 282 | 14 -- |
| 264 | 15 -- Pullback from equalizer and product |
| 260 | 16 -- f |
| 300 | 17 -- a ------→ c |
| 682 | 18 -- ^ ^ |
| 19 -- π1 | |g | |
| 20 -- | | | |
| 21 -- axb -----→ b | |
| 260 | 22 -- ^ π2 |
| 23 -- | | |
| 282 | 24 -- | e = equalizer (f π1) (g π1) |
| 264 | 25 -- | |
| 26 -- d <------------------ d' | |
| 27 -- k (π1' × π2' ) | |
| 260 | 28 |
| 261 | 29 open Equalizer |
| 443 | 30 open IsEqualizer |
| 672 | 31 open IsProduct |
| 261 | 32 |
|
681
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
33 pullback-from : {a b c : Obj A} |
| 260 | 34 ( f : Hom A a c ) ( g : Hom A b c ) |
|
681
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
35 ( eqa : {a b : Obj A} → (f g : Hom A a b) → Equalizer A f g ) |
|
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
36 ( prod : ( a b : Obj A ) → Product A a b ) → Pullback A f g |
|
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
37 pullback-from {a} {b} {c} f g eqa prod0 = record { |
| 682 | 38 ab = d ; |
|
681
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
39 π1 = A [ π1 o e ] ; |
|
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
40 π2 = A [ π2 o e ] ; |
|
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
41 isPullback = record { |
| 260 | 42 commute = commute1 ; |
|
681
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
43 pullback = p1 ; |
| 282 | 44 π1p=π1 = λ {d} {π1'} {π2'} {eq} → π1p=π11 {d} {π1'} {π2'} {eq} ; |
| 45 π2p=π2 = λ {d} {π1'} {π2'} {eq} → π2p=π21 {d} {π1'} {π2'} {eq} ; | |
| 260 | 46 uniqueness = uniqueness1 |
|
681
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
47 } |
| 282 | 48 } where |
| 686 | 49 axb : Obj A |
| 50 axb = Product.product (prod0 a b) | |
| 51 π1 : Hom A axb a | |
|
681
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
52 π1 = Product.π1 (prod0 a b ) |
| 686 | 53 π2 : Hom A axb b |
|
681
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
54 π2 = Product.π2 (prod0 a b ) |
| 682 | 55 d : Obj A |
| 56 d = equalizer-c (eqa (A [ f o π1 ]) (A [ g o π2 ])) | |
| 686 | 57 e : Hom A d axb |
|
681
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
58 e = equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) |
|
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
59 prod = Product.isProduct (prod0 a b) |
| 682 | 60 commute1 : A [ A [ f o A [ π1 o e ] ] |
| 61 ≈ A [ g o A [ π2 o e ] ] ] | |
| 262 | 62 commute1 = let open ≈-Reasoning (A) in |
| 63 begin | |
| 682 | 64 f o ( π1 o e ) |
| 262 | 65 ≈⟨ assoc ⟩ |
| 682 | 66 ( f o π1 ) o e |
|
681
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
67 ≈⟨ fe=ge (isEqualizer (eqa (A [ f o π1 ]) (A [ g o π2 ]))) ⟩ |
| 682 | 68 ( g o π2 ) o e |
| 262 | 69 ≈↑⟨ assoc ⟩ |
| 682 | 70 g o ( π2 o e ) |
| 262 | 71 ∎ |
| 282 | 72 lemma1 : {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → |
| 262 | 73 A [ A [ A [ f o π1 ] o (prod × π1') π2' ] ≈ A [ A [ g o π2 ] o (prod × π1') π2' ] ] |
| 282 | 74 lemma1 {d'} { π1' } { π2' } eq = let open ≈-Reasoning (A) in |
| 262 | 75 begin |
| 76 ( f o π1 ) o (prod × π1') π2' | |
| 77 ≈↑⟨ assoc ⟩ | |
| 78 f o ( π1 o (prod × π1') π2' ) | |
| 79 ≈⟨ cdr (π1fxg=f prod) ⟩ | |
| 80 f o π1' | |
| 81 ≈⟨ eq ⟩ | |
| 82 g o π2' | |
| 83 ≈↑⟨ cdr (π2fxg=g prod) ⟩ | |
| 84 g o ( π2 o (prod × π1') π2' ) | |
| 85 ≈⟨ assoc ⟩ | |
| 86 ( g o π2 ) o (prod × π1') π2' | |
| 87 ∎ | |
| 682 | 88 p1 : {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → Hom A d' d |
| 282 | 89 p1 {d'} { π1' } { π2' } eq = |
|
681
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
90 let open ≈-Reasoning (A) in k (isEqualizer (eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ))) (_×_ prod π1' π2' ) ( lemma1 eq ) |
| 282 | 91 π1p=π11 : {d₁ : Obj A} {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} → |
|
681
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
92 A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) ) ] o p1 eq ] ≈ π1' ] |
| 262 | 93 π1p=π11 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in |
| 94 begin | |
|
681
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
95 ( π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) ) ) o p1 eq |
| 262 | 96 ≈⟨⟩ |
|
681
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
97 ( π1 o e) o k (isEqualizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) )) (_×_ prod π1' π2' ) (lemma1 eq) |
| 262 | 98 ≈↑⟨ assoc ⟩ |
|
681
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
99 π1 o ( e o k (isEqualizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) )) (_×_ prod π1' π2' ) (lemma1 eq) ) |
|
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
100 ≈⟨ cdr ( ek=h (isEqualizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) ))) ⟩ |
| 282 | 101 π1 o (_×_ prod π1' π2' ) |
| 262 | 102 ≈⟨ π1fxg=f prod ⟩ |
| 103 π1' | |
| 104 ∎ | |
| 282 | 105 π2p=π21 : {d₁ : Obj A} {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} → |
|
681
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
106 A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) ) ] o p1 eq ] ≈ π2' ] |
| 262 | 107 π2p=π21 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in |
| 108 begin | |
|
681
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
109 ( π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) ) ) o p1 eq |
| 262 | 110 ≈⟨⟩ |
|
681
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
111 ( π2 o e) o k (isEqualizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) )) (_×_ prod π1' π2' ) (lemma1 eq) |
| 262 | 112 ≈↑⟨ assoc ⟩ |
|
681
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
113 π2 o ( e o k (isEqualizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) )) (_×_ prod π1' π2' ) (lemma1 eq) ) |
|
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
114 ≈⟨ cdr ( ek=h (isEqualizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) ))) ⟩ |
| 282 | 115 π2 o (_×_ prod π1' π2' ) |
| 262 | 116 ≈⟨ π2fxg=g prod ⟩ |
| 117 π2' | |
| 118 ∎ | |
| 682 | 119 uniqueness1 : {d₁ : Obj A} (p' : Hom A d₁ d) {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} |
| 302 | 120 {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} → |
|
681
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
121 {eq1 : A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π1' ]} → |
|
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
122 {eq2 : A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π2' ]} → |
| 261 | 123 A [ p1 eq ≈ p' ] |
| 264 | 124 uniqueness1 {d'} p' {π1'} {π2'} {eq} {eq1} {eq2} = let open ≈-Reasoning (A) in |
| 263 | 125 begin |
| 126 p1 eq | |
| 127 ≈⟨⟩ | |
|
681
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
128 k (isEqualizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) )) (_×_ prod π1' π2' ) (lemma1 eq) |
|
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
129 ≈⟨ IsEqualizer.uniqueness (isEqualizer (eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) )) ( begin |
| 264 | 130 e o p' |
| 131 ≈⟨⟩ | |
|
681
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
132 equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p' |
| 672 | 133 ≈↑⟨ IsProduct.uniqueness prod ⟩ |
|
681
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
134 (prod × ( π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p') ) ( π2 o (equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p')) |
| 264 | 135 ≈⟨ ×-cong prod (assoc) (assoc) ⟩ |
|
681
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
136 (prod × (A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ])) |
|
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
680
diff
changeset
|
137 (A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ]) |
| 264 | 138 ≈⟨ ×-cong prod eq1 eq2 ⟩ |
| 139 ((prod × π1') π2') | |
| 140 ∎ ) ⟩ | |
| 263 | 141 p' |
| 142 ∎ | |
| 143 | |
| 266 | 144 -------------------------------- |
| 145 -- | |
| 146 -- If we have two limits on c and c', there are isomorphic pair h, h' | |
| 147 | |
| 148 open Limit | |
| 487 | 149 open IsLimit |
|
312
702adc45704f
is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
303
diff
changeset
|
150 open NTrans |
| 266 | 151 |
| 152 iso-l : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
153 ( lim : Limit I A Γ ) → ( lim' : Limit I A Γ ) |
|
484
fcae3025d900
fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
475
diff
changeset
|
154 → Hom A (a0 lim )(a0 lim') |
| 487 | 155 iso-l I Γ lim lim' = limit (isLimit lim') (a0 lim) ( t0 lim) |
| 266 | 156 |
| 157 iso-r : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
158 ( lim : Limit I A Γ ) → ( lim' : Limit I A Γ ) |
|
484
fcae3025d900
fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
475
diff
changeset
|
159 → Hom A (a0 lim') (a0 lim) |
| 487 | 160 iso-r I Γ lim lim' = limit (isLimit lim) (a0 lim') (t0 lim') |
| 266 | 161 |
| 162 | |
| 163 iso-lr : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
164 ( lim : Limit I A Γ ) → ( lim' : Limit I A Γ ) → |
|
484
fcae3025d900
fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
475
diff
changeset
|
165 ∀{ i : Obj I } → A [ A [ iso-l I Γ lim lim' o iso-r I Γ lim lim' ] ≈ id1 A (a0 lim') ] |
|
fcae3025d900
fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
475
diff
changeset
|
166 iso-lr I Γ lim lim' {i} = let open ≈-Reasoning (A) in begin |
|
fcae3025d900
fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
475
diff
changeset
|
167 iso-l I Γ lim lim' o iso-r I Γ lim lim' |
|
fcae3025d900
fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
475
diff
changeset
|
168 ≈⟨⟩ |
| 487 | 169 limit (isLimit lim') (a0 lim) ( t0 lim) o limit (isLimit lim) (a0 lim') (t0 lim') |
| 495 | 170 ≈↑⟨ limit-uniqueness (isLimit lim') ( λ {i} → ( begin |
| 487 | 171 TMap (t0 lim') i o ( limit (isLimit lim') (a0 lim) (t0 lim) o limit (isLimit lim) (a0 lim') (t0 lim') ) |
| 266 | 172 ≈⟨ assoc ⟩ |
| 487 | 173 ( TMap (t0 lim') i o limit (isLimit lim') (a0 lim) (t0 lim) ) o limit (isLimit lim) (a0 lim') (t0 lim') |
| 174 ≈⟨ car ( t0f=t (isLimit lim') ) ⟩ | |
| 175 TMap (t0 lim) i o limit (isLimit lim) (a0 lim') (t0 lim') | |
| 176 ≈⟨ t0f=t (isLimit lim) ⟩ | |
|
484
fcae3025d900
fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
475
diff
changeset
|
177 TMap (t0 lim') i |
| 271 | 178 ∎) ) ⟩ |
| 487 | 179 limit (isLimit lim') (a0 lim') (t0 lim') |
| 495 | 180 ≈⟨ limit-uniqueness (isLimit lim') idR ⟩ |
|
484
fcae3025d900
fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
475
diff
changeset
|
181 id (a0 lim' ) |
| 266 | 182 ∎ |
| 183 | |
| 184 | |
|
484
fcae3025d900
fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
475
diff
changeset
|
185 |
| 282 | 186 open import CatExponetial |
| 267 | 187 |
| 188 open Functor | |
| 189 | |
| 190 -------------------------------- | |
| 191 -- | |
| 363 | 192 -- Constancy Functor |
| 266 | 193 |
| 268 | 194 KI : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) → Functor A ( A ^ I ) |
| 195 KI { c₁'} {c₂'} {ℓ'} I = record { | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
196 FObj = λ a → K I A a ; |
|
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
197 FMap = λ f → record { -- NTrans I A (K I A a) (K I A b) |
| 267 | 198 TMap = λ a → f ; |
| 282 | 199 isNTrans = record { |
| 267 | 200 commute = λ {a b f₁} → commute1 {a} {b} {f₁} f |
| 201 } | |
| 282 | 202 } ; |
| 266 | 203 isFunctor = let open ≈-Reasoning (A) in record { |
| 267 | 204 ≈-cong = λ f=g {x} → f=g |
| 266 | 205 ; identity = refl-hom |
| 267 | 206 ; distr = refl-hom |
| 266 | 207 } |
| 267 | 208 } where |
| 209 commute1 : {a b : Obj I} {f₁ : Hom I a b} → {a' b' : Obj A} → (f : Hom A a' b' ) → | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
210 A [ A [ FMap (K I A b') f₁ o f ] ≈ A [ f o FMap (K I A a') f₁ ] ] |
| 282 | 211 commute1 {a} {b} {f₁} {a'} {b'} f = let open ≈-Reasoning (A) in begin |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
212 FMap (K I A b') f₁ o f |
| 267 | 213 ≈⟨ idL ⟩ |
| 214 f | |
| 215 ≈↑⟨ idR ⟩ | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
216 f o FMap (K I A a') f₁ |
| 267 | 217 ∎ |
| 218 | |
| 219 | |
| 272 | 220 --------- |
| 221 -- | |
| 298 | 222 -- Limit Constancy Functor F : A → A^I has right adjoint |
| 223 -- | |
| 224 -- we are going to prove universal mapping | |
| 225 | |
| 226 --------- | |
| 227 -- | |
| 272 | 228 -- limit gives co universal mapping ( i.e. adjunction ) |
| 229 -- | |
| 230 -- F = KI I : Functor A (A ^ I) | |
| 282 | 231 -- U = λ b → A0 (lim b {a0 b} {t0 b} |
| 232 -- ε = λ b → T0 ( lim b {a0 b} {t0 b} ) | |
| 475 | 233 -- |
| 234 -- a0 : Obj A and t0 : NTrans K Γ come from the limit | |
| 272 | 235 |
| 282 | 236 limit2couniv : |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
237 ( lim : ( Γ : Functor I A ) → Limit I A Γ ) |
|
690
3d41a8edbf63
fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
689
diff
changeset
|
238 → coUniversalMapping A ( A ^ I ) (KI I) |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
686
diff
changeset
|
239 limit2couniv lim = record { |
|
690
3d41a8edbf63
fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
689
diff
changeset
|
240 U = λ b → a0 ( lim b) ; |
|
3d41a8edbf63
fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
689
diff
changeset
|
241 ε = λ b → t0 (lim b) ; |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
686
diff
changeset
|
242 _*' = λ {b} {a} k → limit (isLimit (lim b )) a k ; |
|
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
243 iscoUniversalMapping = record { |
| 282 | 244 couniversalMapping = λ{ b a f} → couniversalMapping1 {b} {a} {f} ; |
| 271 | 245 couniquness = couniquness2 |
|
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
246 } |
|
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
247 } where |
|
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
248 couniversalMapping1 : {b : Obj (A ^ I)} {a : Obj A} {f : Hom (A ^ I) (FObj (KI I) a) b} → |
| 487 | 249 A ^ I [ A ^ I [ t0 (lim b) o FMap (KI I) (limit (isLimit (lim b)) a f) ] ≈ f ] |
|
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
250 couniversalMapping1 {b} {a} {f} {i} = let open ≈-Reasoning (A) in begin |
| 487 | 251 TMap (t0 (lim b )) i o TMap ( FMap (KI I) (limit (isLimit (lim b )) a f) ) i |
|
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
252 ≈⟨⟩ |
| 487 | 253 TMap (t0 (lim b)) i o (limit (isLimit (lim b)) a f) |
| 254 ≈⟨ t0f=t (isLimit (lim b)) ⟩ | |
|
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
255 TMap f i -- i comes from ∀{i} → B [ TMap f i ≈ TMap g i ] |
|
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
256 ∎ |
|
484
fcae3025d900
fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
475
diff
changeset
|
257 couniquness2 : {b : Obj (A ^ I)} {a : Obj A} {f : Hom (A ^ I) (FObj (KI I) a) b} {g : Hom A a (a0 (lim b ))} → |
|
fcae3025d900
fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
475
diff
changeset
|
258 ( ∀ { i : Obj I } → A [ A [ TMap (t0 (lim b )) i o TMap ( FMap (KI I) g) i ] ≈ TMap f i ] ) |
| 487 | 259 → A [ limit (isLimit (lim b )) a f ≈ g ] |
| 271 | 260 couniquness2 {b} {a} {f} {g} lim-g=f = let open ≈-Reasoning (A) in begin |
| 487 | 261 limit (isLimit (lim b )) a f |
| 495 | 262 ≈⟨ limit-uniqueness (isLimit ( lim b )) lim-g=f ⟩ |
|
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
263 g |
|
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
264 ∎ |
| 268 | 265 |
| 272 | 266 open import Category.Cat |
| 275 | 267 |
| 282 | 268 univ2limit : |
|
690
3d41a8edbf63
fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
689
diff
changeset
|
269 ( univ : coUniversalMapping A (A ^ I) (KI I) ) → |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
270 ( Γ : Functor I A ) → Limit I A Γ |
|
690
3d41a8edbf63
fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
689
diff
changeset
|
271 univ2limit univ Γ = record { |
|
3d41a8edbf63
fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
689
diff
changeset
|
272 a0 = (coUniversalMapping.U univ ) Γ ; |
|
3d41a8edbf63
fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
689
diff
changeset
|
273 t0 = (coUniversalMapping.ε univ ) Γ ; |
| 487 | 274 isLimit = record { |
| 275 limit = λ a t → limit1 a t ; | |
| 276 t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ; | |
| 495 | 277 limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f |
| 487 | 278 } |
| 272 | 279 } where |
|
690
3d41a8edbf63
fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
689
diff
changeset
|
280 U : Obj (A ^ I) → Obj A |
|
3d41a8edbf63
fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
689
diff
changeset
|
281 U b = coUniversalMapping.U univ b |
|
3d41a8edbf63
fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
689
diff
changeset
|
282 ε : ( b : Obj (A ^ I ) ) → NTrans I A (FObj (KI I) (U b)) b |
|
3d41a8edbf63
fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
689
diff
changeset
|
283 ε b = coUniversalMapping.ε univ b |
| 689 | 284 limit1 : (a : Obj A) → NTrans I A (FObj (KI I) a) Γ → Hom A a (U Γ) |
| 285 limit1 a t = coUniversalMapping._*' univ {_} {a} t | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
286 t0f=t1 : {a : Obj A} {t : NTrans I A (K I A a) Γ} {i : Obj I} → |
| 689 | 287 A [ A [ TMap (ε Γ) i o limit1 a t ] ≈ TMap t i ] |
|
274
1b651faa2391
adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
273
diff
changeset
|
288 t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin |
| 689 | 289 TMap (ε Γ) i o limit1 a t |
|
274
1b651faa2391
adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
273
diff
changeset
|
290 ≈⟨⟩ |
| 689 | 291 TMap (ε Γ) i o coUniversalMapping._*' univ t |
| 292 ≈⟨ coIsUniversalMapping.couniversalMapping ( coUniversalMapping.iscoUniversalMapping univ) {Γ} {a} {t} ⟩ | |
|
274
1b651faa2391
adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
273
diff
changeset
|
293 TMap t i |
|
1b651faa2391
adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
273
diff
changeset
|
294 ∎ |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
295 limit-uniqueness1 : { a : Obj A } → { t : NTrans I A ( K I A a ) Γ } → { f : Hom A a (U Γ)} |
| 689 | 296 → ( ∀ { i : Obj I } → A [ A [ TMap (ε Γ) i o f ] ≈ TMap t i ] ) → A [ limit1 a t ≈ f ] |
|
274
1b651faa2391
adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
273
diff
changeset
|
297 limit-uniqueness1 {a} {t} {f} εf=t = let open ≈-Reasoning (A) in begin |
| 689 | 298 coUniversalMapping._*' univ t |
| 299 ≈⟨ ( coIsUniversalMapping.couniquness ( coUniversalMapping.iscoUniversalMapping univ) ) εf=t ⟩ | |
|
274
1b651faa2391
adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
273
diff
changeset
|
300 f |
|
1b651faa2391
adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
273
diff
changeset
|
301 ∎ |
|
1b651faa2391
adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
273
diff
changeset
|
302 |
|
303
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
303 |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
686
diff
changeset
|
304 |
| 686 | 305 -- another form of uniqueness of a product |
| 672 | 306 lemma-p0 : (a b ab : Obj A) ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) ( prod : IsProduct A a b ab π1 π2 ) → |
|
303
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
307 A [ _×_ prod π1 π2 ≈ id1 A ab ] |
|
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
308 lemma-p0 a b ab π1 π2 prod = let open ≈-Reasoning (A) in begin |
|
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
309 _×_ prod π1 π2 |
|
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
310 ≈↑⟨ ×-cong prod idR idR ⟩ |
|
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
311 _×_ prod (A [ π1 o id1 A ab ]) (A [ π2 o id1 A ab ]) |
| 672 | 312 ≈⟨ IsProduct.uniqueness prod ⟩ |
|
303
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
313 id1 A ab |
|
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
314 ∎ |
|
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
315 |
|
7f40d6a51c72
Limit form equalizer and product done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
302
diff
changeset
|
316 |
| 282 | 317 open IProduct |
|
508
3ce21b2a671a
IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
495
diff
changeset
|
318 open IsIProduct |
| 283 | 319 open Equalizer |
|
281
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
320 |
| 282 | 321 -- |
| 322 -- limit from equalizer and product | |
| 323 -- | |
| 685 | 324 -- Γu |
| 692 | 325 -- → Γj → Γk ← |
| 326 -- / ↑ ↑ \ | |
| 327 -- proj j / | | \ proj k | |
| 328 -- / μu| |μu \ Equalizer have to be independent from j and k | |
| 329 -- | | | | so we need products of Obj I and Hom I | |
| 686 | 330 -- |product of Hom I | |
| 331 -- | ↑ ↑ | K u = id lim | |
| 332 -- | f(id)} | | | |
| 333 -- | | |g(Γ) | lim = K j -----------→ K k = lim | |
| 334 -- | | | | | u | | |
| 692 | 335 -- \ | | / proj j o e = ε j | | ε k = proj k o e |
| 686 | 336 -- product of Obj I μ u o g o e | | μ u o f o e |
| 337 -- ↑ | | | |
|
678
867ea41b331c
extensionality remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
677
diff
changeset
|
338 -- | e = equalizer f g | | |
| 682 | 339 -- | ↓ ↓ |
| 686 | 340 -- lim ←---------------- d' Γ j ----------→ Γ k |
| 682 | 341 -- k ( product pi ) Γ u |
| 342 -- Γ u o ε j = ε k | |
| 283 | 343 -- |
| 291 | 344 |
|
678
867ea41b331c
extensionality remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
677
diff
changeset
|
345 -- homprod should be written by IProduct |
| 686 | 346 -- If I is locally small, this is iso to a set |
|
678
867ea41b331c
extensionality remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
677
diff
changeset
|
347 record homprod {c : Level } : Set (suc c₁' ⊔ suc c₂' ) where |
|
867ea41b331c
extensionality remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
677
diff
changeset
|
348 field |
|
867ea41b331c
extensionality remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
677
diff
changeset
|
349 hom-j : Obj I |
|
867ea41b331c
extensionality remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
677
diff
changeset
|
350 hom-k : Obj I |
|
867ea41b331c
extensionality remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
677
diff
changeset
|
351 hom : Hom I hom-j hom-k |
|
867ea41b331c
extensionality remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
677
diff
changeset
|
352 open homprod |
|
867ea41b331c
extensionality remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
677
diff
changeset
|
353 |
|
680
5d894993477f
fh=gh done. limit from product and equalizer done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
679
diff
changeset
|
354 Homprod : {j k : Obj I} (u : Hom I j k) → homprod {c₁} |
|
5d894993477f
fh=gh done. limit from product and equalizer done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
679
diff
changeset
|
355 Homprod {j} {k} u = record {hom-j = j ; hom-k = k ; hom = u} |
|
5d894993477f
fh=gh done. limit from product and equalizer done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
679
diff
changeset
|
356 |
| 282 | 357 limit-from : |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
358 ( prod : {c : Level} { I : Set c } → ( ai : I → Obj A ) → IProduct I A ai ) |
|
673
0007f9a25e9c
fix limit from product and equalizer (not yet finished )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
672
diff
changeset
|
359 ( eqa : {a b : Obj A} → (f g : Hom A a b) → Equalizer A f g ) |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
360 → Limit I A Γ |
|
673
0007f9a25e9c
fix limit from product and equalizer (not yet finished )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
672
diff
changeset
|
361 limit-from prod eqa = record { |
| 682 | 362 a0 = d ; |
| 685 | 363 t0 = cone-ε ; |
| 487 | 364 isLimit = record { |
| 685 | 365 limit = λ a t → cone1 a t ; |
|
673
0007f9a25e9c
fix limit from product and equalizer (not yet finished )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
672
diff
changeset
|
366 t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ; |
| 495 | 367 limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f |
| 487 | 368 } |
| 282 | 369 } where |
|
680
5d894993477f
fh=gh done. limit from product and equalizer done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
679
diff
changeset
|
370 p0 : Obj A |
|
673
0007f9a25e9c
fix limit from product and equalizer (not yet finished )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
672
diff
changeset
|
371 p0 = iprod (prod (FObj Γ)) |
| 682 | 372 Fcod : homprod {c₁} → Obj A |
| 373 Fcod = λ u → FObj Γ ( hom-k u ) | |
| 679 | 374 f : Hom A p0 (iprod (prod Fcod)) |
|
680
5d894993477f
fh=gh done. limit from product and equalizer done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
679
diff
changeset
|
375 f = iproduct (isIProduct (prod Fcod)) (λ u → pi (prod (FObj Γ)) (hom-k u )) |
| 679 | 376 g : Hom A p0 (iprod (prod Fcod)) |
|
680
5d894993477f
fh=gh done. limit from product and equalizer done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
679
diff
changeset
|
377 g = iproduct (isIProduct (prod Fcod)) (λ u → A [ FMap Γ (hom u) o pi (prod (FObj Γ)) (hom-j u ) ] ) |
| 682 | 378 equ-ε : Equalizer A g f |
| 379 equ-ε = eqa g f | |
| 380 d : Obj A | |
| 381 d = equalizer-c equ-ε | |
| 382 e : Hom A d p0 | |
| 383 e = equalizer equ-ε | |
| 384 equ = isEqualizer equ-ε | |
| 683 | 385 -- projection of the product of Obj I |
| 682 | 386 proj : (i : Obj I) → Hom A p0 (FObj Γ i) |
| 387 proj = pi ( prod (FObj Γ) ) | |
| 388 prodΓ = isIProduct ( prod (FObj Γ) ) | |
| 683 | 389 -- projection of the product of Hom I |
| 686 | 390 μ : {j k : Obj I} → (u : Hom I j k ) → Hom A (iprod (prod Fcod)) (Fcod (Homprod u)) |
| 391 μ u = pi (prod Fcod ) (Homprod u) | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
392 cone-ε : NTrans I A (K I A (equalizer-c equ-ε ) ) Γ |
| 685 | 393 cone-ε = record { |
| 682 | 394 TMap = λ i → tmap i ; |
| 395 isNTrans = record { commute = commute1 } | |
| 396 } where | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
397 tmap : (i : Obj I) → Hom A (FObj (K I A d) i) (FObj Γ i) |
| 682 | 398 tmap i = A [ proj i o e ] |
| 399 commute1 : {j k : Obj I} {u : Hom I j k} → | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
400 A [ A [ FMap Γ u o tmap j ] ≈ A [ tmap k o FMap (K I A d) u ] ] |
| 682 | 401 commute1 {j} {k} {u} = let open ≈-Reasoning (A) in begin |
| 402 FMap Γ u o tmap j | |
| 403 ≈⟨⟩ | |
| 404 FMap Γ u o ( proj j o e ) | |
| 405 ≈⟨ assoc ⟩ | |
| 406 ( FMap Γ u o pi (prod (FObj Γ)) j ) o e | |
| 407 ≈↑⟨ car ( pif=q (isIProduct (prod Fcod )) ) ⟩ | |
| 686 | 408 ( μ u o g ) o e |
| 682 | 409 ≈↑⟨ assoc ⟩ |
| 686 | 410 μ u o (g o e ) |
| 682 | 411 ≈⟨ cdr ( fe=ge (isEqualizer equ-ε )) ⟩ |
| 686 | 412 μ u o (f o e ) |
| 682 | 413 ≈⟨ assoc ⟩ |
| 686 | 414 (μ u o f ) o e |
| 682 | 415 ≈⟨ car ( pif=q (isIProduct (prod Fcod ))) ⟩ |
| 416 pi (prod (FObj Γ)) k o e | |
| 417 ≈⟨⟩ | |
| 418 proj k o e | |
| 419 ≈↑⟨ idR ⟩ | |
| 420 (proj k o e ) o id1 A d | |
| 421 ≈⟨⟩ | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
422 tmap k o FMap (K I A d) u |
| 682 | 423 ∎ |
| 683 | 424 -- an arrow to our product of Obj I ( is an equalizer because of commutativity of t ) |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
425 h : {a : Obj A} → (t : NTrans I A (K I A a) Γ ) → Hom A a p0 |
| 683 | 426 h t = iproduct prodΓ (TMap t) |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
427 fh=gh : (a : Obj A) → (t : NTrans I A (K I A a) Γ ) → |
| 683 | 428 A [ A [ g o h t ] ≈ A [ f o h t ] ] |
| 679 | 429 fh=gh a t = let open ≈-Reasoning (A) in begin |
| 683 | 430 g o h t |
|
680
5d894993477f
fh=gh done. limit from product and equalizer done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
679
diff
changeset
|
431 ≈↑⟨ ip-uniqueness (isIProduct (prod Fcod)) ⟩ |
| 683 | 432 iproduct (isIProduct (prod Fcod)) (λ u → pi (prod Fcod) u o ( g o h t )) |
| 682 | 433 ≈⟨ ip-cong (isIProduct (prod Fcod)) ( λ u → begin |
| 683 | 434 pi (prod Fcod) u o ( g o h t ) |
| 682 | 435 ≈⟨ assoc ⟩ |
| 683 | 436 ( pi (prod Fcod) u o g ) o h t |
| 682 | 437 ≈⟨ car (pif=q (isIProduct (prod Fcod ))) ⟩ |
| 683 | 438 (FMap Γ (hom u) o pi (prod (FObj Γ)) (hom-j u) ) o h t |
| 682 | 439 ≈↑⟨ assoc ⟩ |
| 683 | 440 FMap Γ (hom u) o (pi (prod (FObj Γ)) (hom-j u) o h t ) |
| 682 | 441 ≈⟨ cdr ( pif=q prodΓ ) ⟩ |
| 442 FMap Γ (hom u) o TMap t (hom-j u) | |
| 443 ≈⟨ IsNTrans.commute (isNTrans t) ⟩ | |
| 444 TMap t (hom-k u) o id1 A a | |
| 445 ≈⟨ idR ⟩ | |
| 446 TMap t (hom-k u) | |
| 447 ≈↑⟨ pif=q prodΓ ⟩ | |
| 683 | 448 pi (prod (FObj Γ)) (hom-k u) o h t |
| 682 | 449 ≈↑⟨ car (pif=q (isIProduct (prod Fcod ))) ⟩ |
| 683 | 450 (pi (prod Fcod) u o f ) o h t |
| 682 | 451 ≈↑⟨ assoc ⟩ |
| 683 | 452 pi (prod Fcod) u o ( f o h t ) |
| 682 | 453 ∎ |
| 454 ) ⟩ | |
| 683 | 455 iproduct (isIProduct (prod Fcod)) (λ u → pi (prod Fcod) u o ( f o h t )) |
|
680
5d894993477f
fh=gh done. limit from product and equalizer done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
679
diff
changeset
|
456 ≈⟨ ip-uniqueness (isIProduct (prod Fcod)) ⟩ |
| 683 | 457 f o h t |
|
678
867ea41b331c
extensionality remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
677
diff
changeset
|
458 ∎ |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
459 cone1 : (a : Obj A) → NTrans I A (K I A a) Γ → Hom A a d |
| 685 | 460 cone1 a t = k equ (h t) ( fh=gh a t ) |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
461 t0f=t1 : {a : Obj A} {t : NTrans I A (K I A a) Γ} {i : Obj I} → |
| 685 | 462 A [ A [ TMap cone-ε i o cone1 a t ] ≈ TMap t i ] |
| 283 | 463 t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin |
| 685 | 464 TMap cone-ε i o cone1 a t |
| 283 | 465 ≈⟨⟩ |
| 683 | 466 ( ( proj i ) o e ) o k equ (h t) (fh=gh a t) |
| 283 | 467 ≈↑⟨ assoc ⟩ |
| 683 | 468 proj i o ( e o k equ (h t) (fh=gh a t ) ) |
|
673
0007f9a25e9c
fix limit from product and equalizer (not yet finished )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
672
diff
changeset
|
469 ≈⟨ cdr ( ek=h equ) ⟩ |
| 683 | 470 proj i o h t |
| 676 | 471 ≈⟨ pif=q prodΓ ⟩ |
| 283 | 472 TMap t i |
| 473 ∎ | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
474 limit-uniqueness1 : {a : Obj A} {t : NTrans I A (K I A a) Γ} {f : Hom A a d} |
| 685 | 475 → ({i : Obj I} → A [ A [ TMap cone-ε i o f ] ≈ TMap t i ]) → |
| 476 A [ cone1 a t ≈ f ] | |
| 283 | 477 limit-uniqueness1 {a} {t} {f} lim=t = let open ≈-Reasoning (A) in begin |
| 685 | 478 cone1 a t |
| 283 | 479 ≈⟨⟩ |
| 683 | 480 k equ (h t) (fh=gh a t) |
|
673
0007f9a25e9c
fix limit from product and equalizer (not yet finished )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
672
diff
changeset
|
481 ≈⟨ IsEqualizer.uniqueness equ ( begin |
| 283 | 482 e o f |
|
673
0007f9a25e9c
fix limit from product and equalizer (not yet finished )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
672
diff
changeset
|
483 ≈↑⟨ ip-uniqueness prodΓ ⟩ |
|
0007f9a25e9c
fix limit from product and equalizer (not yet finished )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
672
diff
changeset
|
484 iproduct prodΓ (λ i → ( proj i o ( e o f ) ) ) |
|
0007f9a25e9c
fix limit from product and equalizer (not yet finished )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
672
diff
changeset
|
485 ≈⟨ ip-cong prodΓ ( λ i → begin |
|
285
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
486 proj i o ( e o f ) |
| 284 | 487 ≈⟨ assoc ⟩ |
|
285
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
488 ( proj i o e ) o f |
|
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
489 ≈⟨ lim=t {i} ⟩ |
|
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
490 TMap t i |
| 284 | 491 ∎ ) ⟩ |
| 683 | 492 h t |
| 283 | 493 ∎ ) ⟩ |
| 494 f | |
| 495 ∎ | |
| 496 | |
|
673
0007f9a25e9c
fix limit from product and equalizer (not yet finished )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
672
diff
changeset
|
497 |
|
0007f9a25e9c
fix limit from product and equalizer (not yet finished )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
672
diff
changeset
|
498 -- |
| 291 | 499 -- |
| 500 -- Adjoint functor preserves limits | |
| 501 -- | |
| 502 -- | |
| 503 | |
| 504 open import Category.Cat | |
| 505 | |
| 506 ta1 : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') ( Γ : Functor I B ) | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
507 ( lim : Obj B ) ( tb : NTrans I B ( K I B lim ) Γ ) → |
|
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
508 ( U : Functor B A) → NTrans I A ( K I A (FObj U lim) ) (U ○ Γ) |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
298
diff
changeset
|
509 ta1 B Γ lim tb U = record { |
| 291 | 510 TMap = TMap (Functor*Nat I A U tb) ; |
| 511 isNTrans = record { commute = λ {a} {b} {f} → let open ≈-Reasoning (A) in begin | |
| 512 FMap (U ○ Γ) f o TMap (Functor*Nat I A U tb) a | |
| 513 ≈⟨ nat ( Functor*Nat I A U tb ) ⟩ | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
514 TMap (Functor*Nat I A U tb) b o FMap (U ○ K I B lim) f |
| 291 | 515 ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩ |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
516 TMap (Functor*Nat I A U tb) b o FMap (K I A (FObj U lim)) f |
| 291 | 517 ∎ |
| 518 } } | |
| 519 | |
| 520 adjoint-preseve-limit : | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
521 { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') ( Γ : Functor I B ) ( limitb : Limit I B Γ ) → |
|
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
522 ( adj : Adjunction A B ) → Limit I A (Adjunction.U adj ○ Γ) |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
686
diff
changeset
|
523 adjoint-preseve-limit B Γ limitb adj = record { |
|
484
fcae3025d900
fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
475
diff
changeset
|
524 a0 = FObj U lim ; |
|
fcae3025d900
fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
475
diff
changeset
|
525 t0 = ta1 B Γ lim tb U ; |
| 487 | 526 isLimit = record { |
| 527 limit = λ a t → limit1 a t ; | |
| 528 t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ; | |
| 495 | 529 limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f |
| 487 | 530 } |
| 291 | 531 } where |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
686
diff
changeset
|
532 U : Functor B A |
|
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
686
diff
changeset
|
533 U = Adjunction.U adj |
|
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
686
diff
changeset
|
534 F : Functor A B |
|
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
686
diff
changeset
|
535 F = Adjunction.F adj |
|
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
686
diff
changeset
|
536 η : NTrans A A identityFunctor ( U ○ F ) |
|
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
686
diff
changeset
|
537 η = Adjunction.η adj |
|
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
686
diff
changeset
|
538 ε : NTrans B B ( F ○ U ) identityFunctor |
|
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
686
diff
changeset
|
539 ε = Adjunction.ε adj |
|
484
fcae3025d900
fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
475
diff
changeset
|
540 ta = ta1 B Γ (a0 limitb) (t0 limitb) U |
|
fcae3025d900
fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
475
diff
changeset
|
541 tb = t0 limitb |
|
fcae3025d900
fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
475
diff
changeset
|
542 lim = a0 limitb |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
543 tfmap : (a : Obj A) → NTrans I A (K I A a) (U ○ Γ) → (i : Obj I) → Hom B (FObj (K I B (FObj F a)) i) (FObj Γ i) |
| 293 | 544 tfmap a t i = B [ TMap ε (FObj Γ i) o FMap F (TMap t i) ] |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
545 tF : (a : Obj A) → NTrans I A (K I A a) (U ○ Γ) → NTrans I B (K I B (FObj F a)) Γ |
| 293 | 546 tF a t = record { |
| 547 TMap = tfmap a t ; | |
| 548 isNTrans = record { commute = λ {a'} {b} {f} → let open ≈-Reasoning (B) in begin | |
| 549 FMap Γ f o tfmap a t a' | |
| 294 | 550 ≈⟨⟩ |
| 551 FMap Γ f o ( TMap ε (FObj Γ a') o FMap F (TMap t a')) | |
| 552 ≈⟨ assoc ⟩ | |
| 553 (FMap Γ f o TMap ε (FObj Γ a') ) o FMap F (TMap t a') | |
| 554 ≈⟨ car (nat ε) ⟩ | |
| 555 (TMap ε (FObj Γ b) o FMap (F ○ U) (FMap Γ f) ) o FMap F (TMap t a') | |
| 556 ≈↑⟨ assoc ⟩ | |
| 557 TMap ε (FObj Γ b) o ( FMap (F ○ U) (FMap Γ f) o FMap F (TMap t a') ) | |
| 558 ≈↑⟨ cdr ( distr F ) ⟩ | |
| 559 TMap ε (FObj Γ b) o ( FMap F (A [ FMap U (FMap Γ f) o TMap t a' ] ) ) | |
| 560 ≈⟨ cdr ( fcong F (nat t) ) ⟩ | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
561 TMap ε (FObj Γ b) o FMap F (A [ TMap t b o FMap (K I A a) f ]) |
| 294 | 562 ≈⟨⟩ |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
563 TMap ε (FObj Γ b) o FMap F (A [ TMap t b o id1 A (FObj (K I A a) b) ]) |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
298
diff
changeset
|
564 ≈⟨ cdr ( fcong F (idR1 A)) ⟩ |
| 294 | 565 TMap ε (FObj Γ b) o FMap F (TMap t b ) |
| 566 ≈↑⟨ idR ⟩ | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
567 ( TMap ε (FObj Γ b) o FMap F (TMap t b)) o id1 B (FObj F (FObj (K I A a) b)) |
| 294 | 568 ≈⟨⟩ |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
569 tfmap a t b o FMap (K I B (FObj F a)) f |
| 293 | 570 ∎ |
| 571 } } | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
572 limit1 : (a : Obj A) → NTrans I A (K I A a) (U ○ Γ) → Hom A a (FObj U (a0 limitb) ) |
| 487 | 573 limit1 a t = A [ FMap U (limit (isLimit limitb) (FObj F a) (tF a t )) o TMap η a ] |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
574 t0f=t1 : {a : Obj A} {t : NTrans I A (K I A a) (U ○ Γ)} {i : Obj I} → |
| 291 | 575 A [ A [ TMap ta i o limit1 a t ] ≈ TMap t i ] |
| 295 | 576 t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin |
| 577 TMap ta i o limit1 a t | |
| 578 ≈⟨⟩ | |
| 487 | 579 FMap U ( TMap tb i ) o ( FMap U (limit (isLimit limitb) (FObj F a) (tF a t )) o TMap η a ) |
| 295 | 580 ≈⟨ assoc ⟩ |
| 487 | 581 ( FMap U ( TMap tb i ) o FMap U (limit (isLimit limitb) (FObj F a) (tF a t ))) o TMap η a |
| 295 | 582 ≈↑⟨ car ( distr U ) ⟩ |
| 487 | 583 FMap U ( B [ TMap tb i o limit (isLimit limitb) (FObj F a) (tF a t ) ] ) o TMap η a |
| 584 ≈⟨ car ( fcong U ( t0f=t (isLimit limitb) ) ) ⟩ | |
| 295 | 585 FMap U (TMap (tF a t) i) o TMap η a |
| 586 ≈⟨⟩ | |
| 587 FMap U ( B [ TMap ε (FObj Γ i) o FMap F (TMap t i) ] ) o TMap η a | |
| 588 ≈⟨ car ( distr U ) ⟩ | |
| 589 ( FMap U ( TMap ε (FObj Γ i)) o FMap U ( FMap F (TMap t i) )) o TMap η a | |
| 590 ≈↑⟨ assoc ⟩ | |
| 591 FMap U ( TMap ε (FObj Γ i) ) o ( FMap U ( FMap F (TMap t i) ) o TMap η a ) | |
| 592 ≈⟨ cdr ( nat η ) ⟩ | |
| 593 FMap U (TMap ε (FObj Γ i)) o ( TMap η (FObj U (FObj Γ i)) o FMap (identityFunctor {_} {_} {_} {A}) (TMap t i) ) | |
| 594 ≈⟨ assoc ⟩ | |
| 595 ( FMap U (TMap ε (FObj Γ i)) o TMap η (FObj U (FObj Γ i))) o TMap t i | |
| 596 ≈⟨ car ( IsAdjunction.adjoint1 ( Adjunction.isAdjunction adj ) ) ⟩ | |
| 597 id1 A (FObj (U ○ Γ) i) o TMap t i | |
| 598 ≈⟨ idL ⟩ | |
| 599 TMap t i | |
| 600 ∎ | |
| 296 | 601 -- ta = TMap (Functor*Nat I A U tb) , FMap U ( TMap tb i ) o f ≈ TMap t i |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
690
diff
changeset
|
602 limit-uniqueness1 : {a : Obj A} {t : NTrans I A (K I A a) (U ○ Γ)} {f : Hom A a (FObj U lim)} |
| 291 | 603 → ({i : Obj I} → A [ A [ TMap ta i o f ] ≈ TMap t i ]) → |
| 604 A [ limit1 a t ≈ f ] | |
| 295 | 605 limit-uniqueness1 {a} {t} {f} lim=t = let open ≈-Reasoning (A) in begin |
| 606 limit1 a t | |
| 607 ≈⟨⟩ | |
| 487 | 608 FMap U (limit (isLimit limitb) (FObj F a) (tF a t )) o TMap η a |
| 495 | 609 ≈⟨ car ( fcong U (limit-uniqueness (isLimit limitb) ( λ {i} → lemma1 i) )) ⟩ |
| 298 | 610 FMap U ( B [ TMap ε lim o FMap F f ] ) o TMap η a -- Universal mapping |
|
297
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
611 ≈⟨ car (distr U ) ⟩ |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
612 ( (FMap U (TMap ε lim)) o (FMap U ( FMap F f )) ) o TMap η a |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
613 ≈⟨ sym assoc ⟩ |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
614 (FMap U (TMap ε lim)) o ((FMap U ( FMap F f )) o TMap η a ) |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
615 ≈⟨ cdr (nat η) ⟩ |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
616 (FMap U (TMap ε lim)) o ((TMap η (FObj U lim )) o f ) |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
617 ≈⟨ assoc ⟩ |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
618 ((FMap U (TMap ε lim)) o (TMap η (FObj U lim))) o f |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
619 ≈⟨ car ( IsAdjunction.adjoint1 ( Adjunction.isAdjunction adj)) ⟩ |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
620 id (FObj U lim) o f |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
621 ≈⟨ idL ⟩ |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
622 f |
| 296 | 623 ∎ where |
| 624 lemma1 : (i : Obj I) → B [ B [ TMap tb i o B [ TMap ε lim o FMap F f ] ] ≈ TMap (tF a t) i ] | |
| 625 lemma1 i = let open ≈-Reasoning (B) in begin | |
| 626 TMap tb i o (TMap ε lim o FMap F f) | |
|
297
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
627 ≈⟨ assoc ⟩ |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
628 ( TMap tb i o TMap ε lim ) o FMap F f |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
629 ≈⟨ car ( nat ε ) ⟩ |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
630 ( TMap ε (FObj Γ i) o FMap F ( FMap U ( TMap tb i ))) o FMap F f |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
631 ≈↑⟨ assoc ⟩ |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
632 TMap ε (FObj Γ i) o ( FMap F ( FMap U ( TMap tb i )) o FMap F f ) |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
633 ≈↑⟨ cdr ( distr F ) ⟩ |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
634 TMap ε (FObj Γ i) o FMap F ( A [ FMap U ( TMap tb i ) o f ] ) |
|
537570f6a44f
limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
296
diff
changeset
|
635 ≈⟨ cdr ( fcong F (lim=t {i}) ) ⟩ |
| 296 | 636 TMap ε (FObj Γ i) o FMap F (TMap t i) |
| 637 ≈⟨⟩ | |
| 638 TMap (tF a t) i | |
| 639 ∎ | |
| 295 | 640 |
| 296 | 641 |
| 642 |