--- /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
+        
+        
+