open import Level
open import Category 
module CCC 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 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₂ ℓ) 
         ( １ : Obj A )
         ( ○ : (a : Obj A ) → Hom A a １ )
          ( _∧_ : Obj A → Obj A → Obj A  ) 
          ( <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b)  ) 
          ( π : {a b : Obj A } → Hom A (a ∧ b) a ) 
          ( π' : {a b : Obj A } → Hom A (a ∧ b) b ) 
          ( _<=_ : (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 )
             :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
     field
       -- cartesian
       e2  : {a : Obj A} → ∀ ( f : Hom A a １ ) →  A [ f ≈ ○ a ]
       e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } →  A [ A [ π o < f , g > ] ≈ f ]
       e3b : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } →  A [ A [ π' o < f , g > ] ≈ g ]
       e3c : {a b c : Obj A} → { h : Hom A c (a ∧ b) } →  A [ < A [ π o h ] , A [ π' o h  ] >  ≈ h ]
       π-congl :  {a b c : Obj A} → { f f' : Hom A c a }{ g : Hom A c b } → A [ f ≈ f' ]  →  A [ < f , g >  ≈ < f' , g > ] 
       π-congr :  {a b c : Obj A} → { f : Hom A c a }{ g g' : Hom A c b } → A [ g ≈ g' ]  →  A [ < f , g >  ≈ < f , g' > ] 
       -- closed
       e4a : {a b c : Obj A} → { h : Hom A (c ∧ b) a } →  A [ A [ ε o < A [ (h *) o π ]  ,  π' > ] ≈ h ]
       e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } →  A [ ( A [ ε o < A [ k o  π ]  ,  π' > ] ) * ≈ k ]

     e'2 : A [ ○ １ ≈ id1 A １ ]
     e'2 = let open  ≈-Reasoning A in begin
            ○ １
        ≈↑⟨ e2 (id1 A １ ) ⟩
           id1 A １
        ∎
     e''2 : {a b : Obj A} {f : Hom A a b } → A [ A [  ○ b o f ] ≈ ○ a ]
     e''2 {a} {b} {f} = let open  ≈-Reasoning A in begin
           ○ b o f
        ≈⟨ e2 (○ b o f) ⟩
           ○ a
        ∎
     distr : {a b c d : Obj A} {f : Hom A c a }{g : Hom A c b } {h : Hom A d c } → A [ A [ < f , g > o h ]  ≈  < A [ f o h ] , A [ g o h ] > ]
     distr {a} {b} {c} {d} {f} {g} {h} = let open  ≈-Reasoning A in begin
            < f , g > o h
        ≈↑⟨ e3c ⟩
            < π o  < f , g > o h  , π' o  < f , g > o h  >
        ≈⟨ π-congl assoc ⟩
            < ( π o  < f , g > ) o h  , π' o  < f , g > o h  >
        ≈⟨ π-congl (car e3a ) ⟩
            < f o h  , π' o  < f , g > o h  >
        ≈⟨ π-congr assoc ⟩
            < f o h  , (π' o  < f , g > ) o h  >
        ≈⟨  π-congr (car e3b ) ⟩
            < f o h ,  g o h  >
        ∎
     _×_ :  {  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
     field
         １ : Obj A 
         ○ : (a : Obj A ) → Hom A a １ 
         _∧_ : Obj A → Obj A → Obj A   
         <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b)  
         π : {a b : Obj A } → Hom A (a ∧ b) a 
         π' : {a b : Obj A } → Hom A (a ∧ b) b  
         _<=_ : (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 １ ○ _∧_ <_,_> π π' _<=_ _* ε