Martin Escardo Feb 2013.

Some of this is based on work with Altenkirch, Coquand, Escardo and
Kraus 2012-2013. See http://www.cs.bham.ac.uk/~mhe/GeneralizedHedberg/html/GeneralizedHedberg.html.

\begin{code}

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

module HSets where

open import SetsAndFunctions
open import Equality

U = Set

hprop : U → U
hprop X = (x y : X) → x ≡ y

∅-is-hprop : hprop ∅
∅-is-hprop x y = unique-from-∅ x

𝟙-is-hprop : hprop 𝟙
𝟙-is-hprop * * = refl

hset : U → U
hset X = {x y : X} → hprop(x ≡ y)

constant : {X Y : U} → (f : X → Y) → U
constant {X} {Y} f = (x y : X) → f x ≡ f y

collapsible : U → U
collapsible X = Σ \(f : X → X) → constant f

path-collapsible : U → U
path-collapsible X = {x y : X} → collapsible(x ≡ y)

hset-is-path-collapsible : {X : U} → hset X → path-collapsible X
hset-is-path-collapsible u = (id , u)

path-collapsible-is-hset : {X : U} → path-collapsible X → hset X
path-collapsible-is-hset {X} pc p q = claim₂
where
f : {x y : X} → x ≡ y → x ≡ y
f = π₀ pc
g : {x y : X} (p q : x ≡ y) → f p ≡ f q
g = π₁ pc
claim₀ : {x y : X} (r : x ≡ y) → r ≡ trans (sym(f refl)) (f r)
claim₀ = J (λ x y r → r ≡ trans (sym(f refl)) (f r)) (λ x → sym-is-inverse(f refl))
claim₁ : trans (sym (f refl)) (f p) ≡ trans (sym(f refl)) (f q)
claim₁ = cong (λ h → trans (sym(f refl)) h) (g p q)
claim₂ : p ≡ q
claim₂ = trans (trans (claim₀ p) claim₁) (sym(claim₀ q))

hprop-is-path-collapsible : {X : U} → hprop X → path-collapsible X
hprop-is-path-collapsible h {x} {y} = ((λ p → h x y) , (λ p q → refl))

hprop-is-hset : {X : U} → hprop X → hset X
hprop-is-hset h = path-collapsible-is-hset(hprop-is-path-collapsible h)

hprop-hprop : {X : U} → hprop(hprop X)
hprop-hprop {X} f g = claim₁
where
open import Extensionality
lemma : hset X
lemma = hprop-is-hset f
claim : (x y : X) → f x y ≡ g x y
claim x y = lemma (f x y) (g x y)
claim₀ : (x : X) → f x ≡ g x
claim₀ x = funext (claim x)
claim₁ : f ≡ g
claim₁  = funext claim₀

∅-is-collapsible : collapsible ∅
∅-is-collapsible = (λ x → x) , (λ x → λ ())

inhabited-is-collapsible : {X : U} → X → collapsible X
inhabited-is-collapsible x = ((λ y → x) , λ y y' → refl)

empty : U → U
empty X = X → ∅

empty-is-collapsible : {X : U} → empty X → collapsible X
empty-is-collapsible u = (id , (λ x x' → unique-from-∅(u x)))

∅-is-collapsible-as-a-particular-case : collapsible ∅
∅-is-collapsible-as-a-particular-case = empty-is-collapsible id

open import DecidableAndDetachable

decidable-is-collapsible : {X : U} → decidable X → collapsible X
decidable-is-collapsible (in₀ x) = inhabited-is-collapsible x
decidable-is-collapsible (in₁ u) = empty-is-collapsible u

open import DiscreteAndSeparated

discrete-is-path-collapsible : {X : U} → discrete X → path-collapsible X
discrete-is-path-collapsible d = decidable-is-collapsible (d _ _)

discrete-is-hset : {X : U} → discrete X → hset X
discrete-is-hset d = path-collapsible-is-hset(discrete-is-path-collapsible d)

open import Two

₂-hset : hset ₂
₂-hset = discrete-is-hset ₂-discrete

open import Naturals

ℕ-hset : hset ℕ
ℕ-hset = discrete-is-hset ℕ-discrete

nonempty : U → U
nonempty X = empty(empty X)

stable : U → U
stable X = nonempty X → X

decidable-is-stable : {X : U} → decidable X → stable X
decidable-is-stable (in₀ x) φ = x
decidable-is-stable (in₁ u) φ = unique-from-∅(φ u)

open import Extensionality

stable-is-collapsible : {X : U} → stable X → collapsible X
stable-is-collapsible {X} s = (f , g)
where
f : X → X
f x = s(λ u → u x)
claim₀ : (x y : X) → (u : empty X) → u x ≡ u y
claim₀ x y u = unique-from-∅(u x)
claim₁ : (x y : X) → (λ u → u x) ≡ (λ u → u y)
claim₁ x y = funext(claim₀ x y)
g : (x y : X) → f x ≡ f y
g x y = cong s (claim₁ x y)

open import Injection

subtype-of-hset-is-hset : {X Y : U} (m : X → Y) → left-cancellable m → hset Y → hset X
subtype-of-hset-is-hset {X} m i h = path-collapsible-is-hset (f , g)
where
f : {x x' : X} → x ≡ x' → x ≡ x'
f r = i(cong m r)
g : {x x' : X} (r s : x ≡ x') → f r ≡ f s
g r s = cong i (h (cong m r) (cong m s))

separated-is-path-collapsible : {X : U} → separated X → path-collapsible X
separated-is-path-collapsible s = stable-is-collapsible(s _ _)

separated-is-hset : {X : U} → separated X → hset X
separated-is-hset s = path-collapsible-is-hset (separated-is-path-collapsible s)

totally-separated-is-hset : (X : U) → totally-separated X → hset X
totally-separated-is-hset X t = separated-is-hset(totally-separated-is-separated X t)

\end{code}

Old proof, which is longer and uses dependent funext:

\begin{code}

totally-separated-is-hset' : (X : U) → totally-separated X → hset X
totally-separated-is-hset' X t = path-collapsible-is-hset h
where
open import Extensionality
f : {x y : X} → x ≡ y → x ≡ y
f r = t(λ p → cong p r)
b : {x y : X} (φ γ : (p : X → ₂) → p x ≡ p y) → φ ≡ γ
b φ γ = funext(λ p → discrete-is-hset ₂-discrete (φ p) (γ p))
c : {x y : X} (r s : x ≡ y) → (λ p → cong p r) ≡ (λ p → cong p s)
c r s = b(λ p → cong p r) (λ p → cong p s)
g : {x y : X} → constant(f {x} {y})
g r s = cong t (c r s)
h : path-collapsible X
h {x} {y} = f , g

\end{code}

\begin{code}

contractible : U → U
contractible X = Σ \(x : X) → (y : X) → x ≡ y

paths-from : {X : U} (x : X) → U
paths-from {X} x = Σ \(y : X) → x ≡ y

end-point : {X : U} {x : X} → paths-from x → X
end-point = π₀

trivial-loop : {X : U} (x : X) → paths-from x
trivial-loop x = (x , refl)

path-from-trivial-loop : {X : U} {x x' : X} (r : x ≡ x') → trivial-loop x ≡ (x' , r)
path-from-trivial-loop {X} = J {X} A (λ x → refl)
where
A : (x x' : X) → x ≡ x' → U
A x x' r = _≡_ {Σ \(x' : X) → x ≡ x'} (trivial-loop x) (x' , r)

paths-from-is-contractible : {X : U} (x₀ : X) → contractible(paths-from x₀)
paths-from-is-contractible x₀ = trivial-loop x₀ , (λ t → path-from-trivial-loop (π₁ t))

contractible-is-hprop : {X : U} → contractible X → hprop X
contractible-is-hprop (x , f) y z = trans (sym(f y)) (f z)

inhabited-hprop-is-contractible : {X : U} → X → hprop X → contractible X
inhabited-hprop-is-contractible x h = x , h x

paths-from-is-hprop : {X : U} (x : X) → hprop(paths-from x)
paths-from-is-hprop x = contractible-is-hprop (paths-from-is-contractible x)

\end{code}