Mention potential simplification of 2.13.1, see HoTT/HoTT#972

[mikeshulman]

[EgbertRijke]

You can show directly by induction that observational equality is an identity system. You don't need Hedberg's theorem or even propositions at all.

[mikeshulman]

I would expect that to take more space though. Is it equally concise?

[EgbertRijke]

The entire agda code is just:

Eq-ℕ : ℕ → (ℕ → UU lzero)
Eq-ℕ zero-ℕ zero-ℕ = 𝟙
Eq-ℕ zero-ℕ (succ-ℕ n) = 𝟘
Eq-ℕ (succ-ℕ m) zero-ℕ = 𝟘
Eq-ℕ (succ-ℕ m) (succ-ℕ n) = Eq-ℕ m n

refl-Eq-ℕ : (n : ℕ) → Eq-ℕ n n
refl-Eq-ℕ zero-ℕ = star
refl-Eq-ℕ (succ-ℕ n) = refl-Eq-ℕ n

path-ind-Eq-ℕ :
  {i : Level} (R : (m n : ℕ) → Eq-ℕ m n → UU i)
  ( ρ : (n : ℕ) → R n n (refl-Eq-ℕ n)) →
  ( m n : ℕ) (e : Eq-ℕ m n) → R m n e
path-ind-Eq-ℕ R ρ zero-ℕ zero-ℕ star = ρ zero-ℕ
path-ind-Eq-ℕ R ρ (succ-ℕ m) (succ-ℕ n) e =
  path-ind-Eq-ℕ
    ( λ m n e → R (succ-ℕ m) (succ-ℕ n) e)
    ( λ n → ρ (succ-ℕ n)) m n e

comp-path-ind-Eq-ℕ :
  {i : Level} (R : (m n : ℕ) → Eq-ℕ m n → UU i)
  ( ρ : (n : ℕ) → R n n (refl-Eq-ℕ n)) →
  ( n : ℕ) → Id (path-ind-Eq-ℕ R ρ n n (refl-Eq-ℕ n)) (ρ n)
comp-path-ind-Eq-ℕ R ρ zero-ℕ = refl
comp-path-ind-Eq-ℕ R ρ (succ-ℕ n) =
  comp-path-ind-Eq-ℕ
    ( λ m n e → R (succ-ℕ m) (succ-ℕ n) e)
    ( λ n → ρ (succ-ℕ n)) n

There's nothing going on except induction, so it depends on how much you would want there to be written about the induction steps.

[EgbertRijke]

Aside from this observation, which is fine to ignore, I think that Mike's pull request is good.