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 \to B$ of Sets induces a functor $\prod_f : \sets/A \to \sets/B$ , which is right adjoint to the base change functor $f^* : \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