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 of Sets induces a functor , which is right adjoint to the base change 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
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