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)(AB)\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 ( , 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 ,

We must then show that, given some other set BB and an isomorphism i:ABi : 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 = x} refl i))
        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)
      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 (AB)(AB)(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)    ≃∎