\import Category
\import Category.Functor
\import Category.Limit
\import Category.Product
\import Equiv
\import Function.Meta
\import Logic
\import Logic.Unique
\import Meta
\import Paths
\import Paths.Meta
\import Set.SetCategory
\open PrecatWithBprod

\class CartesianClosedPrecat \extends CartesianPrecat {
  | CHom : Ob -> Ob -> Ob
  | CHom-eval {X Y : Ob} : Hom (Bprod (CHom X Y) X) Y
  | CHom-univ {X Y Z : Ob} : IsEquiv {Hom Z (CHom X Y)} {Hom (Bprod Z X) Y} (\lam g => CHom-eval ∘ prodMap g id)

  \func curry {X Y Z : Ob} (f : Hom (Bprod Z X) Y) : Hom Z (CHom X Y)
    => IsEquiv.ret CHom-univ f

  \func uncurry {X Y Z : Ob} (g : Hom Z (CHom X Y)) : Hom (Bprod Z X) Y
    => CHom-eval ∘ prodMap g id

  \lemma curry_uncurry {X Y Z : Ob} {g : Hom Z (CHom X Y)} : curry (uncurry g) = g
    => IsEquiv.ret_f CHom-univ

  \lemma uncurry_curry {X Y Z : Ob} {f : Hom (Bprod Z X) Y} : uncurry (curry f) = f
    => IsEquiv.f_ret CHom-univ
}

\instance SetCartesianClosed.{u} : CartesianClosedPrecat (\Set u)
  | CartesianPrecat => SetBicat.{u}
  | CHom X Y => X -> Y
  | CHom-eval s => s. s.
  | CHom-univ => inP \new QEquiv {
    | ret f z x => f (z,x)
    | ret_f => idpe
    | f_sec => idpe
  }