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 AA, the type βˆ‘(B:Set)(Aβ‰…B)\sum_{(B : \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 nn-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 AA and show that the type of β€œsets equipped with an isomorphism to AA” is contractible. For the center of contraction, as is usual, we pick AA 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 BB and an isomorphism i:A≅Bi : A \cong B, we can continuously deform AA into BB and, in the process, deform ii 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 nn-types to directly establish that (A≑B)≃(Aβ‰…B)(A \equiv B) \simeq (A \cong B):

  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)    β‰ƒβˆŽ