open import Cat.Prelude module Cat.Instances.Sets where
The category of Setsπ
We prove that the category of Sets is univalent. Recall that this means that, fixing a set , the type is contractible. We first exhibit a contraction directly, using ua
, and then provide an alternative proof in terms of univalence for -types.
Direct proofπ
The direct proof is surprisingly straightforward, in particular because the heavy lifting is done by a plethora of existing lemmas: IsoβEquiv to turn an isomorphism into an equivalence, pathβua-pathp to reduce dependent paths over ua
to non-dependent paths, β
-pathp
to characterise dependent paths in _β
_
, etc.
module _ {β} where import Cat.Reasoning (Sets β) as Sets
We must first rearrange _β
_
to _β_
, for which we can use IsoβEquiv. We must then show that an isomorphism in the category of Sets is the same thing as an isomorphism of types; But the only difference between these types can be patched by happly/funext.
isoβequiv : {A B : Set β} β A Sets.β B β β£ A β£ β β£ B β£ isoβequiv x = IsoβEquiv (x.to , iso x.from (happly x.invl) (happly x.invr)) where module x = Sets._β _ x
We then fix a set and show that the type of βsets equipped with an isomorphism to β is contractible. For the center of contraction, as is usual, we pick itself and the identity isomorphism.
Sets-is-category : is-category (Sets β) Sets-is-category A = isc where isc : is-contr (Ξ£[ B β Set β ] (A Sets.β B)) isc .centre = A , Sets.id-iso
We must then show that, given some other set and an isomorphism , we can continuously deform into and, in the process, deform into the identity. But this follows from paths in sigma types, the rearranging of isomorphisms defined above, and n-ua.
isc .paths (B , isom) = Ξ£-pathp (n-ua AβB) (Sets.β -pathp refl _ (Ξ» i x β pathβua-pathp AβB {x = x} {y = isom.to x} refl i)) where module isom = Sets._β _ isom AβB : β£ A β£ β β£ B β£ AβB = isoβequiv isom
Indirect proofπ
While the proof above is fairly simple, we can give a different formulation, which might be more intuitive. Letβs start by showing that the rearrangement isoβequiv is an equivalence:
equivβiso : {A B : Set β} β β£ A β£ β β£ B β£ β A Sets.β B equivβiso (f , f-eqv) = Sets.make-iso f (equivβinverse f-eqv) (funext (equivβsection f-eqv)) (funext (equivβretraction f-eqv)) equivβiso : {A B : Set β} β (A Sets.β B) β (β£ A β£ β β£ B β£) equivβiso {A} {B} = IsoβEquiv (isoβequiv , iso equivβiso p q) where p : is-right-inverse (equivβiso {A} {B}) isoβequiv p x = Ξ£-prop-path is-equiv-is-prop refl q : is-left-inverse (equivβiso {A} {B}) isoβequiv q x = Sets.β -pathp refl refl refl
We then use univalence for -types to directly establish that :
is-categoryβ²-Sets : β {A B : Set β} β (A β‘ B) β (A Sets.β B) is-categoryβ²-Sets {A} {B} = (A β‘ B) ββ¨ n-univalence eβ»ΒΉ β©β (β£ A β£ β β£ B β£) ββ¨ equivβiso eβ»ΒΉ β©β (A Sets.β B) ββ