open import Cat.CartesianClosed.Locally
open import Cat.Instances.Sets.Complete
open import Cat.Functor.Pullback
open import Cat.Functor.Adjoint
open import Cat.Instances.Slice
open import Cat.Prelude

module Cat.Instances.Sets.CartesianClosed {β„“} where

Sets is (locally) cartesian closedπŸ”—

We show that the category of Sets is locally cartesian closed, i.e. that every map f:Aβ†’Bf : A \to B of Sets induces a functor ∏f:Sets/Aβ†’Sets/B\prod_f : \sets/A \to \sets/B, which is right adjoint to the base change functor fβˆ—:Sets/Bβ†’Sets/Af^* : \sets/B \to \sets/A.

⚠️⚠️⚠️

module _ {A B : Set β„“} (func : ∣ A ∣ β†’ ∣ B ∣) where
  Sets-Ξ  : Functor (Slice (Sets β„“) A) (Slice (Sets β„“) B)
  Sets-Ξ  .Fβ‚€ ob .domain =
      (Ξ£[ y ∈ ∣ B ∣ ] ((f : fibre func y) β†’ fibre (ob .map) (f .fst)))
    , Ξ£-is-hlevel 2 (B .is-tr) Ξ» _ β†’
      Ξ -is-hlevel 2 Ξ» _ β†’
      Σ-is-hlevel 2 (ob .domain .is-tr) λ _ → is-prop→is-set (A .is-tr _ _)

  Sets-Ξ  .Fβ‚€ ob .map g = g .fst

  Sets-Ξ  .F₁ hom .map (i , fibs) = i , go where
    go : βˆ€ _ β†’ _
    go (x , fx=i) = hom .map (fibs (x , fx=i) .fst) ,
      happly (hom .commutes) _ βˆ™ (fibs (x , fx=i) .snd)
  Sets-Ξ  .F₁ hom .commutes = refl
open is-lcc
Sets-lcc : is-lcc (Sets β„“)
Sets-lcc .finitely-complete = Sets-finitely-complete
Sets-lcc .Ξ f = Sets-Ξ 
Sets-lcc .f*⊣Πf f .unit .Ξ· x .map y = x .map y , Ξ» f β†’ (_ , _ , sym (f .snd)) , refl
Sets-lcc .f*⊣Πf f .counit .η x .map ((a , g) , b , p) = g (b , sym p) .fst