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

module Cat.Instances.Sets.CartesianClosed {β} where

open Functor
open /-Obj
open /-Hom
open _β£_
open _=>_


# Sets is (locally) cartesian closedπ

We show that the category of Sets is locally cartesian closed, i.e. that every map of Sets induces a functor which is right adjoint to the pullback functor

β οΈβ οΈβ οΈ

module _ {A B : Set β} (func : β£ A β£ β β£ B β£) where
Sets-Ξ  : Functor (Slice (Sets β) A) (Slice (Sets β) B)
Sets-Ξ  .Fβ ob .domain =
el! (Ξ£[ y β B ] ((f : fibre func y) β fibre (ob .map) (f .fst)))

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

  Sets-Ξ  .F-id = ext Ξ» x y β Ξ£-pathp refl
(funext Ξ» x β Ξ£-pathp refl (A .is-tr _ _ _ _))
Sets-Ξ  .F-β f g = ext Ξ» x y β Ξ£-pathp refl
(funext Ξ» x β Ξ£-pathp refl (A .is-tr _ _ _ _))

Sets-lcc : Locally-cartesian-closed (Sets β)
Sets-lcc = dependent-productβlcc (Sets β) Sets-finitely-complete Sets-Ξ  adj where
adj : β {a b : Set β} (f : β£ a β£ β β£ b β£) β Base-change _ {X = b} {Y = a} f β£ Sets-Ξ  f
adj f .unit .Ξ· x .map y = x .map y , Ξ» f β (_ , _ , sym (f .snd)) , refl
adj f .counit .Ξ· x .map ((a , g) , b , p) = g (b , sym p) .fst
adj f .unit .Ξ· x .commutes = refl
adj {a} {b} f .unit .is-natural x y g =
/-Hom-path (funext Ξ» x β Ξ£-pathp (happly (g .commutes) _)
(funext-dep (Ξ» p β Ξ£-pathp (Ξ£-pathp refl (Ξ£-pathp (Ξ» i β p i .fst)
(is-setβsquarep (Ξ» i j β b .is-tr) _ _ _ _)))
(is-setβsquarep (Ξ» i j β a .is-tr) _ _ _ _))))
adj f .counit .Ξ· x .commutes = funext Ξ» where
((a , g) , b , p) β g (b , sym p) .snd
adj {a} {b} f .counit .is-natural x y g =
/-Hom-path (funext Ξ» x β ap (g .map β fst β x .fst .snd)
(Ξ£-pathp refl (b .is-tr _ _ _ _)))
adj {a} {b} f .zig {A} =
/-Hom-path (funext Ξ» x β Ξ£-pathp refl (Ξ£-pathp refl (b .is-tr _ _ _ _)))
adj {a} {b} f .zag =
/-Hom-path (funext (Ξ» x β Ξ£-pathp refl
(funext Ξ» x β Ξ£-pathp refl (a .is-tr _ _ _ _))))