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