Hedberg's Theorem

1. Hedberg's theorem

1 Hedberg's theorem

module Lib.Hedberg where

This file shows Hedberg's theorem ; that is: if A has a decidable equality, then A is a set.

1.1 Packages imports

The imported packages can be accessed via the following links:

import Stdlib.Prelude
import Lib.FundamentalTheorem
import Lib.Prop.Levels
import Lib.Prop.Σ

1.2 Another statement of the fundamental theorem

If R is a binary relation on A such that:

each R(x, y) is a proposition ;
R is reflexive ;
R implies the identity

then R is the identity.

fundamental-theorem-id-map (A : U) (R : A → A → U) (r : (x : A) → R x x) (x y : A) (p : Path A x y) : R x y =
  J A x (λz _. R x z) (r x) y p

fundamental-theorem-id-isretr (A : U) (R : A → A → U) (H : (x y : A) → is-prop (R x y)) (rf : (x : A) → R x x) (M : (x y : A) → R x y → Path A x y)
                              (x y : A) : retract-of (R x y) (Path A x y) =
  let s : R x y → Path A x y = M x y
      r : Path A x y → R x y = fundamental-theorem-id-map A R rf x y
  in
  (s, (r, λu. H x y (r (s u)) u))

fundamental-theorem-id'' (A : U) (R : A → A → U) (H : (x y : A) → is-prop (R x y)) (r : (x : A) → R x x) (M : (x y : A) → R x y → Path A x y)
                         (x y : A) : is-equiv (Path A x y) (R x y) (fundamental-theorem-id-map A R r x y) =
  fundamental-theorem-id A (R x) x (fundamental-theorem-id-map A R r x)
    (is-contr/closed-retract (Σ A (R x)) (Σ A (λz. Path A x z)) (Sg/closed-retract A (R x) (λz. Path A x z) (fundamental-theorem-id-isretr A R H r M x)) (is-contr/Sg-path-is-contr A x)) y

fundamental-theorem-id/Equiv (A : U) (R : A → A → U) (H : (x y : A) → is-prop (R x y)) (r : (x : A) → R x x) (M : (x y : A) → R x y → Path A x y)
                             (x y : A) : Equiv (Path A x y) (R x y) =
  (fundamental-theorem-id-map A R r x y, fundamental-theorem-id'' A R H r M x y)

Consequently, A is a set: the identity on A is equivalent to a proposition.

id-rel/is-set (A : U) (R : A → A → U) (H : (x y : A) → is-prop (R x y)) (r : (x : A) → R x x) (M : (x y : A) → R x y → Path A x y) : is-set A =
  λx y. is-prop/closed-equiv (Path A x y) (R x y) (fundamental-theorem-id/Equiv A R H r M x y) (H x y)

1.3 Hedberg's theorem

We can deduce that any type with a decidable equality is a set.

hedberg/bin-rel' (A : U) (x y : A) : (Coprod (Path A x y) (neg (Path A x y))) → U = split
  inl _ → Unit
  inr _ → Empty

hedberg/bin-rel (A : U) (d : has-decidable-equality A) (x y : A) : U =
  hedberg/bin-rel' A x y (d x y)

-- hedberg/bin-rel/refl' (A : U) (d : has-decidable-equality A) (x : A) : (Coprod (Path A x x) (neg (Path A x x))) → hedberg/bin-rel A d x x = split
--   inl _ → star
--   inr f → f (refl A x)

hedberg/bin-rel/refl (A : U) (d : has-decidable-equality A) (x : A) : hedberg/bin-rel A d x x =
  ind-Coprod (Path A x x) (neg (Path A x x)) (λp. hedberg/bin-rel' A x x p)
    (λ_. star) (λf. f (refl A x)) (d x x)

hedberg/bin-rel/is-prop (A : U) (d : has-decidable-equality A) (x y : A) : is-prop (hedberg/bin-rel A d x y) =
  ind-Coprod (Path A x y) (neg (Path A x y)) (λq. is-prop (hedberg/bin-rel' A x y q))
    (λ_. Unit/is-prop)
    (λ_ z t. ex-falso (Path Empty z t) z) (d x y)

hedberg/bin-rel/id' (A : U) (d : has-decidable-equality A) (x y : A) : (q : Coprod (Path A x y) (neg (Path A x y))) → hedberg/bin-rel' A x y q → Path A x y = split
  inl p → λ_. p
  inr _ → λe. ex-falso (Path A x y) e

hedberg/bin-rel/id (A : U) (d : has-decidable-equality A) (x y : A) (r : hedberg/bin-rel A d x y) : Path A x y =
  hedberg/bin-rel/id' A d x y (d x y) r

hedberg (A : U) (d : has-decidable-equality A) : is-set A =
  id-rel/is-set A (hedberg/bin-rel A d) (hedberg/bin-rel/is-prop A d) (hedberg/bin-rel/refl A d) (hedberg/bin-rel/id A d)

Hedberg's Theorem

Table of Contents

1 Hedberg's theorem

1.1 Packages imports

1.2 Another statement of the fundamental theorem

1.3 Hedberg's theorem