{-# OPTIONS --without-K --safe #-}
open import Categories.Category.Core using (Category)

-- A "canonical" presentation of cartesian closed categories.
--
-- This presentation is equivalent to the one in
-- Categories.Category.CartesianClosed but it is easier to work with
-- in some circumstances.
--
-- Here, exponentials are not defined in terms of arbitrary products,
-- but in terms of a family of "canonical" products.  Since products
-- are defined only up to isomorphism the choice of product does not
-- matter for the property of being cartesian closed, but working with
-- a fixed choice of representatives simplifies the constructions of
-- some instances of CCCs (e.g. Cats).

module Categories.Category.CartesianClosed.Canonical {o β„“ e} (π’ž : Category o β„“ e) where

open import Level using (levelOfTerm)
open import Function using (flip)

open import Categories.Category.BinaryProducts π’ž
open import Categories.Category.Cartesian π’ž using (Cartesian)
import Categories.Category.CartesianClosed π’ž as π’ž-CC
import Categories.Object.Exponential.Canonical as Exponentials
open import Categories.Object.Product π’ž
open import Categories.Object.Terminal π’ž using (Terminal)
open import Categories.Morphism.Reasoning π’ž

private
  open Category π’ž
  open HomReasoning

  variable
    A B C : Obj
    f g h : A β‡’ B

-- A (canonical) cartesian closed category is a category with all
-- (canonical) products and exponentials
--
-- This presentation is equivalent to the one in
-- Categories.Category.CartesianClosed.CartesianClosed.
record CartesianClosed : Set (levelOfTerm π’ž) where
  infixr 7 _Γ—_
  infixr 9 _^_
  infix 10 ⟨_,_⟩

  field

    -- Canonical products

    ⊀    : Obj
    _Γ—_  : Obj β†’ Obj β†’ Obj

    !     : A β‡’ ⊀
    π₁    : A Γ— B β‡’ A
    Ο€β‚‚    : A Γ— B β‡’ B
    ⟨_,_⟩ : C β‡’ A β†’ C β‡’ B β†’ C β‡’ A Γ— B

    !-unique : (f : A β‡’ ⊀) β†’ ! β‰ˆ f

    π₁-comp  : π₁ ∘ ⟨ f , g ⟩ β‰ˆ f
    Ο€β‚‚-comp  : Ο€β‚‚ ∘ ⟨ f , g ⟩ β‰ˆ g

    ⟨,⟩-unique : βˆ€ {f g} {h : C β‡’ A Γ— B} β†’
                 π₁ ∘ h β‰ˆ f β†’ Ο€β‚‚ ∘ h β‰ˆ g β†’ ⟨ f , g ⟩ β‰ˆ h

  -- The above defines canonical finite products, making π’ž cartesian.

  ⊀-terminal : Terminal
  ⊀-terminal = record { ⊀-is-terminal = record { !-unique = !-unique } }

  Γ—-product : βˆ€ {A B} β†’ Product A B
  Γ—-product {A} {B} =
    record { project₁ = π₁-comp; projectβ‚‚ = Ο€β‚‚-comp; unique = ⟨,⟩-unique }

  isCartesian : Cartesian
  isCartesian = record
    { terminal = ⊀-terminal
    ; products = record { product = Γ—-product }
    }

  open Cartesian isCartesian using (_⁂_)

  open Exponentials isCartesian using (Exponential)

  field

    -- Canonical exponentials (w.r.t. the canonical products)

    _^_   : Obj β†’ Obj β†’ Obj
    eval  : B ^ A Γ— A β‡’ B
    curry : C Γ— A β‡’ B β†’ C β‡’ B ^ A

    eval-comp  : eval ∘ (curry f ⁂ id) β‰ˆ f

    curry-unique : eval ∘ (f ⁂ id) β‰ˆ g β†’ f β‰ˆ curry g

  curry-resp-β‰ˆ : f β‰ˆ g β†’ curry f β‰ˆ curry g
  curry-resp-β‰ˆ fβ‰ˆg = curry-unique (eval-comp β—‹ fβ‰ˆg)

  -- The above defines canonical exponentials, making π’ž cartesian closed.

  ^-exponential : βˆ€ {A B} β†’ Exponential A B
  ^-exponential {A} {B} = record
    { B^A      = B ^ A
    ; eval     = eval
    ; Ξ»g       = Ξ» f β†’ curry f
    ; Ξ²        = eval-comp
    ; Ξ»-unique = curry-unique
    }

module Equivalence where
  open π’ž-CC using () renaming (CartesianClosed to CartesianClosedβ€²)

  -- The two presentations of CCCs are equivalent

  fromCanonical : CartesianClosed β†’ CartesianClosedβ€²
  fromCanonical cc = record
    { cartesian = CartesianClosed.isCartesian cc
    ; exp       = CartesianClosed.^-exponential cc
    }

  toCanonical : CartesianClosedβ€² β†’ CartesianClosed
  toCanonical cc = record
    { ⊀     = ⊀
    ; _Γ—_   = _Γ—_
    ; !     = !
    ; π₁    = π₁
    ; Ο€β‚‚    = Ο€β‚‚
    ; ⟨_,_⟩ = ⟨_,_⟩
    ; !-unique   = !-unique
    ; π₁-comp    = project₁
    ; Ο€β‚‚-comp    = projectβ‚‚
    ; ⟨,⟩-unique = unique
    ; _^_   = _^_
    ; eval  = eval
    ; curry = Ξ»g
    ; eval-comp    = Ξ²
    ; curry-unique = Ξ»-unique
    }
    where
      open CartesianClosedβ€² cc
      open BinaryProducts (Cartesian.products cartesian)
      open Terminal (Cartesian.terminal cartesian)