changeset 786:287d25c87b60

on going CCC
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 18 Apr 2019 10:00:20 +0900
parents a67959bcd44b
children ca5eba647990
files CCChom.agda
diffstat 1 files changed, 49 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/CCChom.agda	Wed Apr 17 21:32:56 2019 +0900
+++ b/CCChom.agda	Thu Apr 18 10:00:20 2019 +0900
@@ -148,18 +148,62 @@
              ; e4a = e4a
              ; e4b = e4b
            } where
+               e20 : ∀ ( f : Hom OneCat OneObj OneObj ) →  _[_≈_] OneCat {OneObj} {OneObj} f OneObj 
+               e20 OneObj = refl
                e2  : {a : Obj A} → ∀ ( f : Hom A a 1 ) →  A [ f ≈ ○ a ]
-               e2 f = {!!}
+               e2 {a} f = begin
+                     f
+                  ≈↑⟨  iso← ( ccc-1 (isCCChom h )) ⟩
+                    ≅← ( ccc-1 (isCCChom h )  {a} {OneObj} {OneObj}) (  ≅→ ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) f ) 
+                  ≈⟨  ≡-cong {Level.zero} {Level.zero} {Level.zero} {OneCat} {OneObj} {OneObj}  (
+                         λ y → ≅← ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) y ) (e20 ( ≅→ ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) f) )  ⟩
+                    ≅← ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) OneObj
+                  ≈⟨⟩
+                     ○ a
+                  ∎ where open ≈-Reasoning A
+               e30 : {a b c d e : Obj A} → { f : Hom A ((_*_ h b) c) ((_*_ h d) e)  } → {g : Hom A a ((_*_ h b) c) }
+                   → A [ A [ proj₁ (≅→ (ccc-2 (isCCChom h)) f ) o g ] ≈  proj₁ (≅→ (ccc-2 (isCCChom h)) (A [ f o g ] ) ) ]
+               e30 = {!!}
+               e31 : {a b c d e : Obj A} → {i : Hom (A × A) (b , c) (d , e )}   → { f : Hom A a b  } → {g : Hom A a c }
+                   → A [ A [ {!!} o ( ≅← (ccc-2 (isCCChom h)) (f , g) ) ] ≈  ( ≅← (ccc-2 (isCCChom h)) ( _[_o_] (A × A) i (f , g ) )) ]
+               e31 = {!!}
                e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } →  A [ A [ π o <,> f g  ] ≈ f ]
-               e3a = {!!}
+               e3a {a} {b} {c} {f} {g} =  begin
+                    π o <,> f g
+                  ≈⟨⟩
+                     proj₁ (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) )) o  (≅← (ccc-2 (isCCChom h)) (f , g))
+                  ≈⟨ e30 ⟩
+                     proj₁ (≅→ (ccc-2 (isCCChom h)) (_[_o_] A ( id1 A ( _*_ h a  b )) ( ≅← (ccc-2 (isCCChom h)) (f , g) ) ))
+                  ≈⟨ {!!} ⟩
+                     proj₁ (≅→ (ccc-2 (isCCChom h)) (≅← (ccc-2 (isCCChom h)) ( _[_o_] (A × A )  ( id1 A a , id1 A b )  (f , g)  )))
+                  ≈⟨ {!!} ⟩
+                     proj₁ ( f , g )
+                  ≈⟨⟩
+                    f 
+                  ∎ where open ≈-Reasoning A
                e3b : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } →  A [ A [ π' o <,> f g  ] ≈ g ]
                e3b = {!!}
                e3c : {a b c : Obj A} → { h : Hom A c (a /\ b) } →  A [ <,> ( A [ π o h ] ) ( A [ π' o h  ] )  ≈ h ]
                e3c = {!!}
                π-cong :  {a b c : Obj A} → { f f' : Hom A c a }{ g g' : Hom A c b } → A [ f ≈ f' ] → A [ g ≈ g' ]  →  A [ <,> f  g   ≈ <,> f'  g'  ] 
-               π-cong = {!!}
-               e4a : {a b c : Obj A} → { h : Hom A (c /\ b) a } →  A [ A [ ε o ( <,> ( A [ (h *) o π ] )   π')  ] ≈ h ]
-               e4a = {!!}
+               π-cong {a} {b} {c} {f} {f'} {g} {g'} eq1 eq2 = begin
+                      <,> f  g 
+                  ≈⟨⟩
+                       ≅← (ccc-2 (isCCChom h)) (f , g)
+                  ≈⟨ ≡-cong {!!} {!!} ⟩
+                       ≅← (ccc-2 (isCCChom h)) (f' , g')
+                  ≈⟨⟩
+                      <,> f'  g' 
+                  ∎ where open ≈-Reasoning A
+               e4a : {a b c : Obj A} → { k : Hom A (c /\ b) a } →  A [ A [ ε o ( <,> ( A [ (k *) o π ] )   π')  ] ≈ k ]
+               e4a {a} {b} {c} {k} =  begin
+                      ε o ( <,> ((k *)  o π  ) π' )
+                  ≈⟨⟩
+                      ≅→ (ccc-3 (isCCChom h)) (id1 A (_^_ h a b)) o 
+                          (≅← (ccc-2 (isCCChom h)) ((( ≅← (ccc-3 (isCCChom h)) k) o π ) , π'))
+                  ≈⟨ {!!} ⟩
+                      k
+                  ∎ where open ≈-Reasoning A
                e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } →  A [ ( A [ ε o ( <,> ( A [ k o  π ]  )  π' ) ] ) * ≈ k ]
                e4b = {!!}