Mercurial > hg > Members > kono > Proof > category

changeset 785:a67959bcd44b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ccc → hom on going
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 17 Apr 2019 21:32:56 +0900
parents f27d966939f8
children 287d25c87b60
files CCC.agda CCChom.agda
diffstat 2 files changed, 97 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
--- a/CCC.agda	Wed Apr 17 14:47:39 2019 +0900
+++ b/CCC.agda	Wed Apr 17 21:32:56 2019 +0900
@@ -26,8 +26,7 @@
        e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } →  A [ A [ π o < f , g > ] ≈ f ]
        e3b : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } →  A [ A [ π' o < f , g > ] ≈ g ]
        e3c : {a b c : Obj A} → { h : Hom A c (a ∧ b) } →  A [ < A [ π o h ] , A [ π' o h  ] >  ≈ h ]
-       π-congl :  {a b c : Obj A} → { f f' : Hom A c a }{ g : Hom A c b } → A [ f ≈ f' ]  →  A [ < f , g >  ≈ < f' , g > ] 
-       π-congr :  {a b c : Obj A} → { f : Hom A c a }{ g g' : Hom A c b } → A [ g ≈ g' ]  →  A [ < f , g >  ≈ < f , g' > ] 
+       π-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' > ] 
        -- closed
        e4a : {a b c : Obj A} → { h : Hom A (c ∧ b) a } →  A [ A [ ε o < A [ (h *) o π ]  ,  π' > ] ≈ h ]
        e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } →  A [ ( A [ ε o < A [ k o  π ]  ,  π' > ] ) * ≈ k ]
@@ -49,13 +48,9 @@
             < f , g > o h
         ≈↑⟨ e3c ⟩
             < π o  < f , g > o h  , π' o  < f , g > o h  >
-        ≈⟨ π-congl assoc ⟩
-            < ( π o  < f , g > ) o h  , π' o  < f , g > o h  >
-        ≈⟨ π-congl (car e3a ) ⟩
-            < f o h  , π' o  < f , g > o h  >
-        ≈⟨ π-congr assoc ⟩
-            < f o h  , (π' o  < f , g > ) o h  >
-        ≈⟨  π-congr (car e3b ) ⟩
+        ≈⟨ π-cong assoc assoc ⟩
+            < ( π o  < f , g > ) o h  , (π' o  < f , g > ) o h  >
+        ≈⟨ π-cong (car e3a ) (car e3b) ⟩
             < f o h ,  g o h  >
         ∎
      _×_ :  {  a b c d e : Obj A } ( f : Hom A a d ) (g : Hom A b e ) ( h : Hom A c (a ∧ b) ) → Hom A c ( d ∧ e )
--- a/CCChom.agda	Wed Apr 17 14:47:39 2019 +0900
+++ b/CCChom.agda	Wed Apr 17 21:32:56 2019 +0900
@@ -14,7 +14,7 @@
 --   ccc-2 : Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b )
 --   ccc-3 : Hom A a (c ^ b) ≅ Hom A (a × b) c
 
-data One {c : Level} : Set c where
+data One  : Set where
   OneObj : One   -- () in Haskell ( or any one object set )
 
 OneCat : Category Level.zero Level.zero Level.zero
@@ -32,7 +32,7 @@
             associative  = λ{a b c d f g h } → refl 
        }
    }  where
-         lemma : {a b : One {Level.zero}} → { f : One {Level.zero}} →  OneObj ≡ f
+         lemma : {a b : One } → { f : One } →  OneObj ≡ f
          lemma {a} {b} {f} with f
          ... | OneObj = refl
 
@@ -48,8 +48,8 @@
 record IsCCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (１ : Obj A) 
           ( _*_ : Obj A → Obj A → Obj A  ) ( _^_ : Obj A → Obj A → Obj A  ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
      field
-       ccc-1 : {a : Obj A}     →  --   Hom A a １ ≅ {*}
-                          IsoS A OneCat  a １ OneObj OneObj  
+       ccc-1 : {a : Obj A} {b c : Obj OneCat}   →  --   Hom A a １ ≅ {*}
+                          IsoS A OneCat a １ b c
        ccc-2 : {a b c : Obj A} →  --  Hom A c ( a * b ) ≅ ( Hom A c a ) * ( Hom A c b )
                           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
@@ -73,8 +73,93 @@
      ; _*_ = CCC._∧_ c 
      ; _^_ = CCC._<=_ c
      ; isCCChom = record {
-            ccc-1 = {!!}
-          ; ccc-2 = {!!}
-          ; ccc-3 = {!!}
+            ccc-1 =  λ {a} {b} {c'} → record {   ≅→ =  c101  ; ≅← = c102  ; iso→  = c103 {a} {b} {c'} ; iso←  = c104 }
+          ; ccc-2 =  record {   ≅→ =  c201 ; ≅← = c202 ; iso→  = c203 ; iso←  = c204  }
+          ; ccc-3 =   record {   ≅→ =  c301 ; ≅← = c302 ; iso→  = c303 ; iso←  = c304  }
         }
-   }
+   } where
+      c101 : {a : Obj A} → Hom A a (CCC.１ c) → Hom OneCat OneObj OneObj
+      c101 _  = OneObj
+      c102 : {a : Obj A} → Hom OneCat OneObj OneObj → Hom A a (CCC.１ c)
+      c102 {a} OneObj = CCC.○ c a
+      c103 : {a : Obj A } {b c : Obj OneCat} {f : Hom OneCat b b } → _[_≈_] OneCat {b} {c} ( c101 {a} (c102 {a} f) ) f 
+      c103 {a} {OneObj} {OneObj} {OneObj} = refl
+      c104 : {a : Obj A} →  {f : Hom A a (CCC.１ c)} → A [ (c102 ( c101 f )) ≈ f ]
+      c104 {a} {f} = let  open  ≈-Reasoning A in HomReasoning.≈-Reasoning.sym A (IsCCC.e2 (CCC.isCCC c) f ) 
+      c201 :  { c₁ a b  : Obj A} → Hom A c₁ ((c CCC.∧ a) b) → Hom (A × A) (c₁ , c₁) (a , b)
+      c201 f = ( A [ CCC.π c o f ]  , A  [ CCC.π' c o f ] )
+      c202 :  { c₁ a b  : Obj A} → Hom (A × A) (c₁ , c₁) (a , b) → Hom A c₁ ((c CCC.∧ a) b)
+      c202 (f , g ) = CCC.<_,_> c f g 
+      c203 : { c₁ a b  : Obj A} → {f : Hom (A × A) (c₁ , c₁) (a , b)} → (A × A) [ (c201 ( c202 f )) ≈ f ]
+      c203 = ( IsCCC.e3a (CCC.isCCC c) , IsCCC.e3b (CCC.isCCC c))
+      c204 : { c₁ a b  : Obj A} → {f : Hom A c₁ ((c CCC.∧ a) b)} → A [ (c202 ( c201 f ))  ≈ f ]
+      c204 = IsCCC.e3c (CCC.isCCC c)
+      c301 :  { d a b  : Obj A} → Hom A a ((c CCC.<= d) b) → Hom A ((c CCC.∧ a) b) d  --   a -> d <= b  -> (a ∧ b ) -> d
+      c301 {d} {a} {b} f = A [ CCC.ε c o  CCC.<_,_> c ( A [ f o CCC.π c ] ) ( CCC.π' c )  ]
+      c302 : { d a b  : Obj A} →  Hom A ((c CCC.∧ a) b) d → Hom A a ((c CCC.<= d) b)
+      c302 f = CCC._* c f
+      c303 : { c₁ a b  : Obj A} →  {f : Hom A ((c CCC.∧ a) b) c₁} → A [  (c301 ( c302 f ))  ≈ f ]
+      c303 = IsCCC.e4a (CCC.isCCC c)
+      c304 : { c₁ a b  : Obj A} →  {f : Hom A a ((c CCC.<= c₁) b)} → A [ (c302 ( c301 f ))  ≈ f ]
+      c304 = IsCCC.e4b (CCC.isCCC c)
+
+open CCChom
+open IsCCChom
+open IsoS
+
+hom→CCC : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( h : CCChom A ) → CCC A
+hom→CCC A h = record {
+         １  = １
+       ; ○ = ○
+       ; _∧_ = _/\_
+       ; <_,_> = <,>
+       ; π = π
+       ; π' = π'
+       ; _<=_ = _<=_
+       ; _* = _*
+       ; ε = ε
+       ; isCCC = isCCC
+  } where
+         １ : Obj A 
+         １ = one h
+         ○ : (a : Obj A ) → Hom A a １ 
+         ○ a = ≅← ( ccc-1 (isCCChom h ) {_} {OneObj} {OneObj} ) OneObj
+         _/\_ : Obj A → Obj A → Obj A   
+         _/\_ a b = _*_ h a b
+         <,> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c ( a /\ b)  
+         <,> f g = ≅← ( ccc-2 (isCCChom h ) ) ( f , g )
+         π : {a b : Obj A } → Hom A (a /\ b) a 
+         π {a} {b} =  proj₁ ( ≅→ ( ccc-2 (isCCChom h ) ) (id1 A (_*_ h a b) ))
+         π' : {a b : Obj A } → Hom A (a /\ b) b  
+         π' {a} {b} =  proj₂ ( ≅→ ( ccc-2 (isCCChom h ) ) (id1 A (_*_ h a b) ))
+         _<=_ : (a b : Obj A ) → Obj A 
+         _<=_ = _^_ h
+         _* : {a b c : Obj A } → Hom A (a /\ b) c → Hom A a (c <= b) 
+         _* =  ≅← ( ccc-3 (isCCChom h ) )
+         ε : {a b : Obj A } → Hom A ((a <= b ) /\ b) a 
+         ε {a} {b} =  ≅→ ( ccc-3 (isCCChom h ) {_^_ h a b} {b} ) (id1 A ( _^_ h a b )) 
+         isCCC : CCC.IsCCC A １ ○ _/\_ <,> π π' _<=_ _* ε 
+         isCCC = record {
+               e2  = e2
+             ; e3a = e3a
+             ; e3b = e3b
+             ; e3c = e3c
+             ; π-cong = π-cong
+             ; e4a = e4a
+             ; e4b = e4b
+           } where
+               e2  : {a : Obj A} → ∀ ( f : Hom A a １ ) →  A [ f ≈ ○ a ]
+               e2 f = {!!}
+               e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } →  A [ A [ π o <,> f g  ] ≈ f ]
+               e3a = {!!}
+               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 = {!!}
+               e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } →  A [ ( A [ ε o ( <,> ( A [ k o  π ]  )  π' ) ] ) * ≈ k ]
+               e4b = {!!}
+