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 .fst = x .Sets.to isoβequiv x .snd = is-isoβis-equiv $ iso x.from (happly x.invl) (happly x.invr) where module x = Sets._β _ x
Using univalence for -types, function extensionality and the computation rule for univalence, it is almost trivial to show that categorical isomorphisms of sets are an identity system.
Sets-is-category : is-category (Sets β) Sets-is-category .to-path i = n-ua (isoβequiv i) Sets-is-category .to-path-over p = Sets.β -pathp refl _ $ funextP Ξ» a β pathβua-pathp _ refl
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βcounit f-eqv)) (funext (equivβunit 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) ββ