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
.
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
is-invertibleβis-equiv : {A B : Set β} {f : β£ A β£ β β£ B β£} β Sets.is-invertible {A} {B} f β is-equiv f is-invertibleβis-equiv x = is-isoβis-equiv $ iso x.inv (happly x.invl) (happly x.invr) where module x = Sets.is-invertible x is-equivβis-invertible : {A B : Set β} {f : β£ A β£ β β£ B β£} β is-equiv f β Sets.is-invertible {A} {B} f is-equivβis-invertible f-eqv = Sets.make-invertible (equivβinverse f-eqv) (funext (equivβcounit f-eqv)) (funext (equivβunit f-eqv))
Using univalence for 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 = trivial! q : is-left-inverse (equivβiso {A} {B}) isoβequiv q x = trivial!
We then use univalence for 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) ββ
Sets^op is also a categoryπ
import Cat.Reasoning (Sets β ^op) as Sets^op
First we show that isomorphism is invariant under ^op
.
iso-op-invariant : β {A B : Set β} β (A Sets^op.β B) β (A Sets.β B) iso-op-invariant {A} {B} = IsoβEquiv the-iso where open import Cat.Morphism open Inverses the-iso : Iso (A Sets^op.β B) (A Sets.β B) the-iso .fst i .to = i .from the-iso .fst i .from = i .to the-iso .fst i .inverses .invl = i .invl the-iso .fst i .inverses .invr = i .invr the-iso .snd .is-iso.inv i .to = i .from the-iso .snd .is-iso.inv i .from = i .to the-iso .snd .is-iso.inv i .inverses .invl = i .invl the-iso .snd .is-iso.inv i .inverses .invr = i .invr the-iso .snd .is-iso.rinv _ = refl the-iso .snd .is-iso.linv _ = refl
This fact lets us re-use the to-path
component of Sets-is-category
. Some
calculation gives us to-path-over
.
Sets^op-is-category : is-category (Sets β ^op) Sets^op-is-category .to-path = Sets-is-category .to-path β transport (ua iso-op-invariant) Sets^op-is-category .to-path-over {a} {b} p = Sets^op.β -pathp refl _ $ funext-dep Ξ» {xβ} {xβ} q β xβ β‘Λβ¨ ap (_$ xβ) p.invr β©β‘Λ p.to β p.from xβ β β‘Λβ¨ apΒ‘ Regularity.reduce! β©β‘Λ p.to β transport refl $ p.from $ transport refl xβ β β‘β¨ ap! (Ξ» i β unglue (β i) (q i)) β©β‘ p.to xβ β where module p = Sets^op._β _ p