open import 1Lab.Reflection.Marker

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 .

## 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 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