Mercurial > hg > Members > kono > Proof > category

changeset 784:f27d966939f8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add CCC hom
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 17 Apr 2019 14:47:39 +0900
parents bded2347efa4
children a67959bcd44b
files CCC.agda CCChom.agda
diffstat 2 files changed, 83 insertions(+), 60 deletions(-) [+]
line wrap: on
line diff
--- a/CCC.agda	Wed Apr 17 12:03:45 2019 +0900
+++ b/CCC.agda	Wed Apr 17 14:47:39 2019 +0900
@@ -4,69 +4,12 @@
 
 open import HomReasoning
 open import cat-utility
--- open import Data.Product renaming (_×_ to _∧_)
--- open import Category.Constructions.Product
 open  import  Relation.Binary.PropositionalEquality
 
-open Functor
-
---   ccc-1 : Hom A a 1 ≅ {*}
---   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
-  OneObj : One   -- () in Haskell ( or any one object set )
-
-OneCat : Category Level.zero Level.zero Level.zero
-OneCat = record {
-    Obj  = One ;
-    Hom = λ a b →   One  ;
-    _o_ =  λ{a} {b} {c} x y → OneObj ;
-    _≈_ =  λ x y → x ≡ y ;
-    Id  =  λ{a} → OneObj ;
-    isCategory  = record {
-            isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ;
-            identityL  = λ{a b f} → lemma {a} {b} {f} ;
-            identityR  = λ{a b f} → lemma {a} {b} {f} ;
-            o-resp-≈  = λ{a b c f g h i} _ _ →  refl ;
-            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} {f} with f
-         ... | OneObj = refl
-
-record IsoS {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (a b : Obj A) ( a' b' : Obj B )
-          :  Set ( c₁  ⊔  c₂ ⊔ ℓ ⊔  c₁'  ⊔  c₂' ⊔ ℓ' ) where
-      field
-           ≅→ :  Hom A a b   → Hom B a' b'
-           ≅← :  Hom B a' b' → Hom A a b
-           iso→  : {f : Hom B a' b' }  → B [ ≅→ ( ≅← f) ≈ f ]
-           iso←  : {f : Hom A a b }    → A [ ≅← ( ≅→ f) ≈ f ]
-
-
-record IsCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (１ : Obj A) ( _×_ : {a b c : Obj A ) → Hom A c a  → Hom A c b → Hom A (a * b) )
-          ( _*_ : 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-2 : {a b c : Obj A} →  --  Hom A c ( a * b ) ≅ ( Hom A c a ) * ( Hom A c b )
-                          IsoS A A 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
-        
-        
-record CCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
-     field
-       one : Obj A
-       _*_ : Obj A → Obj A → Obj A
-       _^_ : Obj A → Obj A → Obj A  
-       _×_ : Obj A → Obj A → Obj A  
-       isCCC : IsCCC A one _×_  _*_ _^_
 
 open import HomReasoning 
 
-record IsEqCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
+record IsCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
          ( １ : Obj A )
          ( ○ : (a : Obj A ) → Hom A a １ )
           ( _∧_ : Obj A → Obj A → Obj A  ) 
@@ -118,7 +61,7 @@
      _×_ :  {  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 )
      f × g  = λ h →  < A [ f o A [ π o h  ] ] , A [ g o A [ π' o h ] ] >
 
-record EqCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
+record CCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
      field
          １ : Obj A 
          ○ : (a : Obj A ) → Hom A a １ 
@@ -129,7 +72,7 @@
          _<=_ : (a b : Obj A ) → Obj A 
          _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b) 
          ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a 
-         isEqCCC : IsEqCCC A １ ○ _∧_ <_,_> π π' _<=_ _* ε 
+         isCCC : IsCCC A １ ○ _∧_ <_,_> π π' _<=_ _* ε 
 
 
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CCChom.agda	Wed Apr 17 14:47:39 2019 +0900
@@ -0,0 +1,80 @@
+open import Level
+open import Category 
+module CCChom where
+
+open import HomReasoning
+open import cat-utility
+open import Data.Product renaming (_×_ to _∧_)
+open import Category.Constructions.Product
+open  import  Relation.Binary.PropositionalEquality
+
+open Functor
+
+--   ccc-1 : Hom A a 1 ≅ {*}
+--   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
+  OneObj : One   -- () in Haskell ( or any one object set )
+
+OneCat : Category Level.zero Level.zero Level.zero
+OneCat = record {
+    Obj  = One ;
+    Hom = λ a b →   One  ;
+    _o_ =  λ{a} {b} {c} x y → OneObj ;
+    _≈_ =  λ x y → x ≡ y ;
+    Id  =  λ{a} → OneObj ;
+    isCategory  = record {
+            isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ;
+            identityL  = λ{a b f} → lemma {a} {b} {f} ;
+            identityR  = λ{a b f} → lemma {a} {b} {f} ;
+            o-resp-≈  = λ{a b c f g h i} _ _ →  refl ;
+            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} {f} with f
+         ... | OneObj = refl
+
+record IsoS {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (a b : Obj A) ( a' b' : Obj B )
+          :  Set ( c₁  ⊔  c₂ ⊔ ℓ ⊔  c₁'  ⊔  c₂' ⊔ ℓ' ) where
+      field
+           ≅→ :  Hom A a b   → Hom B a' b'
+           ≅← :  Hom B a' b' → Hom A a b
+           iso→  : {f : Hom B a' b' }  → B [ ≅→ ( ≅← f) ≈ f ]
+           iso←  : {f : Hom A a b }    → A [ ≅← ( ≅→ f) ≈ f ]
+
+
+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-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
+                          IsoS A A  a (c ^ b) (a * b) c
+        
+        
+record CCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
+     field
+       one : Obj A
+       _*_ : Obj A → Obj A → Obj A
+       _^_ : Obj A → Obj A → Obj A  
+       isCCChom : IsCCChom A one   _*_ _^_
+
+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
+     ; _*_ = CCC._∧_ c 
+     ; _^_ = CCC._<=_ c
+     ; isCCChom = record {
+            ccc-1 = {!!}
+          ; ccc-2 = {!!}
+          ; ccc-3 = {!!}
+        }
+   }