Mercurial > hg > Members > kono > Proof > category
comparison CCChom.agda @ 793:f37f11e1b871
Hom a,b = Hom 1 b^a
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 22 Apr 2019 02:41:53 +0900 |
parents | 1e7319868d77 |
children | ba575c73ea48 |
comparison
equal
deleted
inserted
replaced
792:5bee48f7c126 | 793:f37f11e1b871 |
---|---|
91 c102 : {a : Obj A} → Hom OneCat OneObj OneObj → Hom A a (CCC.1 c) | 91 c102 : {a : Obj A} → Hom OneCat OneObj OneObj → Hom A a (CCC.1 c) |
92 c102 {a} OneObj = CCC.○ c a | 92 c102 {a} OneObj = CCC.○ c a |
93 c103 : {a : Obj A } {b c : Obj OneCat} {f : Hom OneCat b b } → _[_≈_] OneCat {b} {c} ( c101 {a} (c102 {a} f) ) f | 93 c103 : {a : Obj A } {b c : Obj OneCat} {f : Hom OneCat b b } → _[_≈_] OneCat {b} {c} ( c101 {a} (c102 {a} f) ) f |
94 c103 {a} {OneObj} {OneObj} {OneObj} = refl | 94 c103 {a} {OneObj} {OneObj} {OneObj} = refl |
95 c104 : {a : Obj A} → {f : Hom A a (CCC.1 c)} → A [ (c102 ( c101 f )) ≈ f ] | 95 c104 : {a : Obj A} → {f : Hom A a (CCC.1 c)} → A [ (c102 ( c101 f )) ≈ f ] |
96 c104 {a} {f} = let open ≈-Reasoning A in HomReasoning.≈-Reasoning.sym A (IsCCC.e2 (CCC.isCCC c) f ) | 96 c104 {a} {f} = let open ≈-Reasoning A in HomReasoning.≈-Reasoning.sym A (IsCCC.e2 (CCC.isCCC c) ) |
97 c201 : { c₁ a b : Obj A} → Hom A c₁ ((c CCC.∧ a) b) → Hom (A × A) (c₁ , c₁) (a , b) | 97 c201 : { c₁ a b : Obj A} → Hom A c₁ ((c CCC.∧ a) b) → Hom (A × A) (c₁ , c₁) (a , b) |
98 c201 f = ( A [ CCC.π c o f ] , A [ CCC.π' c o f ] ) | 98 c201 f = ( A [ CCC.π c o f ] , A [ CCC.π' c o f ] ) |
99 c202 : { c₁ a b : Obj A} → Hom (A × A) (c₁ , c₁) (a , b) → Hom A c₁ ((c CCC.∧ a) b) | 99 c202 : { c₁ a b : Obj A} → Hom (A × A) (c₁ , c₁) (a , b) → Hom A c₁ ((c CCC.∧ a) b) |
100 c202 (f , g ) = CCC.<_,_> c f g | 100 c202 (f , g ) = CCC.<_,_> c f g |
101 c203 : { c₁ a b : Obj A} → {f : Hom (A × A) (c₁ , c₁) (a , b)} → (A × A) [ (c201 ( c202 f )) ≈ f ] | 101 c203 : { c₁ a b : Obj A} → {f : Hom (A × A) (c₁ , c₁) (a , b)} → (A × A) [ (c201 ( c202 f )) ≈ f ] |
164 (CCC.ε c) o (CCC.<_,_> c ( k o (CCC.π c) ) (CCC.π' c)) | 164 (CCC.ε c) o (CCC.<_,_> c ( k o (CCC.π c) ) (CCC.π' c)) |
165 ≈⟨⟩ | 165 ≈⟨⟩ |
166 c301 k | 166 c301 k |
167 ∎ where open ≈-Reasoning A | 167 ∎ where open ≈-Reasoning A |
168 | 168 |
169 lemma1 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( ccc : CCC A ) → {a b c : Obj A} → -- Hom A 1 ( c ^ b ) ≅ Hom A b c | |
170 IsoS A A (CCC.1 ccc ) (CCC._<=_ ccc c b) b c | |
171 lemma1 A ccc {a} {b} {c} = record { | |
172 ≅→ = λ f → A [ CCC.ε ccc o CCC.<_,_> ccc ( A [ f o CCC.○ ccc b ] ) ( id1 A b ) ] | |
173 ; ≅← = λ f → CCC._* ccc ( A [ f o CCC.π' ccc ] ) | |
174 ; iso→ = iso→ | |
175 ; iso← = iso← | |
176 ; cong→ = cong* | |
177 ; cong← = cong2 | |
178 } where | |
179 cc = IsCCChom.ccc-3 ( CCChom.isCCChom (CCC→hom A ccc ) ) | |
180 -- e4a : {a b c : Obj A} → { k : Hom A (c /\ b) a } → A [ A [ ε o ( <,> ( A [ (k *) o π ] ) π') ] ≈ k ] | |
181 iso→ : {f : Hom A b c} → A [ | |
182 (A Category.o CCC.ε ccc) (CCC.< ccc , (A Category.o (ccc CCC.*) ((A Category.o f) (CCC.π' ccc))) (CCC.○ ccc b) > (Category.Category.Id A)) ≈ f ] | |
183 iso→ {f} = begin | |
184 CCC.ε ccc o (CCC.<_,_> ccc (CCC._* ccc ( f o (CCC.π' ccc)) o (CCC.○ ccc b)) (id1 A b ) ) | |
185 ≈↑⟨ cdr ( IsCCC.π-cong ( CCC.isCCC ccc ) refl-hom (IsCCC.e3b (CCC.isCCC ccc) ) ) ⟩ | |
186 CCC.ε ccc o ( CCC.<_,_> ccc (CCC._* ccc (f o CCC.π' ccc) o CCC.○ ccc b) ((CCC.π' ccc) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) ) ) | |
187 ≈↑⟨ cdr ( IsCCC.π-cong ( CCC.isCCC ccc ) (cdr (IsCCC.e3a (CCC.isCCC ccc))) refl-hom ) ⟩ | |
188 CCC.ε ccc o ( CCC.<_,_> ccc (CCC._* ccc (f o CCC.π' ccc) o ( CCC.π ccc o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) ) ) ((CCC.π' ccc) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) ) ) | |
189 ≈⟨ cdr ( IsCCC.π-cong ( CCC.isCCC ccc ) assoc refl-hom ) ⟩ | |
190 CCC.ε ccc o ( CCC.<_,_> ccc ((CCC._* ccc (f o CCC.π' ccc) o CCC.π ccc ) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) ) ((CCC.π' ccc) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) ) ) | |
191 ≈↑⟨ cdr ( IsCCC.distr ( CCC.isCCC ccc ) ) ⟩ | |
192 CCC.ε ccc o ( CCC.<_,_> ccc (CCC._* ccc (f o CCC.π' ccc) o CCC.π ccc ) (CCC.π' ccc) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) ) | |
193 ≈⟨ assoc ⟩ | |
194 ( CCC.ε ccc o CCC.<_,_> ccc (CCC._* ccc (f o CCC.π' ccc) o CCC.π ccc ) (CCC.π' ccc) ) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) | |
195 ≈⟨ car ( IsCCC.e4a (CCC.isCCC ccc) ) ⟩ | |
196 ( f o CCC.π' ccc ) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) | |
197 ≈↑⟨ assoc ⟩ | |
198 f o ( CCC.π' ccc o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) ) | |
199 ≈⟨ cdr (IsCCC.e3b (CCC.isCCC ccc)) ⟩ | |
200 f o id1 A b | |
201 ≈⟨ idR ⟩ | |
202 f | |
203 ∎ where open ≈-Reasoning A | |
204 lemma : {f : Hom A (CCC.1 ccc) ((ccc CCC.<= c) b)} → A [ A [ A [ f o (CCC.○ ccc b) ] o (CCC.π' ccc) ] ≈ A [ f o (CCC.π ccc) ] ] | |
205 lemma {f} = begin | |
206 ( f o (CCC.○ ccc b) ) o (CCC.π' ccc) | |
207 ≈↑⟨ assoc ⟩ | |
208 f o ( (CCC.○ ccc b) o (CCC.π' ccc) ) | |
209 ≈⟨ cdr ( IsCCC.e2 (CCC.isCCC ccc) ) ⟩ | |
210 f o (CCC.○ ccc ( CCC._∧_ ccc (CCC.1 ccc) b ) ) | |
211 ≈↑⟨ cdr ( IsCCC.e2 (CCC.isCCC ccc) ) ⟩ | |
212 f o ( (CCC.○ ccc) (CCC.1 ccc) o (CCC.π ccc) ) | |
213 ≈↑⟨ cdr ( car ( IsCCC.e2 (CCC.isCCC ccc) )) ⟩ | |
214 f o ( id1 A (CCC.1 ccc) o (CCC.π ccc) ) | |
215 ≈⟨ cdr (idL) ⟩ | |
216 f o (CCC.π ccc) | |
217 ∎ where open ≈-Reasoning A | |
218 -- e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o ( <,> ( A [ k o π ] ) π' ) ] ) * ≈ k ] | |
219 iso← : {f : Hom A (CCC.1 ccc) ((ccc CCC.<= c) b)} → A [ (ccc CCC.*) ((A Category.o (A Category.o CCC.ε ccc) (CCC.< ccc , (A Category.o f) (CCC.○ ccc b) > | |
220 (Category.Category.Id A))) (CCC.π' ccc)) ≈ f ] | |
221 iso← {f} = begin | |
222 CCC._* ccc (( CCC.ε ccc o ( CCC.<_,_> ccc ( f o (CCC.○ ccc b) ) (id1 A b ))) o (CCC.π' ccc)) | |
223 ≈↑⟨ IsCCC.*-cong ( CCC.isCCC ccc ) assoc ⟩ | |
224 CCC._* ccc ( CCC.ε ccc o (( CCC.<_,_> ccc ( f o (CCC.○ ccc b) ) (id1 A b )) o (CCC.π' ccc))) | |
225 ≈⟨ IsCCC.*-cong ( CCC.isCCC ccc ) (cdr ( IsCCC.distr ( CCC.isCCC ccc ) ) ) ⟩ | |
226 CCC._* ccc ( CCC.ε ccc o CCC.<_,_> ccc ( (f o (CCC.○ ccc b)) o CCC.π' ccc ) (id1 A b o CCC.π' ccc) ) | |
227 ≈⟨ IsCCC.*-cong ( CCC.isCCC ccc ) (cdr ( IsCCC.π-cong ( CCC.isCCC ccc ) lemma idL )) ⟩ | |
228 CCC._* ccc ( CCC.ε ccc o CCC.<_,_> ccc ( f o CCC.π ccc ) (CCC.π' ccc) ) | |
229 ≈⟨ IsCCC.e4b (CCC.isCCC ccc) ⟩ | |
230 f | |
231 ∎ where open ≈-Reasoning A | |
232 cong* : {f g : Hom A (CCC.1 ccc) ((ccc CCC.<= c) b)} → | |
233 A [ f ≈ g ] → A [ (A Category.o CCC.ε ccc) (CCC.< ccc , (A Category.o f) (CCC.○ ccc b) > (Category.Category.Id A)) | |
234 ≈ (A Category.o CCC.ε ccc) (CCC.< ccc , (A Category.o g) (CCC.○ ccc b) > (Category.Category.Id A)) ] | |
235 cong* {f} {g} f≈g = begin | |
236 CCC.ε ccc o ( CCC.<_,_> ccc ( f o ( CCC.○ ccc b )) (id1 A b )) | |
237 ≈⟨ cdr (IsCCC.π-cong ( CCC.isCCC ccc ) (car f≈g) refl-hom ) ⟩ | |
238 CCC.ε ccc o ( CCC.<_,_> ccc ( g o ( CCC.○ ccc b )) (id1 A b )) | |
239 ∎ where open ≈-Reasoning A | |
240 cong2 : {f g : Hom A b c} → A [ f ≈ g ] → | |
241 A [ (ccc CCC.*) ((A Category.o f) (CCC.π' ccc)) ≈ (ccc CCC.*) ((A Category.o g) (CCC.π' ccc)) ] | |
242 cong2 {f} {g} f≈g = begin | |
243 CCC._* ccc ( f o (CCC.π' ccc) ) | |
244 ≈⟨ IsCCC.*-cong ( CCC.isCCC ccc ) (car f≈g ) ⟩ | |
245 CCC._* ccc ( g o (CCC.π' ccc) ) | |
246 ∎ where open ≈-Reasoning A | |
247 | |
248 | |
169 | 249 |
170 | 250 |
171 open CCChom | 251 open CCChom |
172 open IsCCChom | 252 open IsCCChom |
173 open IsoS | 253 open IsoS |
214 ; e4b = e4b | 294 ; e4b = e4b |
215 ; *-cong = *-cong | 295 ; *-cong = *-cong |
216 } where | 296 } where |
217 e20 : ∀ ( f : Hom OneCat OneObj OneObj ) → _[_≈_] OneCat {OneObj} {OneObj} f OneObj | 297 e20 : ∀ ( f : Hom OneCat OneObj OneObj ) → _[_≈_] OneCat {OneObj} {OneObj} f OneObj |
218 e20 OneObj = refl | 298 e20 OneObj = refl |
219 e2 : {a : Obj A} → ∀ ( f : Hom A a 1 ) → A [ f ≈ ○ a ] | 299 e2 : {a : Obj A} → ∀ { f : Hom A a 1 } → A [ f ≈ ○ a ] |
220 e2 {a} f = begin | 300 e2 {a} {f} = begin |
221 f | 301 f |
222 ≈↑⟨ iso← ( ccc-1 (isCCChom h )) ⟩ | 302 ≈↑⟨ iso← ( ccc-1 (isCCChom h )) ⟩ |
223 ≅← ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj}) ( ≅→ ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) f ) | 303 ≅← ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj}) ( ≅→ ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) f ) |
224 ≈⟨ ≡-cong {Level.zero} {Level.zero} {Level.zero} {OneCat} {OneObj} {OneObj} ( | 304 ≈⟨ ≡-cong {Level.zero} {Level.zero} {Level.zero} {OneCat} {OneObj} {OneObj} ( |
225 λ y → ≅← ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) y ) (e20 ( ≅→ ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) f) ) ⟩ | 305 λ y → ≅← ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) y ) (e20 ( ≅→ ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) f) ) ⟩ |
361 ; π-cong = π-cong | 441 ; π-cong = π-cong |
362 ; e4a = e4a | 442 ; e4a = e4a |
363 ; e4b = e4b | 443 ; e4b = e4b |
364 ; *-cong = *-cong | 444 ; *-cong = *-cong |
365 } where | 445 } where |
366 e2 : {a : Obj Sets} (f : Hom Sets a 1) → Sets [ f ≈ ○ a ] | 446 e2 : {a : Obj Sets} {f : Hom Sets a 1} → Sets [ f ≈ ○ a ] |
367 e2 {a} f = extensionality Sets ( λ x → e20 x ) | 447 e2 {a} {f} = extensionality Sets ( λ x → e20 x ) |
368 where | 448 where |
369 e20 : (x : a ) → f x ≡ ○ a x | 449 e20 : (x : a ) → f x ≡ ○ a x |
370 e20 x with f x | 450 e20 x with f x |
371 e20 x | OneObj' = refl | 451 e20 x | OneObj' = refl |
372 e3a : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} → | 452 e3a : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} → |