Mercurial > hg > Members > kono > Proof > category

comparison CCChom.agda @ 793:f37f11e1b871

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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.１ c) 91 c102 : {a : Obj A} → Hom OneCat OneObj OneObj → Hom A a (CCC.１ 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.１ c)} → A [ (c102 ( c101 f )) ≈ f ] 95 c104 : {a : Obj A} → {f : Hom A a (CCC.１ 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 １ ( c ^ b ) ≅ Hom A b c
170 IsoS A A (CCC.１ 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.１ 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.１ ccc) b ) )
211 ≈↑⟨ cdr ( IsCCC.e2 (CCC.isCCC ccc) ) ⟩
212 f o ( (CCC.○ ccc) (CCC.１ ccc) o (CCC.π ccc) )
213 ≈↑⟨ cdr ( car ( IsCCC.e2 (CCC.isCCC ccc) )) ⟩
214 f o ( id1 A (CCC.１ 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.１ 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.１ 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 １ ) → A [ f ≈ ○ a ] 299 e2 : {a : Obj A} → ∀ { f : Hom A a １ } → 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 １) → Sets [ f ≈ ○ a ] 446 e2 : {a : Obj Sets} {f : Hom Sets a １} → 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} →