Martin Escardo 2012.

Part of

 Kraus, N., EscardΓ³, M., Coquand, T., Altenkirch, T.
 Generalizations of Hedberg’s Theorem.
 In: Hasegawa, M. (eds) Typed Lambda Calculi and Applications.
 TLCA 2013. Lecture Notes in Computer Science, vol 7941.
 Springer, Berlin, Heidelberg.
 https://doi.org/10.1007/978-3-642-38946-7_14

\begin{code}

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

module UF.Hedberg where

open import MLTT.Spartan
open import UF.Base
open import UF.Sets
open import UF.Subsingletons

wconstant : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (f : X β†’ Y) β†’ 𝓀 βŠ” π“₯ Μ‡
wconstant f = βˆ€ x y β†’ f x ＝ f y

wconstant-pre-comp : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ }
                     (f : X β†’ Y) (g : Y β†’ Z)
                   β†’ wconstant f
                   β†’ wconstant (g ∘ f)
wconstant-pre-comp f g c x x' = ap g (c x x')

wconstant-post-comp : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ }
                      (f : X β†’ Y) (g : Y β†’ Z)
                    β†’ wconstant g
                    β†’ wconstant (g ∘ f)
wconstant-post-comp f g c x x' = c (f x) (f x')

collapsible : 𝓀 Μ‡ β†’ 𝓀 Μ‡
collapsible X = Ξ£ f κž‰ (X β†’ X) , wconstant f

Id-collapsible' : {X : 𝓀 Μ‡ } β†’ X β†’ 𝓀 Μ‡

Id-collapsible' x = βˆ€ {y} β†’ collapsible (x ＝ y)

Id-collapsible : 𝓀 Μ‡ β†’ 𝓀 Μ‡
Id-collapsible X = {x : X} β†’ Id-collapsible' x

h-isolated-points-are-Id-collapsible : {X : 𝓀 Μ‡ } {x : X}
                                     β†’ is-h-isolated x
                                     β†’ Id-collapsible' x
h-isolated-points-are-Id-collapsible h = id , h

sets-are-Id-collapsible : {X : 𝓀 Μ‡ } β†’ is-set X β†’ Id-collapsible X
sets-are-Id-collapsible u = (id , u)

local-hedberg : {X : 𝓀 Μ‡ } (x : X)
              β†’ ((y : X) β†’ collapsible (x ＝ y))
              β†’ (y : X) β†’ is-prop (x ＝ y)
local-hedberg {𝓀} {X} x pc y p q =
 p                    ＝⟨ c y p ⟩
 f x refl ⁻¹ βˆ™ f y p  ＝⟨ ap (Ξ» - β†’ (f x refl)⁻¹ βˆ™ -) (ΞΊ y p q) ⟩
 f x refl ⁻¹ βˆ™ f y q  ＝⟨ (c y q)⁻¹ ⟩
 q                    ∎
 where
  f : (y : X) β†’ x ＝ y β†’ x ＝ y
  f y = pr₁ (pc y)

  ΞΊ : (y : X) (p q : x ＝ y) β†’ f y p ＝ f y q
  ΞΊ y = prβ‚‚ (pc y)

  c : (y : X) (r : x ＝ y) β†’ r ＝ (f x refl)⁻¹ βˆ™ f y r
  c _ refl = sym-is-inverse (f x refl)

Id-collapsibles-are-h-isolated : {X : 𝓀 Μ‡ } (x : X)
                               β†’ Id-collapsible' x
                               β†’ is-h-isolated x
Id-collapsibles-are-h-isolated x pc {y} p q =
 local-hedberg x (Ξ» y β†’ (pr₁ (pc {y})) , (prβ‚‚ (pc {y}))) y p q

Id-collapsibles-are-sets : {X : 𝓀 Μ‡ } β†’ Id-collapsible X β†’ is-set X
Id-collapsibles-are-sets pc {x} = Id-collapsibles-are-h-isolated x pc

\end{code}

We also need the following symmetrical version of local Hedberg, which
can be proved by reduction to the above (using the fact that
collapsible types are closed under equivalence), but at this point we
don't have the machinery at our disposal (which is developed in
modules that depend on this one), and hence we prove it directly by
symmetrizing the proof.

\begin{code}

local-hedberg' : {X : 𝓀 Μ‡ } (x : X)
               β†’ ((y : X) β†’ collapsible (y ＝ x))
               β†’ (y : X) β†’ is-prop (y ＝ x)
local-hedberg' {𝓀} {X} x pc y p q =
  p                     ＝⟨ c y p ⟩
  f y p βˆ™ (f x refl)⁻¹  ＝⟨  ap (Ξ» - β†’ - βˆ™ (f x refl)⁻¹) (ΞΊ y p q) ⟩
  f y q βˆ™ (f x refl)⁻¹  ＝⟨ (c y q)⁻¹ ⟩
  q                     ∎
 where
  f : (y : X) β†’ y ＝ x β†’ y ＝ x
  f y = pr₁ (pc y)

  ΞΊ : (y : X) (p q : y ＝ x) β†’ f y p ＝ f y q
  ΞΊ y = prβ‚‚ (pc y)

  c : (y : X) (r : y ＝ x) β†’ r ＝  f y r βˆ™ (f x refl)⁻¹
  c _ refl = sym-is-inverse' (f x refl)

\end{code}

Here is an example (added some time after the pandemic, not sure
when). Any type that admits a prop-valued, reflexive and antisymmetric
relation is a set.

\begin{code}

type-with-prop-valued-refl-antisym-rel-is-set
 : {X : 𝓀 Μ‡ }
 β†’ (_≀_ : X β†’ X β†’ π“₯ Μ‡ )
 β†’ ((x y : X) β†’ is-prop (x ≀ y))
 β†’ ((x : X) β†’ x ≀ x)
 β†’ ((x y : X) β†’ x ≀ y β†’ y ≀ x β†’ x ＝ y)
 β†’ is-set X
type-with-prop-valued-refl-antisym-rel-is-set
 {𝓀} {π“₯} {X} _≀_ ≀-prop-valued ≀-refl ≀-anti = Ξ³
 where
  Ξ± : βˆ€ {x y} (l l' : x ≀ y) (m m' : y ≀ x) β†’ ≀-anti x y l m ＝ ≀-anti x y l' m'
  Ξ± {x} {y} l l' m m' = apβ‚‚ (≀-anti x y)
                            (≀-prop-valued x y l l')
                            (≀-prop-valued y x m m')

  g : βˆ€ {x y} β†’ x ＝ y β†’ x ≀ y
  g {x} p = transport (x ≀_) p (≀-refl x)

  h : βˆ€ {x y} β†’ x ＝ y β†’ y ≀ x
  h p = g (p ⁻¹)

  f : βˆ€ {x y} β†’ x ＝ y β†’ x ＝ y
  f {x} {y} p = ≀-anti x y (g p) (h p)

  ΞΊ : βˆ€ {x y} p q β†’ f {x} {y} p ＝ f {x} {y} q
  ΞΊ p q = Ξ± (g p) (g q) (h p) (h q)

  Ξ³ : is-set X
  Ξ³ = Id-collapsibles-are-sets (f , ΞΊ)

\end{code}