5 Dec 2012. MHE.

If every type has a constant endomap, then every relation has a
functional sub-relation with the same domain. This is a form of the
axiom of choice that shouldn't hold in type theory.

\begin{code} 

module ConstantChoice where

open import mini-library

Type  = Set

hprop : Type  Type
hprop X = (x y : X)  x  y

_[_] :  {X Y : Type}  (X  Y  Type)  X  Type
A [ x ] = Σ \y  A x y

sub-relation : {X Y : Type}  (X  Y  Type)  (X  Y  Type)  Type
sub-relation {X} {Y} A B = (x : X) (y : Y)  A x y  B x y

functional : {X Y : Type}  (X  Y  Type)  Type
functional {X} {Y} A = (x : X)  hprop(A [ x ])

same-domain : {X Y : Type}  (X  Y  Type)  (X  Y  Type)  Type
same-domain {X} {Y} A B = (x : X)   A [ x ]  B [ x ]

chooses : {X Y : Type}  (X  Y  Type)  (X  Y  Type)  Type
chooses A B = sub-relation A B × functional A × same-domain A B

constant : {X Y : Type}  (f : X  Y)  Type
constant {X} {Y} f = (x y : X)  f x  f y

collapsible : Type  Type
collapsible X = Σ \(f : X  X)  constant f

fix : {X : Type}  (f : X  X)  Type
fix f = Σ \x  x  f x

postulate Kraus-Lemma : {X : Type}  (f : X  X)  constant f  hprop(fix f)

postulate all-collapsible : (X : Type)  collapsible X

collapser : (X : Type)  X  X
collapser X = π₀(all-collapsible X)

collapser-constant : (X : Type)  constant(collapser X)
collapser-constant X = π₁(all-collapsible X)

functionalization : {X Y : Type}  (X  Y  Type)  (X  Y  Type)
functionalization A x y = Σ \(a : A x y)   (y , a)  collapser (A [ x ]) (y , a)

functionalization-is-subrelation : {X Y : Type}  (A : X  Y  Type)  sub-relation (functionalization A) A
functionalization-is-subrelation A x y = π₀

functionalization' : {X Y : Type} (A : X  Y  Type)  X  Type
functionalization' A x = fix(collapser(A [ x ]))

F : (X Y : Type) (A : X  Y  Type) (x : X)  functionalization A [ x ]  functionalization' A x
F _ _ _ _ (y , (a , p)) = ((y , a) , p)

G : (X Y : Type) (A : X  Y  Type) (x : X)  functionalization' A x  functionalization A [ x ] 
G _ _ _ _ ((y , a) , p) = (y , (a , p))

H : {X Y : Type} (A : X  Y  Type) (x : X)  hprop(functionalization' A x)
H A x = Kraus-Lemma (collapser(A [ x ])) (collapser-constant(A [ x ]))

functionalization-is-functional : {X Y : Type}  (A : X  Y  Type)  functional (functionalization A)
functionalization-is-functional {X} {Y} A x u v = q
 where
  p : F X Y A x u  F X Y A x v
  p = H A x (F X Y A x u) (F X Y A x v)

  q : u  v
  q = cong (G X Y A x) p

functionalization-has-same-domain : {X Y : Type}  (A : X  Y  Type)  same-domain (functionalization A) A
functionalization-has-same-domain {X} {Y} A x = f , g
 where
  f : functionalization A [ x ]  A [ x ]
  f (y , (a , p)) = (y , a)

  g :  A [ x ]  functionalization A [ x ]
  g (y , a)  = y' , (a' , p)
   where
    y' : Y
    y' = π₀(collapser (A [ x ]) (y , a))

    a' : A x y'
    a' = π₁(collapser (A [ x ]) (y , a))

    p : (y' , a')  collapser (A [ x ]) (y' , a')
    p = collapser-constant (A [ x ]) (y , a) ((y' , a'))

a-choice-theorem : {X Y : Type}  (A : X  Y  Type)  chooses (functionalization A) A
a-choice-theorem {X} {Y} A = functionalization-is-subrelation A , 
                             functionalization-is-functional A , 
                             functionalization-has-same-domain A

\end{code}

In fact, the above shows that the type (functionalization A [ x ]) is
a retract of the type (A [ x ]).

We (Altenkirch, Coquand, Kraus and myself) already knew what
follows. I am recording it here for the moment: under the above axiom
all-collapsible, hpropositional reflection is definable.

\begin{code} 

hinhabited : Type  Type
hinhabited X = fix(collapser X)

hprop-hinhabited : {X : Type}  hprop(hinhabited X)
hprop-hinhabited {X} = Kraus-Lemma (collapser X) (collapser-constant X)

η : {X : Type}  X  hinhabited X
η {X} x = (collapser X x , collapser-constant X x (collapser X x))

hinhabited-elim : {X P : Type}  hprop P  (X  P)  (hinhabited X  P)
hinhabited-elim _ f = f  π₀

\end{code}

Notice that the fact that P is an hprop is not used.

Moreover, we have, under all-collapsible:

\begin{code} 

down : {X : Type}  hinhabited X  X
down = π₀

\end{code}