Martin Escardo, 1st April 2013

Recall that a type is called collapsible if it has a weakly constant
endomap. If every type is collapsible then every type has decidable
equality and hence is a set by Hedberg's Theorem, and global hoice
holds, because collapsible types have split support.

\begin{code}

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

module Various.NonCollapsibleFamily where

open import MLTT.Spartan
open import UF.Base
open import UF.DiscreteAndSeparated
open import UF.Hedberg
open import UF.KrausLemma
open import UF.Subsingletons

decidable-equality-criterion : (X : ๐ค ฬ )
(a : ๐ โ X)
โ ((x : X) โ collapsible (ฮฃ i ๊ ๐ , a i ๏ผ x))
โ is-decidable(a โ ๏ผ a โ)
decidable-equality-criterion {๐ค} X a c = equal-or-different
where
ฮบ : (x : X) โ (ฮฃ i ๊ ๐ , a i ๏ผ x) โ ฮฃ i ๊ ๐ , a i ๏ผ x
ฮบ x = prโ(c x)

ฮบ-constant : (x : X) โ wconstant(ฮบ x)
ฮบ-constant x = prโ(c x)

prop-fix : (x : X) โ is-prop (fix(ฮบ x))
prop-fix x = fix-is-prop (ฮบ x) (ฮบ-constant x)

choice : (x : X) โ fix(ฮบ x) โ ฮฃ i ๊ ๐ , a i ๏ผ x
choice x = prโ

ฮท : (x : X) โ (ฮฃ i ๊ ๐ , a i ๏ผ x) โ fix(ฮบ x)
ฮท x ฯ = ฮบ x ฯ , ฮบ-constant x ฯ (ฮบ x ฯ)

E : ๐ค ฬ
E = ฮฃ x ๊ X , fix(ฮบ x)

r : ๐ โ E
r i = a i , ฮท (a i) (i , refl)

r-splits : (e : E) โ ฮฃ i ๊ ๐ , r i ๏ผ e
r-splits (x , p) = prโ p' , to-ฮฃ-๏ผ (prโ p' , prop-fix x _ p)
where
p' : ฮฃ i ๊ ๐ , a i ๏ผ x
p' = choice x p

s : E โ ๐
s e = prโ(r-splits e)

r-retract : (e : E) โ r(s e) ๏ผ e
r-retract e = prโ(r-splits e)

s-injective : (e e' : E) โ s e ๏ผ s e' โ e ๏ผ e'
s-injective e e' p = (r-retract e)โปยน โ ap r p โ r-retract e'

a-r : (i j : ๐) โ a i ๏ผ a j โ r i ๏ผ r j
a-r i j p = to-ฮฃ-๏ผ (p , prop-fix (a j) _ (ฮท (a j) (j , refl)))

r-a : (i j : ๐) โ r i ๏ผ r j โ a i ๏ผ a j
r-a i j = ap prโ

a-s : (i j : ๐) โ a i ๏ผ a j โ s(r i) ๏ผ s(r j)
a-s i j p = ap s (a-r i j p)

s-a : (i j : ๐) โ s(r i) ๏ผ s(r j) โ a i ๏ผ a j
s-a i j p = r-a i j (s-injective (r i) (r j) p)

equal-or-different : (a โ ๏ผ a โ) + (a โ ๏ผ a โ โ ๐)
equal-or-different = claim(๐-is-discrete (s(r โ)) (s(r โ)))
where
claim : (s(r โ) ๏ผ s(r โ)) + (s(r โ) ๏ผ s(r โ) โ ๐) โ (a โ ๏ผ a โ) + (a โ ๏ผ a โ โ ๐)
claim (inl p) = inl (s-a โ โ p)
claim (inr u) = inr (ฮป p โ u (a-s โ โ p))

\end{code}