What is the purpose of Hedberg's Theorem?

[mrakgr]

Hedberg : {X : 𝓤 ̇ } (x : X)
        → ((y : X) → collapsible (x ≡ y))
        → (y : X) → is-subsingleton (x ≡ y)
Hedberg {𝓤} {X} x c y p q =
 p                       ≡⟨ a y p ⟩
 f x (refl x)⁻¹ ∙ f y p  ≡⟨ ap (λ - → (f x (refl x))⁻¹ ∙ -) (κ y p q) ⟩
 f x (refl x)⁻¹ ∙ f y q  ≡⟨ (a y q)⁻¹ ⟩
 q                       ∎
 where
  f : (y : X) → x ≡ y → x ≡ y
  f y = collapser (x ≡ y) (c y)
  κ : (y : X) (p q : x ≡ y) → f y p ≡ f y q
  κ y = collapser-wconstancy (x ≡ y) (c y)
  a : (y : X) (p : x ≡ y) → p ≡ (f x (refl x))⁻¹ ∙ f y p
  a x (refl x) = (⁻¹-left∙ (f x (refl x)))⁻¹

The above is quite difficult to understand, so I decided to play with it in Agda in order to gain a deepen my understanding. I tried proving it myself and here is the first thing I tried.

Hedberg' : {X : 𝓤 ̇ } (x : X)
        → ((y : X) → collapsible (x ≡ y))
        → (y : X) → is-subsingleton (x ≡ y)
Hedberg' {𝓤} {X} x c .x (refl .x) (refl .x) = refl (refl x)

It typechecks. Is there something wrong with proving it like this instead?

[mrakgr]

{-# OPTIONS --without-K --exact-split --safe #-}

Ah, actually I completely forgot about the options the book sets at the beginning. Sorry about this. It slipped my mind that the separate file I am using that imports the book does not set them.

[mrakgr]

I guess I should be asking what axiom K does exactly instead.

[martinescardo]

It makes the identity type to have at most one element. To see how this affects pattern matching, I recommend you have a look at the paper by Jesper Cockx that I link from my notes. In practice, when you have without-K, some pattern maching on refl is disallowed, when it amounts to using the K rule,

[mrakgr]

Today I ended up studying the proof the whole day. This is one of those things which seemed incredibly obtuse at first glance, but now that I've looked at it from various angles I see that it is nothing.

I did some renaming to make the proof flow more easily.

idᵃ⁻ᵇ : 𝓤 ̇ → 𝓤 ̇
idᵃ⁻ᵇ X = Σ \(id : X → X) → ∀ (a b : X) → id a ≡ id b

-- Extractor for the id field
idᵃ⁻ᵇ→id : (X : 𝓤 ̇ ) → idᵃ⁻ᵇ X → _
idᵃ⁻ᵇ→id X (id , idᵃ≡idᵇ) = id

-- Extractor for the idᵃ≡idᵇ field
idᵃ⁻ᵇ→idᵃ≡idᵇ : (X : 𝓤 ̇ ) (c : idᵃ⁻ᵇ X) → _
idᵃ⁻ᵇ→idᵃ≡idᵇ X (id , idᵃ≡idᵇ) = idᵃ≡idᵇ

Hedberg' : {X : 𝓤 ̇ } (x : X)
        → ((y : X) → idᵃ⁻ᵇ (x ≡ y))
        → (y : X) → is-subsingleton (x ≡ y)
Hedberg' {𝓤} {X} x y→idᵃ⁻ᵇ y a b =
  a                       ≡⟨ eq-id-decompose a ⟩
  id' (refl x)⁻¹ ∙ id' a  ≡⟨ ap ((id' (refl x))⁻¹ ∙_) (idᵃ≡idᵇ a b) ⟩
  id' (refl x)⁻¹ ∙ id' b  ≡⟨ (eq-id-decompose b)⁻¹ ⟩
  b                       ∎
  where
   id' : {y : X} → x ≡ y → x ≡ y
   id' {y} = idᵃ⁻ᵇ→id (x ≡ y) (y→idᵃ⁻ᵇ y)
   idᵃ≡idᵇ : {y : X} (a b : x ≡ y) → id' a ≡ id' b
   idᵃ≡idᵇ {y} = idᵃ⁻ᵇ→idᵃ≡idᵇ (x ≡ y) (y→idᵃ⁻ᵇ y)
   eq-id-decompose : {y : X} (a : x ≡ y) → a ≡ (id' (refl x))⁻¹ ∙ id' a
   eq-id-decompose {x} (refl x) = (⁻¹-left∙ (id' (refl x)))⁻¹

A decent heuristic for naming variables when there are more than just a few is to use names that allude to their intended functionality. Agda is good at this due to its support for Unicode. I would not be able to use this naming convention in any other language.

I feel like this refactor makes the proof significantly clearer. If you agree, please feel free to use this.

Edit: Changed idᵃ⁻ᵇ-id to idᵃ⁻ᵇ→id, and idᵃ⁻ᵇ-idᵃ≡idᵇ to idᵃ⁻ᵇ→idᵃ≡idᵇ.