30 Mar 2013. MHE.

A type is called collapsible if it has a constant endomap, where a map
is called constant if any two of its values are equal. Hence any empty
or inhabited type is collapsible, and all types are collapsible under
excluded middle.

We give an explicit counter-example to collapsibility. From any two
given elements of any type, we construct a family of types such that
if each of them has a constant endomap, then the equality of the two
elements is decidable. Because there are types that don't provably
have decidable equality, this gives an example of a family of types
that can't be provably collapsible in general. This is developed in
pure intensional MLTT.

This module should probably be called non-collapsible-family-of-types
instead. It is an open problem to produce a single type (in a context)
that cannot be proved to be collapsible.

\begin{code}

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

module non-collapsible-type where

open import mini-library
open import KrausLemma
open import decidable-and-discrete

\end{code}

The type

    (a₀ ≡ x) + (a₁ ≡ x)

cannot be collapsible for all x unless a₀ ≡ a₁ is decidable. We
represent the displayed type as Σ \(i : ₂) → a i ≡ x for convenience.

A positive way of formulating this is as follows, as a technique for
proving the decidable equality of two given elements. But at present
it is difficult to imagine a situation where this technique would be
profitably applicable.


\begin{code}

bold-proof-technique : (X : Type) → (a : ₂ → X) → ((x : X) → collapsible(Σ \(i : ₂) → a i ≡ x)) → decidable(a ₀ ≡ a ₁)
bold-proof-technique X a c = equal-or-different
 where
  κ : (x : X) → (Σ \(i : ₂) → a i ≡ x) → Σ \(i : ₂) → a i ≡ x
  κ x = π₀(c x)
  κ-constant : (x : X) → constant(κ x)
  κ-constant x = π₁(c x)

  hprop-fix : (x : X) → hprop(fix(κ x))
  hprop-fix x = Kraus-Lemma (κ x) (κ-constant x)

  choice : (x : X) → fix(κ x) → Σ \(i : ₂) → a i ≡ x
  choice x = π₀

  η : (x : X) → (Σ \(i : ₂) → a i ≡ x) → fix(κ x)
  η x σ = κ x σ , κ-constant x σ (κ x σ)

  E : Type
  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) = π₀ p' , split (a(π₀ p')) x (η (a (π₀ p')) ((π₀ p') , refl)) p (π₁ p') (hprop-fix x _ p)
   where
    p' : Σ \(i : ₂) → a i ≡ x
    p' = choice x p

  s : E → ₂
  s e = π₀(r-splits e)

  r-retract : (e : E) → r(s e) ≡ e
  r-retract e = π₁(r-splits e)

  s-injective : (e e' : E) → s e ≡ s e' → e ≡ e'
  s-injective e e' p = (r-retract e)⁻¹ • cong r p • r-retract e'

  a-r : (i j : ₂) → a i ≡ a j → r i ≡ r j
  a-r i j p = split (a i) (a j) (η (a i) (i , refl)) (η (a j) (j , refl)) p (hprop-fix (a j) _ (η (a j) (j , refl)))

  r-a : (i j : ₂) → r i ≡ r j → a i ≡ a j
  r-a i j = cong π₀

  a-s : (i j : ₂) → a i ≡ a j → s(r i) ≡ s(r j)
  a-s i j p = cong 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(₂-discrete {s(r ₀)} {s(r ₁)})
   where
    claim : (s(r ₀) ≡ s(r ₁)) + (s(r ₀) ≡ s(r ₁) → ∅) → (a ₀ ≡ a ₁) + (a ₀ ≡ a ₁ → ∅)
    claim (in₀ p) = in₀ (s-a ₀ ₁ p)
    claim (in₁ u) = in₁ (λ p → u (a-s ₀ ₁ p))

\end{code}