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 --exact-split --safe #-}

module Sets where 

open import SpartanMLTT

isProp : {i : 𝕃}  𝕌 i  𝕌 i
isProp X = (x y : X)  x  y

∅-is-prop : isProp 
∅-is-prop x y = unique-from-∅ x

𝟙-is-prop : isProp 𝟙
𝟙-is-prop * * = refl

isSet : U  U
isSet X = {x y : X}  isProp(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)

set-is-path-collapsible : {X : U}  isSet X  path-collapsible X
set-is-path-collapsible u = (id , u)

path-collapsible-is-set : {X : U}  path-collapsible X  isSet X
path-collapsible-is-set {X} pc p q = claim₂
 where
  f : {x y : X}  x  y  x  y
  f = pr₁ pc
  g : {x y : X} (p q : x  y)  f p  f q
  g = pr₂ 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₁ = ap  h  trans (sym(f refl)) h) (g p q)
  claim₂ : p  q
  claim₂ = trans (trans (claim₀ p) claim₁) (sym(claim₀ q))

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

prop-is-set : {X : U}  isProp X  isSet X
prop-is-set h = path-collapsible-is-set(prop-is-path-collapsible h)

isProp-isProp : {X : U}  isProp(isProp X)
isProp-isProp {X} f g = claim₁
 where
  open import FunExt
  lemma : isSet X
  lemma = prop-is-set 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 (inl x) = inhabited-is-collapsible x
decidable-is-collapsible (inr 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-set : {X : U}  discrete X  isSet X
discrete-is-set d = path-collapsible-is-set(discrete-is-path-collapsible d)

open import Two

𝟚-is-set : isSet 𝟚
𝟚-is-set = discrete-is-set 𝟚-discrete

open import Naturals

ℕ-is-set : isSet 
ℕ-is-set = discrete-is-set ℕ-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 (inl x) φ = x
decidable-is-stable (inr u) φ = unique-from-∅(φ u)

open import FunExt

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 = ap s (claim₁ x y)

open import Injection

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

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

separated-is-set : {X : U}  separated X  isSet X
separated-is-set s = path-collapsible-is-set (separated-is-path-collapsible s) 

totally-separated-is-set : (X : U)  totally-separated X  isSet X
totally-separated-is-set X t = separated-is-set(totally-separated-is-separated X t)

\end{code}

Old proof, which is longer and uses dependent funext:

\begin{code}

totally-separated-is-set' : (X : U)  totally-separated X  isSet X
totally-separated-is-set' X t = path-collapsible-is-set h
 where
  open import FunExt
  f : {x y : X}  x  y  x  y
  f r = t p  ap p r)
  b : {x y : X} (φ γ : (p : X  𝟚)  p x  p y)  φ  γ
  b φ γ = funext p  discrete-is-set 𝟚-discrete (φ p) (γ p))
  c : {x y : X} (r s : x  y)   p  ap p r)   p  ap p s)
  c r s = b p  ap p r)  p  ap p s)
  g : {x y : X}  constant(f {x} {y})
  g r s = ap 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 = pr₁ 

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 (pr₂ t))

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

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

paths-from-is-prop : {X : U} (x : X)  isProp(paths-from x)
paths-from-is-prop x = contractible-is-prop (paths-from-is-contractible x)

\end{code}