open import Agda.Primitive
record Category {ℓ ℓ'} {A : Set ℓ}  : Set (lsuc ℓ ⊔ ℓ') where
  infixr 7 _∘_
  infix 5 _≅_ _⇒_
  field
    Obj : Set ℓ
    _⇒_ : Obj → Obj → Set ℓ
    _≅_ : ∀ {A B} → (f g : A ⇒ B) → Set ℓ

    id : ∀ {A} → A ⇒ A
    _∘_ : ∀ {A B C : Obj} → B ⇒ C → A ⇒ B → A ⇒ C
    idˡ : ∀ {A B} {g : A ⇒ B} → id ∘ g ≅ g 
    idʳ : ∀ {A B} {f : A ⇒ B} → f ∘ id ≅ f
    assoc : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D}
          → (h ∘ g) ∘ f ≅ h ∘ g ∘ f 



record Terminal {ℓ ℓ'} {A : Set ℓ}  : Set (lsuc ℓ ⊔ ℓ') where
  open Category ⦃...⦄
  field
    {{cat}} : Category {ℓ} {ℓ'} {A} 
    𝟙 : Obj
    term : ∀ {A : Obj} → A ⇒ 𝟙
    
    
record Cartesian {ℓ ℓ'} {A : Set ℓ}  : Set (lsuc ℓ ⊔ ℓ') where
  open Category ⦃...⦄ public
  infix 7 _×_
  field
    {{cat}} : Category {ℓ} {ℓ'} {A}
    _×_ : Obj → Obj → Obj
    ⟨_,_⟩ : ∀ {A B C : Obj} → A ⇒ B → A ⇒ C → A ⇒ B × C
    proj₁ : ∀ {A B} → A × B ⇒ A
    proj₂ : ∀ {A B} → A × B ⇒ B
    
    
record CCC {ℓ ℓ'} {A : Set ℓ}  : Set (lsuc ℓ ⊔ ℓ') where
  open Cartesian ⦃...⦄ public
  infix 6 _⟶_
  field
    {{cat}} : Cartesian {ℓ} {ℓ'} {A}
    _⟶_ : Obj → Obj → Obj
    apply : ∀ {A B : Obj} → (A ⟶ B) × A ⇒ B 
    curry : ∀ {A B C : Obj} → A × B ⇒ C → A ⇒ (B ⟶ C) 
    uncurry : ∀ {A B C : Obj} → A ⇒ B ⟶ C → A ⇒ (B × C)