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