Mercurial > hg > Members > kono > Proof > category

changeset 779:6b4bd02efd80

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
CCC start
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 06 Oct 2018 13:42:27 +0900
parents 06388660995b
children b44c1c6ce646
files CCC.agda pullback.agda system-f.agda
diffstat 3 files changed, 41 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CCC.agda	Sat Oct 06 13:42:27 2018 +0900
@@ -0,0 +1,34 @@
+open import Level
+open import Category 
+module CCC where
+
+open import HomReasoning
+open import cat-utility
+open import Data.Product renaming (_×_ to _*_)
+
+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
+
+record _≅_ {c₁ c₂ ℓ ℓ' : Level} {A : Category c₁ c₂ ℓ} {a b : Obj A} (f : Hom A a b) (S : Set ℓ') :  Set ( c₁  ⊔  c₂ ⊔ ℓ ⊔ ℓ' ) where
+      field
+           ≅→ :  {!!}
+           ≅← :  {!!}
+           iso→  :  {!!}
+           iso←  :  {!!}
+
+data One {c : Level} : Set c where
+  OneObj : One   -- () in Haskell ( or any one object set )
+
+
+record isCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (one : 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 one  ≅ One {ℓ}
+       ccc-2 : {a b c : Obj A} → Hom A c ( a × b ) ≅ ( Hom A c a ) * ( Hom A c b )
+       ccc-3 : {a b c : Obj A} → Hom A a ( c ^ b ) ≅ Hom A ( a × b ) c
+        
+        
+
--- a/pullback.agda	Wed Sep 26 20:17:09 2018 +0900
+++ b/pullback.agda	Sat Oct 06 13:42:27 2018 +0900
@@ -320,16 +320,16 @@
 --
 --              Γu
 --            → Γj → Γk ←   
---           /   ↑   ↑    \     
--- proj j   /    |   |     \ proj k
---         /   μu|   |μu    \           Equalizer have to be independent from j and k
+--           /   ↑   ↑   \     
+-- proj j   /    |   |    \ proj k
+--         /   μu|   |μu   \           Equalizer have to be independent from j and k
 --        |      |   |      |            so we need products of Obj I and Hom I
 --        |product of Hom I |   
 --        |      ↑   ↑      |                    K u = id lim                        
---        | f(id)}   |      |                       
---        |      |   |g(Γ)  |            lim = K j -----------→ K k = lim
+--        |      }   |      |                       
+--        | f(id)|   |g(Γ)  |            lim = K j -----------→ K k = lim
 --        |      |   |      |                   |      u        |
---        \      |   |     /   proj j o e = ε j |               | ε k = proj k o e
+--         \     |   |     /   proj j o e = ε j |               | ε k = proj k o e
 --         product of Obj I       μ  u o g o e  |               | μ  u o f o e
 --        ↑                                     |               |
 --        | e = equalizer f g                   |               |
--- a/system-f.agda	Wed Sep 26 20:17:09 2018 +0900
+++ b/system-f.agda	Sat Oct 06 13:42:27 2018 +0900
@@ -27,7 +27,7 @@
 _×_ {l} U V =  {X : Set l} → (U → V → X)  → X 
  
 <_,_> : {l : Level} {U V : Set l} → U → V → (U ×  V) 
-<_,_> {l} {U} {V} u v = λ{X} → λ(x : U → V → X) → x u v
+<_,_> {l} {U} {V} u v = λ X  → λ(x : U → V → X) → x u v
 
 π1 : {l : Level} {U V : Set l} → (U ×  V) → U
 π1 {l} {U} {V}  t = t {U} (λ(x : U) → λ(y : V) → x)