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 $A\text{,}$ the type ${\sum }_{(B:\mathrm{Set})}(A\cong B)$ is contractible. We first exhibit a contraction directly, using ua, and then provide an alternative proof in terms of univalence for $n\text{-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

  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 $n\text{-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 .fst = iso→equiv
  equiv≃iso .snd = is-iso→is-equiv record where
    from   = equiv→iso
    linv f = ext λ _ → refl
    rinv f = ext λ _ → refl

We then use univalence for $n\text{-types}$ to directly establish that $(A\equiv B)\simeq (A\cong B)\text{:}$

  is-category'-Sets : ∀ {A B : Set ℓ} → (A ≡ B) ≃ (A Sets.≅ B)
  is-category'-Sets {A} {B} =
    (A ≡ B)         ≃˘⟨ n-univalence ⟩≃˘
    (∣ A ∣ ≃ ∣ B ∣) ≃˘⟨ equiv≃iso ⟩≃˘
    (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.from i .to = i .from
    the-iso .snd .is-iso.from i .from = i .to
    the-iso .snd .is-iso.from i .inverses .invl = i .invl
    the-iso .snd .is-iso.from 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 ⊙ iso-op-invariant .fst
  Sets^op-is-category .to-path-over {a} {b} p = Sets^op.≅-pathp refl _ $ ua→ λ a → sym (p.invr $ₚ a)
    where module p = Sets^op._≅_ p