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}