# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1538984907 -32400
# Node ID b44c1c6ce6461969757672b835507093d11d8e88
# Parent  6b4bd02efd80f2c4f1f379270fdda58c91a6a39a
CCC in Hom form

diff -r 6b4bd02efd80 -r b44c1c6ce646 CCC.agda
--- a/CCC.agda	Sat Oct 06 13:42:27 2018 +0900
+++ b/CCC.agda	Mon Oct 08 16:48:27 2018 +0900
@@ -4,7 +4,9 @@
 
 open import HomReasoning
 open import cat-utility
-open import Data.Product renaming (_×_ to _*_)
+open import Data.Product renaming (_×_ to _∧_)
+open import Category.Constructions.Product
+open  import  Relation.Binary.PropositionalEquality
 
 open Functor
 
@@ -12,23 +14,46 @@
 --   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
+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
-           ≅→ :  {!!}
-           ≅← :  {!!}
-           iso→  :  {!!}
-           iso←  :  {!!}
+           ≅→ :  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 ]
 
 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 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
+          ( _*_ : 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
+       ccc-1 : {a : Obj A}     →  --   Hom A a one ≅ {*}
+                          IsoS A OneCat  a one 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