### changeset 788:a3e124e36acf

nat in ccc-2
author Shinji KONO Fri, 19 Apr 2019 12:20:48 +0900 ca5eba647990 4e1e2f7199c8 CCChom.agda 1 files changed, 47 insertions(+), 27 deletions(-) [+]
line wrap: on
line diff
```--- a/CCChom.agda	Thu Apr 18 20:07:22 2019 +0900
+++ b/CCChom.agda	Fri Apr 19 12:20:48 2019 +0900
@@ -56,7 +56,11 @@
IsoS A (A × A)  c (a * b) (c , c ) (a , b )
ccc-3 : {a b c : Obj A} →  -- Hom A a ( c ^ b ) ≅ Hom A ( a * b ) c
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 ] ) ]
+
+open import CCC
+

record CCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
field
@@ -67,8 +71,6 @@

open import HomReasoning

-open import CCC
-
CCC→hom : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( c : CCC A ) → CCChom A
CCC→hom A c = record {
one = CCC.１ c
@@ -78,6 +80,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
}
} where
c101 : {a : Obj A} → Hom A a (CCC.１ c) → Hom OneCat OneObj OneObj
@@ -128,6 +131,14 @@
≈⟨ cdr ( IsCCC.π-cong (CCC.isCCC c ) (car f=g )  refl-hom)  ⟩
CCC.ε c o  CCC.<_,_> c (  g o CCC.π c ) ( CCC.π' c )
∎  where open ≈-Reasoning A
+      nat-2 :  {a b : Obj A} {c = c₁ : Obj A} {f : Hom A ((c CCC.∧ b) c₁) ((c CCC.∧ b) c₁)}
+            {g : Hom A a ((c CCC.∧ b) c₁)} → (A × A) [ (A × A) [ c201 f o g , g ] ≈ c201 (A [ f o g ]) ]
+      nat-2 {a} {b} {c₁} {f} {g} =   ( begin
+                 ( CCC.π c  o f) o g
+             ≈↑⟨ assoc ⟩
+                 ( CCC.π c ) o (f o g)
+             ∎ ) , (sym-hom assoc) where open ≈-Reasoning A
+

open CCChom
@@ -196,35 +207,16 @@
--     a -------------> b * c ------>  b
--     a -------------> b * c ------>  c
--
-               e31 : {a b c  : Obj A} → {f : Hom A ((_*_ h b) c) ((_*_ h b) c) } → {g : Hom A a ((_*_ h b) c) }
-                 → (A × A) [ (A × A) [ ≅→ (ccc-2 (isCCChom h)) f o (g , g ) ] ≈  ≅→ (ccc-2 (isCCChom h)) ( A [ f o g ] ) ]
-               e31 = {!!}
-               e30 : {a b c  : Obj A} → {g : Hom A a ((_*_ h b) c) }
-                   → (A × A) [ (A × A) [ (≅→ (ccc-2 (isCCChom h)) (id1 A ((_*_ h b) c))) o (g , g) ] ≈ (≅→ (ccc-2 (isCCChom h)) (A [ id1 A ((_*_ h b) c)  o g ] ) ) ]
-               e30 {a} {b} {c} {g} =   begin
-                    (≅→ (ccc-2 (isCCChom h)) (id1 A ((_*_ h b) c))) o (g , g)
-                  ≈⟨⟩
-                    ( π , π' ) o ( g , g )
-                  ≈⟨⟩
-                    ( _[_o_] A π  g , _[_o_] A π'  g )
-                  ≈↑⟨ cdr1 A (iso← (ccc-2 (isCCChom h)))  , cdr1 A (iso← (ccc-2 (isCCChom h)))  ⟩
-                    ( _[_o_] A (proj₁ ( ≅→ ( ccc-2 (isCCChom h ) ) (id1 A (_*_ h b c) )))  (≅← (ccc-2 (isCCChom h))((≅→ (ccc-2 (isCCChom h)))  g)) ,
-                      _[_o_] A π' (≅← (ccc-2 (isCCChom h))((≅→ (ccc-2 (isCCChom h)))  g)) )
-                  ≈⟨ {!!} ⟩
-                    ( proj₁ ((≅→ (ccc-2 (isCCChom h)))  g) ,  proj₂ ((≅→ (ccc-2 (isCCChom h)))  g) )
-                  ≈⟨⟩
-                     ≅→ (ccc-2 (isCCChom h)) g
-                  ≈↑⟨ cong→ (ccc-2 (isCCChom h)) ( idL1 A )  ⟩
-                     ≅→ (ccc-2 (isCCChom h)) (_[_o_] A ( id1 A ((_*_ h b) c))   g  )
-                  ∎ where open ≈-Reasoning (A × A)
cong-proj₁ : {a b c d  : Obj A} → { f g : Hom (A × A) ( a , b ) ( c , d ) } → (A × A) [ f ≈ g ] → A [ proj₁ f  ≈ proj₁ g ]
cong-proj₁ eq =  proj₁ eq
+               cong-proj₂ : {a b c d  : Obj A} → { f g : Hom (A × A) ( a , b ) ( c , d ) } → (A × A) [ f ≈ g ] → A [ proj₂ f  ≈ proj₂ g ]
+               cong-proj₂ eq =  proj₂ eq
e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } →  A [ A [ π o <,> f g  ] ≈ f ]
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))
-                  ≈⟨ cong-proj₁ e30 ⟩
+                  ≈⟨ cong-proj₁ (nat-2 (isCCChom h))  ⟩
proj₁ (≅→ (ccc-2 (isCCChom h)) (( id1 A ( _*_ h a  b )) o ( ≅← (ccc-2 (isCCChom h)) (f , g) ) ))
≈⟨ cong-proj₁  ( cong→ (ccc-2 (isCCChom h)) idL ) ⟩
proj₁ (≅→ (ccc-2 (isCCChom h)) ( ≅← (ccc-2 (isCCChom h)) (f , g) ))
@@ -234,9 +226,34 @@
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 = {!!}
+               e3b {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))
+                  ≈⟨ cong-proj₂ (nat-2 (isCCChom h))  ⟩
+                     proj₂ (≅→ (ccc-2 (isCCChom h)) (( id1 A ( _*_ h a  b )) o ( ≅← (ccc-2 (isCCChom h)) (f , g) ) ))
+                  ≈⟨ cong-proj₂  ( cong→ (ccc-2 (isCCChom h)) idL ) ⟩
+                     proj₂ (≅→ (ccc-2 (isCCChom h)) ( ≅← (ccc-2 (isCCChom h)) (f , g) ))
+                  ≈⟨ cong-proj₂ ( iso→ (ccc-2 (isCCChom h))) ⟩
+                     proj₂ ( f , g )
+                  ≈⟨⟩
+                    g
+                  ∎ where open ≈-Reasoning A
e3c : {a b c : Obj A} → { h : Hom A c (a /\ b) } →  A [ <,> ( A [ π o h ] ) ( A [ π' o h  ] )  ≈ h ]
-               e3c = {!!}
+               e3c {a} {b} {c} {f} = begin
+                   <,> (  π o f  ) (  π' o f   )
+                  ≈⟨⟩
+                    ≅← (ccc-2 (isCCChom h)) ( ( proj₁ (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) ))) o f
+                           , ( proj₂ (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b)))) o f )
+                  ≈⟨⟩
+                    ≅← (ccc-2 (isCCChom h)) (_[_o_] (A × A) (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) )) (f , f ) )
+                  ≈⟨ cong← (ccc-2 (isCCChom h)) (nat-2 (isCCChom h))   ⟩
+                    ≅← (ccc-2 (isCCChom h)) (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) o f  ))
+                  ≈⟨ cong← (ccc-2 (isCCChom h)) (cong→ (ccc-2 (isCCChom h)) idL ) ⟩
+                    ≅← (ccc-2 (isCCChom h)) (≅→ (ccc-2 (isCCChom h)) f )
+                  ≈⟨ iso← (ccc-2 (isCCChom h))  ⟩
+                    f
+                  ∎ where open ≈-Reasoning A
π-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 {a} {b} {c} {f} {f'} {g} {g'} eq1 eq2 = begin
<,> f  g
@@ -257,6 +274,9 @@
≈⟨⟩
≅→ (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 )  ( π  , π')))
+                  ≈⟨ {!!} ⟩
≅→ (ccc-3 (isCCChom h)) (≅← (ccc-3 (isCCChom h)) k)
≈⟨ iso→  (ccc-3 (isCCChom h))  ⟩
k```