Mercurial > hg > Members > kono > Proof > category

changeset 789:4e1e2f7199c8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
files CCC.agda CCChom.agda
diffstat 2 files changed, 38 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/CCC.agda	Fri Apr 19 12:20:48 2019 +0900
+++ b/CCC.agda	Fri Apr 19 19:20:04 2019 +0900
@@ -44,6 +44,14 @@
         ≈⟨ e2 (○ b o f) ⟩
            ○ a
         ∎
+     π-id : {a b : Obj A} → A [ < π ,  π' >  ≈ id1 A (a ∧ b ) ]
+     π-id {a} {b} = let open  ≈-Reasoning A in begin
+           < π ,  π' > 
+        ≈↑⟨ π-cong idR idR  ⟩
+          < π o id1 A (a ∧ b)  ,  π'  o id1 A (a ∧ b) >
+        ≈⟨ e3c ⟩
+          id1 A (a ∧ b )
+        ∎
      distr : {a b c d : Obj A} {f : Hom A c a }{g : Hom A c b } {h : Hom A d c } → A [ A [ < f , g > o h ]  ≈  < A [ f o h ] , A [ g o h ] > ]
      distr {a} {b} {c} {d} {f} {g} {h} = let open  ≈-Reasoning A in begin
             < f , g > o h
--- a/CCChom.agda	Fri Apr 19 12:20:48 2019 +0900
+++ b/CCChom.agda	Fri Apr 19 19:20:04 2019 +0900
@@ -58,6 +58,9 @@
                           IsoS A A  a (c ^ b) (a * b) c
        nat-2 : {a b c  : Obj A} → {f : Hom A (b * c) (b * c) } → {g : Hom A a (b * c) }
                  → (A × A) [ (A × A) [ IsoS.≅→ ccc-2 f o (g , g) ] ≈  IsoS.≅→ ccc-2 ( A [ f o g ] ) ]
+       nat-3 : {a b c : Obj A} → { k : Hom A c (a ^ b ) } → A [ A [  IsoS.≅→ (ccc-3) (id1 A (a ^ b)) o
+                    (IsoS.≅← (ccc-2 ) (A [ k o (proj₁ ( IsoS.≅→ ccc-2  (id1 A (c *  b)))) ] ,
+                        (proj₂ ( IsoS.≅→ ccc-2  (id1 A (c *  b) ))))) ] ≈ IsoS.≅→ (ccc-3 ) k ]
 
 open import CCC
 
@@ -80,7 +83,7 @@
             ccc-1 =  λ {a} {b} {c'} → record {   ≅→ =  c101  ; ≅← = c102  ; iso→  = c103 {a} {b} {c'} ; iso←  = c104 ; cong← = c105 ; cong→ = c106 }
           ; ccc-2 =  record {   ≅→ =  c201 ; ≅← = c202 ; iso→  = c203 ; iso←  = c204  ; cong← = c205; cong→ = c206 }
           ; ccc-3 =   record {   ≅→ =  c301 ; ≅← = c302 ; iso→  = c303 ; iso←  = c304 ; cong← = c305 ; cong→ = c306 }
-          ; nat-2 = nat-2
+          ; nat-2 = nat-2 ; nat-3 = nat-3
         }
    } where
       c101 : {a : Obj A} → Hom A a (CCC.１ c) → Hom OneCat OneObj OneObj
@@ -138,6 +141,30 @@
              ≈↑⟨ assoc ⟩
                  ( CCC.π c ) o (f o g)  
              ∎ ) , (sym-hom assoc) where open ≈-Reasoning A
+      nat-3 : {a b : Obj A} {c = c₁ : Obj A} {k : Hom A c₁ ((c CCC.<= a) b)} →
+            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)))) ]
+            ≈ c301 k ]
+      nat-3 {a} {b} { c₁} {k} =  begin
+                 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)))) 
+             ≈⟨⟩
+                  ( CCC.ε c o CCC.<_,_> c ((id1 A (CCC._<=_ c a b )) o CCC.π c) (CCC.π' c))
+                     o (CCC.<_,_> c (k o ( CCC.π c o (id1 A (CCC._∧_ c c₁ b )))) ( CCC.π' c o (id1 A (CCC._∧_ c c₁ b))))
+             ≈↑⟨ assoc ⟩
+                 (CCC.ε c) o ((  CCC.<_,_> c ((id1 A (CCC._<=_ c a b )) o CCC.π c) (CCC.π' c))
+                     o (CCC.<_,_> c (k o ( CCC.π c o (id1 A (CCC._∧_ c c₁ b )))) ( CCC.π' c o (id1 A (CCC._∧_ c c₁ b)))))
+             ≈⟨ cdr (car (IsCCC.π-cong (CCC.isCCC c ) idL refl-hom ) )   ⟩
+                 (CCC.ε c) o (  CCC.<_,_> c (CCC.π c) (CCC.π' c)
+                     o (CCC.<_,_> c (k o ( CCC.π c o (id1 A (CCC._∧_ c c₁ b )))) ( CCC.π' c o (id1 A (CCC._∧_ c c₁ b)))))
+             ≈⟨ cdr (car (IsCCC.π-id (CCC.isCCC c)))   ⟩
+                 (CCC.ε c) o ( id1 A (CCC._∧_ c ((c CCC.<= a) b) b )
+                     o (CCC.<_,_> c (k o ( CCC.π c o (id1 A (CCC._∧_ c c₁ b )))) ( CCC.π' c o (id1 A (CCC._∧_ c c₁ b)))))
+             ≈⟨ cdr ( cdr ( IsCCC.π-cong (CCC.isCCC c) (cdr idR) idR )) ⟩
+                 (CCC.ε c) o ( id1 A (CCC._∧_ c ((c CCC.<= a) b) b ) o (CCC.<_,_> c (k o ( CCC.π c )) ( CCC.π' c )))
+             ≈⟨ cdr idL  ⟩
+                 (CCC.ε c) o (CCC.<_,_> c  ( k o  (CCC.π c) ) (CCC.π' c))
+             ≈⟨⟩
+                 c301 k
+             ∎ where open ≈-Reasoning A
 
 
 
@@ -264,19 +291,12 @@
                   ≈⟨⟩
                       <,> f'  g' 
                   ∎ where open ≈-Reasoning A
-               e40 : {a c : Obj A} → { f : Hom A (_*_ h a c ) a } → A [ ≅→ (ccc-3 (isCCChom h)) (≅← (ccc-3 (isCCChom h)) f) ≈ f ]
-               e40 = iso→  (ccc-3 (isCCChom h))
-               e41 : {a c : Obj A} → { f : Hom A a (_^_ h c a )} → A [ ≅← (ccc-3 (isCCChom h)) (≅→ (ccc-3 (isCCChom h))  f) ≈ f ]
-               e41 = iso←  (ccc-3 (isCCChom h))
                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 π ) , π'))
-                  ≈⟨ {!!} ⟩
-                      ≅→ (ccc-3 (isCCChom h)) (id1 A (_^_ h a b)) o (≅← (ccc-2 (isCCChom h))
-                          (_[_o_] (A × A) ( ≅← (ccc-3 (isCCChom h)) k ,  id1 A b )  ( π  , π')))
-                  ≈⟨ {!!} ⟩
+                  ≈⟨ nat-3 (isCCChom h) ⟩
                       ≅→ (ccc-3 (isCCChom h)) (≅← (ccc-3 (isCCChom h)) k) 
                   ≈⟨ iso→  (ccc-3 (isCCChom h))  ⟩
                       k
@@ -286,7 +306,7 @@
                       ( ε o ( <,> (  k o  π  )  π' ) ) *
                   ≈⟨⟩
                      ≅← (ccc-3 (isCCChom h)) ( ≅→ ( ccc-3 (isCCChom h ) {_^_ h a b} {b} ) (id1 A ( _^_ h a b )) o (≅← (ccc-2 (isCCChom h)) ( k o  π , π'))) 
-                  ≈⟨ {!!} ⟩
+                  ≈⟨ cong← (ccc-3 (isCCChom h)) (nat-3 (isCCChom h)) ⟩
                      ≅← (ccc-3 (isCCChom h)) (≅→ (ccc-3 (isCCChom h)) k)
                   ≈⟨ iso←  (ccc-3 (isCCChom h))  ⟩
                       k