Mercurial > hg > Members > kono > Proof > category
comparison CCChom.agda @ 789:4e1e2f7199c8
CCC Hom done
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 19 Apr 2019 19:20:04 +0900 |
parents | a3e124e36acf |
children | 1e7319868d77 |
comparison
equal
deleted
inserted
replaced
788:a3e124e36acf | 789:4e1e2f7199c8 |
---|---|
56 IsoS A (A × A) c (a * b) (c , c ) (a , b ) | 56 IsoS A (A × A) c (a * b) (c , c ) (a , b ) |
57 ccc-3 : {a b c : Obj A} → -- Hom A a ( c ^ b ) ≅ Hom A ( a * b ) c | 57 ccc-3 : {a b c : Obj A} → -- Hom A a ( c ^ b ) ≅ Hom A ( a * b ) c |
58 IsoS A A a (c ^ b) (a * b) c | 58 IsoS A A a (c ^ b) (a * b) c |
59 nat-2 : {a b c : Obj A} → {f : Hom A (b * c) (b * c) } → {g : Hom A a (b * c) } | 59 nat-2 : {a b c : Obj A} → {f : Hom A (b * c) (b * c) } → {g : Hom A a (b * c) } |
60 → (A × A) [ (A × A) [ IsoS.≅→ ccc-2 f o (g , g) ] ≈ IsoS.≅→ ccc-2 ( A [ f o g ] ) ] | 60 → (A × A) [ (A × A) [ IsoS.≅→ ccc-2 f o (g , g) ] ≈ IsoS.≅→ ccc-2 ( A [ f o g ] ) ] |
61 nat-3 : {a b c : Obj A} → { k : Hom A c (a ^ b ) } → A [ A [ IsoS.≅→ (ccc-3) (id1 A (a ^ b)) o | |
62 (IsoS.≅← (ccc-2 ) (A [ k o (proj₁ ( IsoS.≅→ ccc-2 (id1 A (c * b)))) ] , | |
63 (proj₂ ( IsoS.≅→ ccc-2 (id1 A (c * b) ))))) ] ≈ IsoS.≅→ (ccc-3 ) k ] | |
61 | 64 |
62 open import CCC | 65 open import CCC |
63 | 66 |
64 | 67 |
65 record CCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where | 68 record CCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where |
78 ; _^_ = CCC._<=_ c | 81 ; _^_ = CCC._<=_ c |
79 ; isCCChom = record { | 82 ; isCCChom = record { |
80 ccc-1 = λ {a} {b} {c'} → record { ≅→ = c101 ; ≅← = c102 ; iso→ = c103 {a} {b} {c'} ; iso← = c104 ; cong← = c105 ; cong→ = c106 } | 83 ccc-1 = λ {a} {b} {c'} → record { ≅→ = c101 ; ≅← = c102 ; iso→ = c103 {a} {b} {c'} ; iso← = c104 ; cong← = c105 ; cong→ = c106 } |
81 ; ccc-2 = record { ≅→ = c201 ; ≅← = c202 ; iso→ = c203 ; iso← = c204 ; cong← = c205; cong→ = c206 } | 84 ; ccc-2 = record { ≅→ = c201 ; ≅← = c202 ; iso→ = c203 ; iso← = c204 ; cong← = c205; cong→ = c206 } |
82 ; ccc-3 = record { ≅→ = c301 ; ≅← = c302 ; iso→ = c303 ; iso← = c304 ; cong← = c305 ; cong→ = c306 } | 85 ; ccc-3 = record { ≅→ = c301 ; ≅← = c302 ; iso→ = c303 ; iso← = c304 ; cong← = c305 ; cong→ = c306 } |
83 ; nat-2 = nat-2 | 86 ; nat-2 = nat-2 ; nat-3 = nat-3 |
84 } | 87 } |
85 } where | 88 } where |
86 c101 : {a : Obj A} → Hom A a (CCC.1 c) → Hom OneCat OneObj OneObj | 89 c101 : {a : Obj A} → Hom A a (CCC.1 c) → Hom OneCat OneObj OneObj |
87 c101 _ = OneObj | 90 c101 _ = OneObj |
88 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) |
136 nat-2 {a} {b} {c₁} {f} {g} = ( begin | 139 nat-2 {a} {b} {c₁} {f} {g} = ( begin |
137 ( CCC.π c o f) o g | 140 ( CCC.π c o f) o g |
138 ≈↑⟨ assoc ⟩ | 141 ≈↑⟨ assoc ⟩ |
139 ( CCC.π c ) o (f o g) | 142 ( CCC.π c ) o (f o g) |
140 ∎ ) , (sym-hom assoc) where open ≈-Reasoning A | 143 ∎ ) , (sym-hom assoc) where open ≈-Reasoning A |
144 nat-3 : {a b : Obj A} {c = c₁ : Obj A} {k : Hom A c₁ ((c CCC.<= a) b)} → | |
145 A [ A [ c301 (id1 A ((c CCC.<= a) b)) o c202 (A [ k o proj₁ (c201 (id1 A ((c CCC.∧ c₁) b))) ] , proj₂ (c201 (id1 A ((c CCC.∧ c₁) b)))) ] | |
146 ≈ c301 k ] | |
147 nat-3 {a} {b} { c₁} {k} = begin | |
148 c301 (id1 A ((c CCC.<= a) b)) o c202 ( k o proj₁ (c201 (id1 A ((c CCC.∧ c₁) b))) , proj₂ (c201 (id1 A ((c CCC.∧ c₁) b)))) | |
149 ≈⟨⟩ | |
150 ( CCC.ε c o CCC.<_,_> c ((id1 A (CCC._<=_ c a b )) o CCC.π c) (CCC.π' c)) | |
151 o (CCC.<_,_> c (k o ( CCC.π c o (id1 A (CCC._∧_ c c₁ b )))) ( CCC.π' c o (id1 A (CCC._∧_ c c₁ b)))) | |
152 ≈↑⟨ assoc ⟩ | |
153 (CCC.ε c) o (( CCC.<_,_> c ((id1 A (CCC._<=_ c a b )) o CCC.π c) (CCC.π' c)) | |
154 o (CCC.<_,_> c (k o ( CCC.π c o (id1 A (CCC._∧_ c c₁ b )))) ( CCC.π' c o (id1 A (CCC._∧_ c c₁ b))))) | |
155 ≈⟨ cdr (car (IsCCC.π-cong (CCC.isCCC c ) idL refl-hom ) ) ⟩ | |
156 (CCC.ε c) o ( CCC.<_,_> c (CCC.π c) (CCC.π' c) | |
157 o (CCC.<_,_> c (k o ( CCC.π c o (id1 A (CCC._∧_ c c₁ b )))) ( CCC.π' c o (id1 A (CCC._∧_ c c₁ b))))) | |
158 ≈⟨ cdr (car (IsCCC.π-id (CCC.isCCC c))) ⟩ | |
159 (CCC.ε c) o ( id1 A (CCC._∧_ c ((c CCC.<= a) b) b ) | |
160 o (CCC.<_,_> c (k o ( CCC.π c o (id1 A (CCC._∧_ c c₁ b )))) ( CCC.π' c o (id1 A (CCC._∧_ c c₁ b))))) | |
161 ≈⟨ cdr ( cdr ( IsCCC.π-cong (CCC.isCCC c) (cdr idR) idR )) ⟩ | |
162 (CCC.ε c) o ( id1 A (CCC._∧_ c ((c CCC.<= a) b) b ) o (CCC.<_,_> c (k o ( CCC.π c )) ( CCC.π' c ))) | |
163 ≈⟨ cdr idL ⟩ | |
164 (CCC.ε c) o (CCC.<_,_> c ( k o (CCC.π c) ) (CCC.π' c)) | |
165 ≈⟨⟩ | |
166 c301 k | |
167 ∎ where open ≈-Reasoning A | |
141 | 168 |
142 | 169 |
143 | 170 |
144 open CCChom | 171 open CCChom |
145 open IsCCChom | 172 open IsCCChom |
262 ≈⟨ cong← (ccc-2 (isCCChom h)) ( eq1 , eq2 ) ⟩ | 289 ≈⟨ cong← (ccc-2 (isCCChom h)) ( eq1 , eq2 ) ⟩ |
263 ≅← (ccc-2 (isCCChom h)) (f' , g') | 290 ≅← (ccc-2 (isCCChom h)) (f' , g') |
264 ≈⟨⟩ | 291 ≈⟨⟩ |
265 <,> f' g' | 292 <,> f' g' |
266 ∎ where open ≈-Reasoning A | 293 ∎ where open ≈-Reasoning A |
267 e40 : {a c : Obj A} → { f : Hom A (_*_ h a c ) a } → A [ ≅→ (ccc-3 (isCCChom h)) (≅← (ccc-3 (isCCChom h)) f) ≈ f ] | |
268 e40 = iso→ (ccc-3 (isCCChom h)) | |
269 e41 : {a c : Obj A} → { f : Hom A a (_^_ h c a )} → A [ ≅← (ccc-3 (isCCChom h)) (≅→ (ccc-3 (isCCChom h)) f) ≈ f ] | |
270 e41 = iso← (ccc-3 (isCCChom h)) | |
271 e4a : {a b c : Obj A} → { k : Hom A (c /\ b) a } → A [ A [ ε o ( <,> ( A [ (k *) o π ] ) π') ] ≈ k ] | 294 e4a : {a b c : Obj A} → { k : Hom A (c /\ b) a } → A [ A [ ε o ( <,> ( A [ (k *) o π ] ) π') ] ≈ k ] |
272 e4a {a} {b} {c} {k} = begin | 295 e4a {a} {b} {c} {k} = begin |
273 ε o ( <,> ((k *) o π ) π' ) | 296 ε o ( <,> ((k *) o π ) π' ) |
274 ≈⟨⟩ | 297 ≈⟨⟩ |
275 ≅→ (ccc-3 (isCCChom h)) (id1 A (_^_ h a b)) o (≅← (ccc-2 (isCCChom h)) ((( ≅← (ccc-3 (isCCChom h)) k) o π ) , π')) | 298 ≅→ (ccc-3 (isCCChom h)) (id1 A (_^_ h a b)) o (≅← (ccc-2 (isCCChom h)) ((( ≅← (ccc-3 (isCCChom h)) k) o π ) , π')) |
276 ≈⟨ {!!} ⟩ | 299 ≈⟨ nat-3 (isCCChom h) ⟩ |
277 ≅→ (ccc-3 (isCCChom h)) (id1 A (_^_ h a b)) o (≅← (ccc-2 (isCCChom h)) | |
278 (_[_o_] (A × A) ( ≅← (ccc-3 (isCCChom h)) k , id1 A b ) ( π , π'))) | |
279 ≈⟨ {!!} ⟩ | |
280 ≅→ (ccc-3 (isCCChom h)) (≅← (ccc-3 (isCCChom h)) k) | 300 ≅→ (ccc-3 (isCCChom h)) (≅← (ccc-3 (isCCChom h)) k) |
281 ≈⟨ iso→ (ccc-3 (isCCChom h)) ⟩ | 301 ≈⟨ iso→ (ccc-3 (isCCChom h)) ⟩ |
282 k | 302 k |
283 ∎ where open ≈-Reasoning A | 303 ∎ where open ≈-Reasoning A |
284 e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o ( <,> ( A [ k o π ] ) π' ) ] ) * ≈ k ] | 304 e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o ( <,> ( A [ k o π ] ) π' ) ] ) * ≈ k ] |
285 e4b {a} {b} {c} {k} = begin | 305 e4b {a} {b} {c} {k} = begin |
286 ( ε o ( <,> ( k o π ) π' ) ) * | 306 ( ε o ( <,> ( k o π ) π' ) ) * |
287 ≈⟨⟩ | 307 ≈⟨⟩ |
288 ≅← (ccc-3 (isCCChom h)) ( ≅→ ( ccc-3 (isCCChom h ) {_^_ h a b} {b} ) (id1 A ( _^_ h a b )) o (≅← (ccc-2 (isCCChom h)) ( k o π , π'))) | 308 ≅← (ccc-3 (isCCChom h)) ( ≅→ ( ccc-3 (isCCChom h ) {_^_ h a b} {b} ) (id1 A ( _^_ h a b )) o (≅← (ccc-2 (isCCChom h)) ( k o π , π'))) |
289 ≈⟨ {!!} ⟩ | 309 ≈⟨ cong← (ccc-3 (isCCChom h)) (nat-3 (isCCChom h)) ⟩ |
290 ≅← (ccc-3 (isCCChom h)) (≅→ (ccc-3 (isCCChom h)) k) | 310 ≅← (ccc-3 (isCCChom h)) (≅→ (ccc-3 (isCCChom h)) k) |
291 ≈⟨ iso← (ccc-3 (isCCChom h)) ⟩ | 311 ≈⟨ iso← (ccc-3 (isCCChom h)) ⟩ |
292 k | 312 k |
293 ∎ where open ≈-Reasoning A | 313 ∎ where open ≈-Reasoning A |
294 *-cong : {a b c : Obj A} {f f' : Hom A (a /\ b) c} → A [ f ≈ f' ] → A [ f * ≈ f' * ] | 314 *-cong : {a b c : Obj A} {f f' : Hom A (a /\ b) c} → A [ f ≈ f' ] → A [ f * ≈ f' * ] |