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}

Some stuff about contractibility:

\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}