G e n e r a l i z a t i o n s o f H e d b e r g' s T h e o r e m
under the axioms of extensionality and/or hpropositional reflection
Thorsten Altenkirch University of Nottingham, UK
Thierry Coquand University of Gothenburg, Sweden
Martin Escardo University of Birmingham, UK
Nicolai Kraus University of Nottingham, UK
12th October 2012, last updated 29 November 2012.
Total separatedness added 16 Feb 2013 flying over the atlantic ocean.
Choice discussion added 12 Mar 2013.
This file type checks in Agda version 2.3.2
I n t r o d u c t i o n
Hedberg's Theorem says that any type with decidable equality satisfies
the uniqueness of identity proofs (UIP), or equivalently, is an hset.
We say that a type X is collapsible if there is a constant map X → X,
and that a type X is path-collapsible if the path space x ≡ y is
collapsible for all x,y: X.
We claim that the essence of Hedberg's argument is this:
(i) If a type is path-collapsible then it is an hset.
(ii) A type with decidable equality is path-collapsible.
Condition (i) also gives immediately the well-known fact that
hpropositions are hsets.
We apply this analysis of Hedberg's argument to develop two
generalizations of Hedberg's theorem, by successively weakening the
decidability hypothesis:
(1) If a type X is separated then X is path-collapsible and hence an hset.
The hypothesis means that if the path type x ≡ y is nonempty then
it is inhabited, for any two points x,y: X.
The conclusion requires the axiom of extensionality for ∅-valued
functions, where ∅ is the empty type.
(2) If a type X is hseparated then X is path-collapsible and hence an hset.
The hypothesis means that if the path type x ≡ y is hinhabited
then it is inhabited.
The proof this time doesn't rely on extensionality, but the very
formulation of this fact of course requires that hpropositional
reflections, denoted by hinhabited, exist.
Decidable equality (also known as discreteness) implies separatedness
assuming extensionality of ∅-valued functions, which in turn implies
hseparatedness. Hence in the presence of extensionality and
hpropositional reflection, (2) generalizes (1), which in turn
generalizes Hedberg's theorem.
This is as far as one can go in this sequence of weakenings of the
discreteness hypothesis in Hedberg's Theorem, because
If X is an hset then X must be hseparated.
In summary, we prove that the following are logically equivalent:
(i) X is an hset.
(ii) X is path-collapsible.
(iii) X is hseparated.
Because discreteness implies separation, which in turn implies
hseparation, Hedberg's theorem follows from this.
Generalizing part of the above, we also prove, with a non-trivial
argument, that the following are logically equivalent:
(ii') X is collapsible.
(iii') X is inhabited if it is hinhabited (we say that X is hstable).
Organization.
------------
1. Weakenings of the hypothesis of Hedberg's Theorem.
2. collapsible X ⇔ hstable X.
3. A type size reduction without resizing axioms.
4. Taboos and counter-models.
The last two sections are motivated by technical considerations
arising in the previous two, and hence we don't discuss them in this
introduction. They include some open questions.
We now proceed to the technical development.
\begin{code}
{-# OPTIONS --without-K #-}
module GeneralizedHedberg where
open import mini-library
\end{code}
-----------------------------------------------------------
-- 1. Weakenings of the hypothesis of Hedberg's Theorem. --
-----------------------------------------------------------
"x ≡ y" denotes the identity type Id X x y for some implicitly
given X. Its elements p : x ≡ y are called paths from x to y.
In Agda, "Set" means "Type", which gives a rather unfortunate clash of
terminology with Homotopy Type Theory (HoTT), where (h-)sets are taken
to be certain types, which amount to those that satisfy the uniqueness
of identity proofs (UIP), that is, of paths. To avoid terminological
conflicts, we define:
\begin{code}
Type = Set
Type₁ = Set₁
\end{code}
The following definition of hproposition is not quite the same as
Voevodsky's, but is logically and even (weakly) equivalent. An
hproposition is a type that has at most one element, or, equivalently,
such that there is a path from any point to any other point.
\begin{code}
hprop : Type → Type
hprop X = (x y : X) → x ≡ y
\end{code}
This amounts to saying that X is a subsingleton. For future
reference, notice that it also amounts to saying that the identity
function X → X is constant. Of course:
\begin{code}
∅-is-hprop : hprop ∅
∅-is-hprop x y = ∅-elim x
\end{code}
An hset amounts to a type whose path relation is an hproposition:
\begin{code}
hset : Type → Type
hset X = {x y : X} → hprop(x ≡ y)
\end{code}
We call a type X collapsible if there is a constant map X → X. The
idea is that such a map collapses X to a single point, if X has a
point, and that its image is a sub-singleton, or hproposition.
\begin{code}
constant : {X Y : Type} → (X → Y) → Type
constant {X} {Y} f = (x y : X) → f x ≡ f y
collapsible : Type → Type
collapsible X = Σ \(f : X → X) → constant f
path-collapsible : Type → Type
path-collapsible X = {x y : X} → collapsible(x ≡ y)
\end{code}
A type is an hset if and only if it is path-collapsible. One direction
is trivial and the other is rather subtle, requiring path-induction
(that is, Martin-Löf's J eliminator) with a non-obvious induction
hypothesis (claim₀).
\begin{code}
hset-is-path-collapsible : {X : Type} → hset X → path-collapsible X
hset-is-path-collapsible u = (id , u)
path-collapsible-is-hset : {X : Type} → path-collapsible X → hset X
path-collapsible-is-hset {X} pc p q = claim₂
where
f : {x y : X} → x ≡ y → x ≡ y
f = π₀ pc
g : {x y : X} (p q : x ≡ y) → f p ≡ f q
g = π₁ pc
claim₀ : {x y : X} (r : x ≡ y) → r ≡ (f refl)⁻¹ • (f r)
claim₀ = J (λ r → r ≡ ((f refl)⁻¹) • (f r)) (sym-is-inverse(f refl))
claim₁ : (f refl)⁻¹ • (f p) ≡ (f refl)⁻¹ • (f q)
claim₁ = ap (λ h → (f refl)⁻¹ • h) (g p q)
claim₂ : p ≡ q
claim₂ = (claim₀ p) • claim₁ • (claim₀ q)⁻¹
\end{code}
An immediate consequence is the well-known fact that hpropositions are
hsets:
\begin{code}
hprop-is-path-collapsible : {X : Type} → hprop X → path-collapsible X
hprop-is-path-collapsible h {x} {y} = ((λ p → h x y) , (λ p q → refl))
hprop-is-hset : {X : Type} → hprop X → hset X
hprop-is-hset h = path-collapsible-is-hset(hprop-is-path-collapsible h)
\end{code}
To arrive at Hedberg's Theorem and its generalizations discussed
above, we investigate collapsible types.
The empty type ∅ is collapsible, and any inhabited type is
collapsible.
\begin{code}
∅-is-collapsible : collapsible ∅
∅-is-collapsible = (λ x → x) , (λ x → λ ())
inhabited : Type → Type
inhabited X = X
inhabited-is-collapsible : {X : Type} → inhabited X → collapsible X
inhabited-is-collapsible x = ((λ y → x) , λ y y' → refl)
\end{code}
This suggests that under excluded-middle (EM), all types are
collapsible, and so the collapsibility of all types is a weakening of
EM. In fact, we have more than that: if a particular type is
decidable, then it is is collapsible:
\begin{code}
empty : Type → Type
empty X = inhabited(X → ∅)
empty-is-collapsible : {X : Type} → empty X → collapsible X
empty-is-collapsible u = (id , (λ x x' → ∅-elim(u x)))
∅-is-collapsible-as-a-particular-case : collapsible ∅
∅-is-collapsible-as-a-particular-case = empty-is-collapsible id
\end{code}
NB. This second inhabitant of collapsible ∅ is not definitionally the
same as the previous one. (This cannot be expressed in Agda or as a
term of MLTT - definitional equality is a meta-level concept.)
\begin{code}
decidable : Type → Type
decidable X = inhabited X + empty X
decidable-is-collapsible : {X : Type} → decidable X → collapsible X
decidable-is-collapsible (in₀ x) = inhabited-is-collapsible x
decidable-is-collapsible (in₁ u) = empty-is-collapsible u
EM : Type₁
EM = (X : Type) → decidable X
all-types-are-collapsible-under-EM : EM → (X : Type) → collapsible X
all-types-are-collapsible-under-EM em X = decidable-is-collapsible (em X)
all-types-are-hsets-under-EM : EM → (X : Type) → hset X
all-types-are-hsets-under-EM em X = path-collapsible-is-hset(λ {x} {y} → all-types-are-collapsible-under-EM em (x ≡ y))
\end{code}
In constructive mathematics a set is customarily called discrete if it
has decidable equality:
\begin{code}
discrete : Type → Type
discrete X = {x y : X} → decidable(x ≡ y)
discrete-is-path-collapsible : {X : Type} → discrete X → path-collapsible X
discrete-is-path-collapsible d = decidable-is-collapsible d
\end{code}
With the above terminology, Hedberg's Theorem is that any discrete
type is an hset:
\begin{code}
discrete-is-hset : {X : Type} → discrete X → hset X
discrete-is-hset d = path-collapsible-is-hset(discrete-is-path-collapsible d)
\end{code}
Two applications of this analysis of Hedberg's argument follow.
The first one is a generalization of Hedberg's Theorem with a caveat:
Hedberg's Theorem doesn't require function extensionality but our
"generalization" does. So it is a generalization only in the presence
of extensionality.
\begin{code}
nonempty : Type → Type
nonempty X = empty(empty X)
stable : Type → Type
stable X = nonempty X → inhabited X
decidable-is-stable : {X : Type} → decidable X → stable X
decidable-is-stable (in₀ x) φ = x
decidable-is-stable (in₁ u) φ = ∅-elim(φ u)
separated : Type → Type
separated X = {x y : X} → stable(x ≡ y)
discrete-is-separated : {X : Type} → discrete X → separated X
discrete-is-separated {X} d = decidable-is-stable d
\end{code}
The separatedness condition holds often in constructive mathematics
and its generalizations. E.g. the (Dedekind and Cauchy) reals in a
topos are separated, and so are the Cantor space and the Baire space,
but they are not discrete. In MLTT, the Cantor space and the Baire
space are separated under the assumption that any two pointwise equal
functions are equal (the axiom of function extensionality).
Extensionality for (certain) ∅-valued functions is all we use here,
and as sparsely as possible:
\begin{code}
funext : Type → Type → Type
funext X Y = {f g : X → Y} → ((x : X) → f x ≡ g x) → f ≡ g
funext-special-case₀ : Type → Type
funext-special-case₀ X = funext (empty X) ∅
stable-is-collapsible : {X : Type} → funext-special-case₀ X → stable X → collapsible X
stable-is-collapsible {X} e 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 = ∅-elim(u x)
claim₁ : (x y : X) → (λ u → u x) ≡ (λ u → u y)
claim₁ x y = e (claim₀ x y)
g : (x y : X) → f x ≡ f y
g x y = ap s (claim₁ x y)
funext-special-case₁ : Type → Type
funext-special-case₁ X = {x y : X} → funext-special-case₀(x ≡ y)
separated-is-path-collapsible : {X : Type} → funext-special-case₁ X → separated X → path-collapsible X
separated-is-path-collapsible e s = stable-is-collapsible e s
\end{code}
discrete-is-separated shows that the following is a generalization of
Hedberg's theorem under the assumption of function extensionality.
\begin{code}
separated-is-hset : {X : Type} → funext-special-case₁ X → separated X → hset X
separated-is-hset e s = path-collapsible-is-hset(separated-is-path-collapsible e s)
\end{code}
We now give a further generalization, assuming the types that are
hpropositions form a reflective subcategory of that of all types.
We define hpropositional reflection axiomatically, to avoid
impredicativity and resizing axioms, which are not available in Agda
anyway. The axiomatization is given by postulating the universal
property of the reflection, with the reflector called hinhabited. The
universal property is given by the (non-dependent) eliminator.
\begin{code}
postulate hinhabited : Type → Type
postulate hprop-hinhabited : {X : Type} → hprop(hinhabited X)
postulate η : {X : Type} → X → hinhabited X
postulate hinhabited-elim : (X P : Type) → hprop P → (X → P) → (hinhabited X → P)
postulate hinhabited-ind : {X : Type} {P : hinhabited X → Type} → ((s : hinhabited X) → hprop(P s)) → ((x : X) → P (η x)) → (s : hinhabited X) → P s
\end{code}
Assuming function extensionality, the reflection diagram
η {X}
X -------> hinhabited X
\ .
\ .
\ . _ _
∀ g \ . ∃! g (namely g = hinhabited-elim X P f g)
\ .
\ .
\ .
v v
P
commmutes because any two hprop-valued maps are equal by function
extensionality. Moreover, the "extension" of g : X → P to a map
hinhabited X → P is unique for the same reason.
Voevodsky constructs the hpropositional reflection as follows, where
he uses a resizing axiom to go down from Type₁ to Type:
\begin{code}
hinhabited₁ : Type → Type₁
hinhabited₁ X = (P : Type) → hprop P → (X → P) → P
\end{code}
This can be read as saying that X is hinhabited iff every hproposition
implied by X is inhabited.
The large type (hinhabited₁ X) is equivalent to our postulated small
type (hinhabited X):
\begin{code}
hinhabited-elim' : (X : Type) → hinhabited X → hinhabited₁ X
hinhabited-elim' X p P f g = hinhabited-elim X P f g p
hinhabited-elim'-converse : (X : Type) → hinhabited₁ X → hinhabited X
hinhabited-elim'-converse X f = f (hinhabited X) hprop-hinhabited η
hstable : Type → Type
hstable X = hinhabited X → inhabited X
hseparated : Type → Type
hseparated X = {x y : X} → hstable(x ≡ y)
\end{code}
hinhabitation is a weakening of inhabitation and a strenghening of
nonemptiness.
\begin{code}
inhabited-is-hinhabited : {X : Type} → inhabited X → hinhabited X
inhabited-is-hinhabited = η
hinhabited-is-nonempty : {X : Type} → hinhabited X → nonempty X
hinhabited-is-nonempty {X} a u = hinhabited-elim X ∅ ∅-is-hprop u a
\end{code}
Hence hseparation is a weakening of separation:
\begin{code}
stable-is-hstable : {X : Type} → stable X → hstable X
stable-is-hstable {X} s a = s(hinhabited-is-nonempty a)
separated-is-hseparated : {X : Type} → separated X → hseparated X
separated-is-hseparated s a = s(hinhabited-is-nonempty a)
\end{code}
Notice that the universal property is not used in the following lemma
and corollary:
\begin{code}
hstable-is-collapsible : {X : Type} → hstable X → collapsible X
hstable-is-collapsible {X} s = (f , g)
where
f : X → X
f x = s(η x)
claim₀ : (x y : X) → η x ≡ η y
claim₀ x y = hprop-hinhabited (η x) (η y)
g : (x y : X) → f x ≡ f y
g x y = ap s (claim₀ x y)
hseparated-is-path-collapsible : {X : Type} → hseparated X → path-collapsible X
hseparated-is-path-collapsible s = hstable-is-collapsible s
\end{code}
By separated-is-hseparated, the following is a further generalization
of Hedberg's Theorem:
\begin{code}
hseparated-is-hset : {X : Type} → hseparated X → hset X
hseparated-is-hset s = path-collapsible-is-hset(hseparated-is-path-collapsible s)
\end{code}
This is as far as we can get in our sequence of weakenings of the
hypothesis of Hedberg's Theorem, because the converse holds:
\begin{code}
hprop-is-hstable : {X : Type} → hprop X → hstable X
hprop-is-hstable {X} h a = hinhabited-elim X X h id a
hset-is-hseparated : {X : Type} → hset X → hseparated X
hset-is-hseparated h a = hprop-is-hstable h a
\end{code}
Hence we have proved that the following are logically equivalent:
(i) X is an hset.
(ii) X is path-collapsible.
(iii) X is hseparated.
Because discreteness implies separation, which in turn implies
hseparation, Hedberg's theorem follows from this.
We haven't thought about the possibility of meaningful examples that
are hseparated but not already separated. In any case, the above
shows that to assume that every type is hstable is unreasonable,
because then all types would be hsets, and we know that there are
(intended HoTT) models in which this fails. But the assumption that
all types are hstable looks much more unreasonable than that. Is it
classical? Very likely. What is its status exactly? See Section 4.
A p p e n d i x t o t h i s s e c t i o n.
Another class of examples of types that are hsets is that of totally
separated types. Notice that the type (totally-separated X) is an
hproposition, assuming function extensionality. A type is totally
separated if any two points satisfying the same decidable properties
are equal.
\begin{code}
₂-discrete : discrete ₂
₂-discrete {₀} {₀} = in₀ refl
₂-discrete {₀} {₁} = in₁(λ())
₂-discrete {₁} {₀} = in₁(λ())
₂-discrete {₁} {₁} = in₀ refl
totally-separated : Type → Type
totally-separated X = {x y : X} → ((p : X → ₂) → p x ≡ p y) → x ≡ y
dependent-funext : Type₁
dependent-funext = {X : Type} {Y : X → Type} {f g : (x : X) → Y x} → ((x : X) → f x ≡ g x) → f ≡ g
totally-separated-is-hset : dependent-funext → (X : Type) → totally-separated X → hset X
totally-separated-is-hset de X t = path-collapsible-is-hset h
where
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 φ γ = de(λ p → discrete-is-hset ₂-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}
There is a better and shorter proof than the above by showing that
totally separated spaces are separated, and concluding the hset
condition from that. This also avoids dependent function
extensionality (but in any case it is known that dependent
extensionality follows from extensionality).
\begin{code}
contra-positive : {R X Y : Type} → (X → Y) → (Y → R) → (X → R)
contra-positive f p x = p(f x)
₂-separated : separated ₂
₂-separated = discrete-is-separated ₂-discrete
totally-separated-is-separated : {X : Type} → totally-separated X → separated X
totally-separated-is-separated {X} t {x} {y} φ = t h
where
a : (p : X → ₂) → nonempty(p x ≡ p y)
a p = φ ∘ contra-positive(ap p)
h : (p : X → ₂) → p x ≡ p y
h p = ₂-separated(a p)
totally-separated-is-hset' : {X : Type} → funext-special-case₁ X → totally-separated X → hset X
totally-separated-is-hset' e t = separated-is-hset e (totally-separated-is-separated t)
\end{code}
Here is another application of (the main lemma
path-collapsible-is-hset of) Hedberg's theorem (17 Feb 2013):
\begin{code}
injective : {X Y : Type} → (f : X → Y) → Type
injective {X} f = {x x' : X} → f x ≡ f x' → x ≡ x'
subtype-of-hset-is-hset : {X Y : Type} (m : X → Y) → injective m → hset Y → hset X
subtype-of-hset-is-hset {X} m i h = path-collapsible-is-hset(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))
π₀-injective : {X : Type} {Y : X → Type} → ({x : X} → hprop(Y x)) → injective π₀
π₀-injective {X} {Y} f {u} {v} r = lemma r (π₁ u) (π₁ v) (f(transport {X} {Y} r (π₁ u)) (π₁ v))
where
A : {x x' : X} → x ≡ x' → Type
A {x} {x'} r = (y : Y x) (y' : Y x') → transport r y ≡ y' → (x , y) ≡ (x' , y')
lemma : {x x' : X} (r : x ≡ x') → A {x} {x'} r
lemma = J A (λ {x} x' y → ap (λ y → (x , y)))
subset-of-hset-is-hset : (X : Type) (Y : X → Type) → hset X → ({x : X} → hprop(Y x)) → hset(Σ \(x : X) → Y x)
subset-of-hset-is-hset X Y h p = subtype-of-hset-is-hset π₀ (π₀-injective p) h
\end{code}
-------------------------------------
-- 2. collapsible X ⇔ hstable X. --
-------------------------------------
Next we prove that the following are logically equivalent:
(ii') X is collapsible.
(iii') X is hstable.
In order to establish this, we need a non-trivial lemma, due to
Nicolai Kraus, which is interesting in its own right. It asserts that
the type of fixed points of any constant endomap is an hproposition.
\begin{code}
fix : {X : Type} → (f : X → X) → Type
fix f = Σ \x → x ≡ f x
\end{code}
The key insight for the proof of Kraus Lemma is the following:
If f : X → Y is constant, then f maps any path x ≡ x to the
trivial path refl.
We need to prove a slightly more general version.
\begin{code}
Kraus-Lemma₀ : {X Y : Type} (f : X → Y) (g : constant f) {x y : X} (p : x ≡ y) → ap f p ≡ (g x x)⁻¹ • (g x y)
Kraus-Lemma₀ f g {x} {y} = J (λ {x} {y} p → ap f p ≡ (g x x)⁻¹ • (g x y)) (λ {x} → sym-is-inverse(g x x))
Kraus-Lemma₁ : {X Y : Type} (f : X → Y) → constant f → {x : X} (p : x ≡ x) → ap f p ≡ refl
Kraus-Lemma₁ f g p = (Kraus-Lemma₀ f g p) • ((sym-is-inverse(g _ _))⁻¹)
\end{code}
We need that transport of equalities in equalities can be described as
composition. We prove a fairly general version and the version we
actually need.
\begin{code}
transport-paths-along-paths : {X Y : Type} {x y : X} (p : x ≡ y) (h k : X → Y) (q : h x ≡ k x)
→ transport p q ≡ (ap h p)⁻¹ • q • (ap k p)
transport-paths-along-paths {X} {Y} {x} p h k q =
J' x (λ p → transport p q ≡ ((ap h p)⁻¹) • q • (ap k p)) (refl-is-right-id q) p
transport-paths-along-paths' : {X : Type} {x : X} (p : x ≡ x) (f : X → X) (q : x ≡ f x)
→ transport {X} {λ z → z ≡ f z} p q ≡ p ⁻¹ • q • (ap f p)
transport-paths-along-paths' {X} {x} p f q =
(transport-paths-along-paths p (λ z → z) f q) • (ap (λ pr → pr ⁻¹ • q • (ap f p)) ((ap-id-is-id p)⁻¹))
\end{code}
We are now ready to prove the fixed-point lemma:
\begin{code}
Kraus-Lemma : {X : Type} (f : X → X) → constant f → hprop(fix f)
Kraus-Lemma {X} f g (x , p) (y , q) =
-- p : x ≡ f x
-- q : y ≡ f y
(x , p) ≡⟨ Σ-≡ x y p p' r refl ⟩
(y , p') ≡⟨ Σ-≡ y y p' q s t ⟩∎
(y , q) ∎
where
r : x ≡ y
r = x ≡⟨ p ⟩
f x ≡⟨ g x y ⟩
f y ≡⟨ q ⁻¹ ⟩∎
y ∎
p' : y ≡ f y
p' = transport r p
s : y ≡ y
s = y ≡⟨ p' ⟩
f y ≡⟨ q ⁻¹ ⟩∎
y ∎
q' : y ≡ f y
q' = transport {X} {λ y → y ≡ f y} s p'
t : q' ≡ q
t = q' ≡⟨ transport-paths-along-paths' s f p' ⟩
s ⁻¹ • (p' • ap f s) ≡⟨ ap (λ pr → s ⁻¹ • (p' • pr)) (Kraus-Lemma₁ f g s) ⟩
s ⁻¹ • (p' • refl) ≡⟨ ap (λ pr → s ⁻¹ • pr) ((refl-is-right-id p')⁻¹) ⟩
s ⁻¹ • p' ≡⟨ refl ⟩
(p' • (q ⁻¹))⁻¹ • p' ≡⟨ ap (λ pr → pr • p') ((sym-trans p' (q ⁻¹))⁻¹) ⟩
((q ⁻¹)⁻¹ • (p' ⁻¹)) • p' ≡⟨ ap (λ pr → (pr • (p' ⁻¹)) • p') ((sym-sym-trivial q)⁻¹) ⟩
(q • (p' ⁻¹)) • p' ≡⟨ trans-assoc q (p' ⁻¹) p' ⟩
q • ((p' ⁻¹) • p') ≡⟨ ap (λ pr → q • pr) ((sym-is-inverse p')⁻¹) ⟩
q • refl ≡⟨ (refl-is-right-id q)⁻¹ ⟩∎
q ∎
\end{code}
It is now easy to prove that collapsible types are hstable:
\begin{code}
from-fix : {X : Type} (f : X → X) → fix f → X
from-fix f = π₀
to-fix : {X : Type} (f : X → X) → constant f → X → fix f
to-fix f g x = (f x , g x (f x))
collapsible-is-hstable : {X : Type} → collapsible X → hstable X
collapsible-is-hstable {X} (f , g) hi = from-fix f l
-- f : X → X
-- g : constant f
-- hi : hinhabited X
where
h : X → fix f
h = to-fix f g
k : hinhabited X → fix f
k = hinhabited-elim X (fix f) (Kraus-Lemma f g) h
l : fix f
l = k hi
\end{code}
This amounts to
collapsible X → (hinhabited X → X),
which can equivalently be written as
hinhabited X → (collapsible X → X).
This says that if X is hinhabited, then from any constant function
f : X → X we can inhabit X, which may be surprising. This inhabitant
of X is a fixed point of f and hence the constant value of f.
More generally, we can ask what is necessary to know about X in order
to inhabit X from any given constant function X → X.
It is natural to conjecture that the weakest condition is that X is
hinhabited. But in fact there is a seemingly weaker condition.
We define (populated₁ X), and show that we have a logical equivalence
populated₁ X ⇔ (collapsible X → X).
The large type (populated₁ X) is defined in the same way as the large
type (hinhabited₁ X), but quantifying over the sub-hpropositions of X,
rather than all hpropositions, so that
hinhabited X → populated₁ X, and populated₁ X → nonempty X.
The type (populated₁ X) is an hproposition, assuming function
extensionality and ignoring size issues, which is larger than
(hinhabited X), as the map hinhabited X → populated₁ X is trivially a
monomorphism.
A small version of populated₁ is constructed in the next section,
using the results of this section.
As already discussed, hinhabited₁ X can be read as saying that any
hproposition implied by X is inhabited. Likewise, populated₁ X can be
read as saying that any hproposition that is logically equivalent to
X must be inhabited:
\begin{code}
populated₁ : Type → Type₁
populated₁ X = (P : Type) → hprop P → (P → X) → (X → P) → P
hinhabited-is-populated₁ : {X : Type} → hinhabited X → populated₁ X
hinhabited-is-populated₁ {X} hi P h a b = hinhabited-elim X P h b hi
populated₁-is-hinhabited-under-hstability : {X : Type} → hstable X → populated₁ X → hinhabited X
populated₁-is-hinhabited-under-hstability {X} s po = po (hinhabited X) hprop-hinhabited s η
\end{code}
Of course, it shouldn't be the case that (populated₁ X → hinhabited X)
in general. But how does one argue about this conjecture? The trouble
is that excluded middle does give that. So we should get a "taboo" out
of (populated₁ X → hinhabited X) to establish the conjecture, or, as a
last resource, provide a counter-model. This conjecture is similar in
this respect to the conjecture that ((X : Type) → collapsible X)
should "fail". This is investigated in Section 4.
Of course:
\begin{code}
populated₁-is-nonempty : {X : Type} → populated₁ X → nonempty X
populated₁-is-nonempty p = p ∅ (∅-is-hprop) ∅-elim
\end{code}
We now prove the logical equivalence (collapsible X → X) ⇔ populated₁ X
and derive collapsible X → hstable X as a corollary.
\begin{code}
D : Type → Type
D X = collapsible X → X
populated₁-is-D : {X : Type} → populated₁ X → D X
populated₁-is-D {X} p (f , g) = from-fix f (p (fix f) (Kraus-Lemma f g) (from-fix f) (to-fix f g))
D-is-populated₁ : {X : Type} → D X → populated₁ X
D-is-populated₁ {X} d P h a b = b x
where
f : X → X
f x = a(b x)
g : constant f
g x y = ap a (h (b x) (b y))
x : X
x = d(f , g)
\end{code}
We have already proved a special case of this:
\begin{code}
collapsible-is-hstable-bis : {X : Type} → collapsible X → hstable X
collapsible-is-hstable-bis c hi = populated₁-is-D (hinhabited-is-populated₁ hi) c
\end{code}
This seems to generalize the main step of the original version of
Hedberg's Theorem:
\begin{code}
path-collapsible-is-hset-bis : {X : Type} → path-collapsible X → hset X
path-collapsible-is-hset-bis c = hseparated-is-hset(collapsible-is-hstable c)
\end{code}
But this is cheating, because hseparated-is-hset uses Hedberg's original proof.
Finally, we can combine both directions:
\begin{code}
both-directions-combined : {X : Type} → ((populated₁ X → X) → X) → populated₁ X
both-directions-combined {X} hypothesis = D-is-populated₁ fact₁
where
fact₀ : collapsible X → (populated₁ X → X)
fact₀ c p = populated₁-is-D p c
fact₁ : D X
fact₁ c = hypothesis(fact₀ c)
both-directions-combined-converse : {X : Type} → populated₁ X → ((populated₁ X → X) → X)
both-directions-combined-converse p u = u p
both-directions-combined-bis : {X : Type} → ((hinhabited X → X) → X) → populated₁ X
both-directions-combined-bis {X} hypothesis = D-is-populated₁(λ c → hypothesis(collapsible-is-hstable c))
\end{code}
Notice that "populated₁" doesn't seem to be functorial, for the same
reasons that D X doesn't seem to be functorial. This gives further
support to the conjecture that (populated₁ X → hinhabited X) ought to
fail (in the sense of being a taboo or having a counter-model). See
Section 4.
This concludes the main development.
--------------------------------------------------------
-- 3. A type size reduction without resizing axioms. --
--------------------------------------------------------
Next we show that the large type (populated₁ X) is equivalent to a
small definable type (populated X), which is an hproposition, without
using hpropositional reflections.
The proof that φ defined below is constant uses function
extensionality. There is an alternative construction of φ, given
later, that doesn't use extensionality but uses hpropositional
reflections. (It seems that hpropositional reflection has some
built-in amount of extensionality. Does it imply some instance of
extensionality?)
Notice that the type D X (=collapsible X → X) is empty if X is empty,
and is inhabited if X is inhabited (and more generally if X is
populated₁, as we have seen above). Of course we cannot in general
decide whether X is empty or inhabited, or that the type D X is empty
or inhabited.
But the following illustrates that there are types that can be shown
to have constant endomaps (and hence to be hstable) without knowledge
of whether they are empty or inhabited.
\begin{code}
postulate funext-special-case₂ : {X : Type} → funext (collapsible X) X
φ : (X : Type) → D X → D X
φ X h (f , g) = f(h(f , g))
\end{code}
To understand this, recall that D X = collapsible X → X where
collapsible X = Σ \(f : X → X) → constant f.
Then the inputs of φ are
h : collapsible X → X
f : X → X
g : constant f
and hence
(f , g) : collapsible X.
Now h(f , g) : X, but this doesn't need to be the constant value of
the function f : X → X. Hence we apply f to h(f , g) to force it to be
the constant value of f. Because f is constant, φ defined in this way
is pointwise constant, and hence constant by function extensionality:
\begin{code}
φ-constant : (X : Type) → constant(φ X)
φ-constant X h k = funext-special-case₂(claim₁ h k)
where
claim₀ : (h k : D X) → (f : X → X) → (g : constant f) → φ X h (f , g) ≡ φ X k (f , g)
claim₀ h k f g = g (h(f , g)) (k(f , g))
claim₁ : (h k : D X) → (c : collapsible X) → φ X h c ≡ φ X k c
claim₁ h k (f , g) = claim₀ h k f g
populated : Type → Type
populated X = fix(φ X)
hprop-populated : (X : Type) → hprop(populated X)
hprop-populated X = Kraus-Lemma (φ X) (φ-constant X)
populated-is-D : {X : Type} → populated X → D X
populated-is-D {X} = from-fix (φ X)
D-is-populated : {X : Type} → D X → populated X
D-is-populated {X} = to-fix (φ X) (φ-constant X)
populated-is-populated₁ : {X : Type} → populated X → populated₁ X
populated-is-populated₁ po = D-is-populated₁(populated-is-D po)
populated₁-is-populated : {X : Type} → populated₁ X → populated X
populated₁-is-populated po = D-is-populated(populated₁-is-D po)
\end{code}
The last two functions are isomorphisms as the two types are
hpropositions, and hence we have a (weak) equivalence.
The following can be proved by reduction to populated₁, but the given
proof avoids detours via large types:
\begin{code}
inhabited-is-populated : {X : Type} → X → populated X
inhabited-is-populated {X} x = D-is-populated (λ c → x)
populated-is-nonempty : {X : Type} → populated X → nonempty X
populated-is-nonempty {X} (f , g) u = u(f(h , h-constant))
where
h : X → X
h = ∅-elim ∘ u
h-constant : (x y : X) → h x ≡ h y
h-constant x y = ∅-elim(u x)
\end{code}
Similarly, the facts that hinhabited-is-populated and that
collapsible-is-hstable can be proved without a detour via large types.
Q u e s t i o n. It is hence natural to ask whether it is possible
to perform a similar type size reduction to show that inhabited₁ X
has a small definable counter-part, in particular getting rid of
postulates and resizing axioms to define hinhabited X.
Hence we formulate:
P r o b l e m. Prove (by exhibiting a construction within type
theory) or disprove (by exhibiting a counter-model or using
syntactical arguments or reducing to a taboo) that there is a
definable type constructor hinhabited : Type → Type such that
hinhabited X ⇔ hinhabited₁ X. This problem can be considered with
and without assuming extensionality axioms, and with and without
assuming univalence, and with or without considering universes,
etc.
D i s c u s s i o n o f t h e p r o b l e m.
We have inhabited₁ X → populated X, and this map (and any such map)
is a monomorphism embedding the large type inhabited₁ X into the
small type populated X. Can a small version of inhabited₁ X be
carved out of the small type populated X? A difficulty is that that
inhabited₁ X cannot be a retract of populated X, because this would
amount to the existence of a map populated X → inhabited₁ X, which
is shown to be unlikely in Section 4. But there may be other ways
of getting a small copy of inhabited₁ X out of the small type
populated X. It is unclear at the time of writing whether the
large type inhabited₁ X can be made small without axioms. Of
course, it may be natural to conjecture that it cannot. But we
don't know. At least it is interesting to know that it is
monomorphically embedded into a small definable type. This is
analogous to the fact that a subset of a finite set doesn't need to
be finite.
Ignoring this question, next we show that if we instead assume (small)
hpropositional reflections, we don't need to assume extensionality to
perform the above size reduction from populated₁ x to populated X.
To do this, it is convenient to first define the monad structure on
hinhabited coming from the reflection. To define it as a Kleisli
triple, it remains to define the Kleisli extension operator (following
standard category theory):
\begin{code}
hinhabited-extension : {X Y : Type} → (X → hinhabited Y) → (hinhabited X → hinhabited Y)
hinhabited-extension {X} {Y} f p = hinhabited-elim X (hinhabited Y) hprop-hinhabited f p
\end{code}
The Kleisli-triple laws are trivial, because they are equations
between hproposition-valued functions. We formulate them pointwise to
avoid extensionality.
\begin{code}
kleisli-law₀ : {X : Type} (p : hinhabited X) → hinhabited-extension η p ≡ p
kleisli-law₀ p = hprop-hinhabited (hinhabited-extension η p) p
kleisli-law₁ : {X Y : Type} → (f : X → hinhabited Y) → (x : X) → (hinhabited-extension f)(η x) ≡ f x
kleisli-law₁ {X} {Y} f x = hprop-hinhabited ((hinhabited-extension f)(η x)) (f x)
kleisli-law₂ : {X Y Z : Type} → (f : X → hinhabited Y) → (g : Y → hinhabited Z) → (p : hinhabited X) →
hinhabited-extension((hinhabited-extension g) ∘ f) p ≡ (hinhabited-extension g)(hinhabited-extension f p)
kleisli-law₂ f g p =
hprop-hinhabited (hinhabited-extension((hinhabited-extension g) ∘ f) p) ((hinhabited-extension g)(hinhabited-extension f p))
\end{code}
Now the standard data that defines the monad (which automatically
satisfies the monad laws (pointwise)):
\begin{code}
hinhabited-functor : {X Y : Type} → (X → Y) → hinhabited X → hinhabited Y
hinhabited-functor f = hinhabited-extension(η ∘ f)
μ : {X : Type} → hinhabited(hinhabited X) → hinhabited X
μ = hinhabited-extension id
\end{code}
Because the functor is enriched (that is, internally defined) and the
category of types is cartesian closed, the monad is strong:
\begin{code}
hinhabited-strength : {X Y : Type} → X × hinhabited Y → hinhabited(X × Y)
hinhabited-strength (x , q) = hinhabited-functor(λ y → (x , y)) q
hinhabited-shift : {X Y : Type} → hinhabited X × hinhabited Y → hinhabited(X × Y)
hinhabited-shift (p , q) = hinhabited-extension(λ x → hinhabited-strength(x , q)) p
\end{code}
This time we prove directly that a certain type is hstable without
knowing whether it is empty or inhabited:
\begin{code}
hstable-example : (X : Type) → hstable(D X)
hstable-example X h c = x
-- h : hinhabited(D X)
-- c : collapsible X
where
p : hinhabited(collapsible X × D X)
p = hinhabited-strength(c , h)
f : collapsible X × D X → X
f(c , φ) = φ c
q : hinhabited X
q = hinhabited-functor f p
x : X
x = collapsible-is-hstable c q
collapsible-example-bis : (X : Type) → collapsible(D X)
collapsible-example-bis X = hstable-is-collapsible(hstable-example X)
\end{code}
Hence alternatively we can take:
\begin{code}
φ-bis : (X : Type) → D X → D X
φ-bis X = π₀(collapsible-example-bis X)
φ-constant-bis : (X : Type) → constant(φ-bis X)
φ-constant-bis X = π₁(collapsible-example-bis X)
\end{code}
There is yet another natural way of definining the small type
populated X:
populated X = (f : X → X) → constant f → fix f
This says that a type is populated iff every constant endomap has a
fixed point, and hence we can inhabit the type given any constant
endomap.
Again it is easy to show that populated X ⇔ D X, using the above
ideas. We leave the details to the reader. But to show that
populated X is an hproposition we need the dependent version of
function extensionality, using the fact that fix f is an hproposition.
------------------------------------
-- 4. Taboos and counter-models. --
------------------------------------
We want to undertand the differences between the various notions of
inhabitation, hinhabitation, population and nonemptiness. We use two
techniques, namely taboos (expressed in Agda) and HoTT models
(expressed in our meta-language, namely mathematical English).
We have the chain of implications
inhabited X → hinhabited X → populated X → nonempy X.
All implications can be reversed if excluded middle holds.
Can them be reversed in general?
1. If the first implication can be reversed, then all types are
hsets (a homotopy type theory taboo, which is not valid e.g. in
the model of simplicial sets).
2. We don't know the answer for the middle implication, which is the
most interesting one, but we reduce it to a simpler question.
3. If the last implication can be reversed, we get excluded middle
for hpropositions, and weak excluded middle for arbitrary types
(a constructive taboo, which is not valid in recursive models).
It would be wonderful to be able to reverse the middle implication,
because then we would have that hinhabited is MLTT definable as
hinhabited X = populated X,
answering positively the open question of Section 3. We very much
doubt that this is the case, but we don't know.
We now discuss each of the three implications in the order they are
given above.
4.1. We have already investigated the reversal of the implication
inhabited X → hinhabited X
to some extent.
When this reversal can be performed, we said that X is hstable. This
reversal can be performed when X is empty, and when X is inhabited,
but not necessarily in the absence of knowledge of which is the
case. In fact, we have already argued, but not proved in Agda, that:
\begin{code}
HoTT-taboo : Type₁
HoTT-taboo = (X : Type) → hset X
all-types-are-hstable-is-a-HoTT-taboo : ((X : Type) → hstable X) → HoTT-taboo
all-types-are-hstable-is-a-HoTT-taboo h _ = hseparated-is-hset(h(_ ≡ _))
\end{code}
This is an application of our generalization hseparated-is-hset of
Hedberg's Theorem.
Because a type is hstable iff it is collapsible, we see that saying
that all types are hstable amounts to saying that every type has a
constant endofunction. This reduction is nice because the notion of
collapsibility can be understood without reference to the notion of
hpropositional reflection.
That every type X has a constant endofunction is rather dubious from a
constructive point of view, bearing in mind that X may or may not be
empty, but we have no means of knowing in general which case
holds. Both empty and inhabited types have constant endomaps, but
defined in different ways. In any case, it is a HoTT taboo, as shown
above, and hence we have:
M e t a - t h e o r e m. It is not provable in MLTT that every
type has a constant endofunction, or in MLTT+hinhabited that every
type is hstable.
We have argued that not every type is collapsible by reducing to a
HoTT taboo and exhibiting a counter-model. It would be much nicer to
instead derive a constructive taboo from the hypothetical
collapsibility of all types, expressed in Agda, in a fragment of the
language corresponding to MLTT, possibly extended with function
extensionality.
4.2. It turns out that the reversal of the implication
hinhabited X → populated X
is also related to hstability or equivalently collapsibility, as
discussed below, in two ways.
Firstly, pstability is logically equivalent to hstability, which is
part of the reason why the reversibility of the implication
hinhabited X → populated X is a difficult question.
\begin{code}
pstable : Type → Type
pstable X = populated X → X
pstable-is-hstable : (X : Type) → pstable X → hstable X
pstable-is-hstable X p h = p(populated₁-is-populated(hinhabited-is-populated₁ h))
hstable-is-pstable : (X : Type) → hstable X → pstable X
hstable-is-pstable X h p = populated-is-D p (hstable-is-collapsible h)
\end{code}
Secondly, in light of the above, the following is perhaps surprising:
although we cannot necessarily inhabit the type (hstable X), we can
always populate it:
\begin{code}
populated₁-hstable : {X : Type} → populated₁(hstable X)
populated₁-hstable {X} P h a b = b hs
-- h : hprop P
-- a : P → hstable X
-- b : hstable X → P
where
u : X → P
u x = b(λ _ → x)
g : hinhabited X → P
g hi = hinhabited-elim X P h u hi
hs : hinhabited X → X
hs hi = a (g hi) hi
populated-hstable : {X : Type} → populated(hstable X)
populated-hstable = populated₁-is-populated populated₁-hstable
nonempty-hstable : {X : Type} → nonempty(hstable X)
nonempty-hstable = populated₁-is-nonempty populated₁-hstable
\end{code}
Using this, we show that the implication (hinhabited X → populated X)
can be reversed for all X if and only if the type (hstable X) is
hinhabited for all X.
\begin{code}
populated-inhabited-charac : ((X : Type) → populated X → hinhabited X) → ((X : Type) → hinhabited(hstable X))
populated-inhabited-charac f X = f (hstable X) populated-hstable
populated-inhabited-charac' : ((X : Type) → hinhabited(hstable X)) → ((X : Type) → populated X → hinhabited X)
populated-inhabited-charac' f X po =
hinhabited-extension (λ h → populated₁-is-hinhabited-under-hstability h (populated-is-populated₁ po)) (f X)
\end{code}
P r o b l e m. Prove that
(X : Type) → hinhabited(hstable X)
by exhibiting a construction, or show that no such construction is
possible by reduction to a taboo or by the use of a counter-model.
We don't expect such a construction to exist. If it is not possible,
an argument with a taboo rather than a counter-model would be
preferable.
4.3. It remains to discuss the reversal of the implication
populated X → nonempty X.
The type (decidable P), where P is any hproposition, is an example of
a nonempty, collapsible type whose (h)inhabitation is a taboo:
\begin{code}
nonempty-decidable : {X : Type} → nonempty(decidable X)
nonempty-decidable d = d(in₁(λ x → d(in₀ x)))
postulate funext-special-case₃ : {X : Type} → funext X ∅
∅-valued-functions-are-equal : {X : Type} → hprop(empty X)
∅-valued-functions-are-equal {X} f g = funext-special-case₃ {X} (λ x → ∅-elim(f x))
hhd : {P : Type} → hprop P → hprop(decidable P)
hhd h (in₀ p) (in₀ q) = ap in₀ (h p q)
hhd h (in₀ p) (in₁ v) = ∅-elim(v p)
hhd h (in₁ u) (in₀ q) = ∅-elim(u q)
hhd h (in₁ u) (in₁ v) = ap in₁ (∅-valued-functions-are-equal u v)
hcd : {P : Type} → hprop P → collapsible(decidable P)
hcd h = (id , hhd h)
\end{code}
We know that populated-is-nonempty. From the above we conclude that
the converse is a constructive taboo, in the sense that it implies
h-excluded middle, which in turn implies weak excluded middle:
\begin{code}
hEM : Type₁
hEM = (P : Type) → hprop P → decidable P
wEM : Type₁
wEM = (X : Type) → decidable(empty X)
hEM-implies-wEM : hEM → wEM
hEM-implies-wEM hem X = hem (empty X) ∅-valued-functions-are-equal
all-nonempty-types-are-populated-taboo : ((X : Type) → nonempty X → populated X) → hEM
all-nonempty-types-are-populated-taboo a P h = populated-is-D p c
where
p : populated(decidable P)
p = a (decidable P) nonempty-decidable
c : collapsible(decidable P)
c = hcd h
\end{code}
A d d e n d u m (12 Mar 2013).
hAC is the (h-)proposition
(X : Type) (Y : X → Type)
→ ((x : X) → hinhabited(Y x)) → hinhabited((x : X) → Y x).
We show that hEM (defined above) gives a weak form of hAC:
(X Y : Type) → (X → hinhabited Y) → hinhabited(X → Y).
First we prove some "choice" facts that don't depend on hEM.
The first proof is obtained automatically by Agda with Ctrl-C Ctrl-A,
but we give a proof organized in steps, which we found before trying
to get an automatic proof, which is
b (λ x → a (h x P hP (λ p → a p x) (λ y → b (λ _ → y))) x),
after we renamed some variables to match the names below.
The term pAC below normalizes to λ {X} {Y} h P hP a b →
b (λ x → a (h x P hP (λ p → a p x) (λ y → b (λ _ → y))) x).
\begin{code}
pAC : {X Y : Type} → (X → populated₁ Y) → populated₁(X → Y)
pAC {X} {Y} h P hP a b = b hs
-- h : X → populated Y
-- hP : hprop P
-- a : P → X → Y
-- b : (X → Y) → P
where
u : X → Y → P -- We could try (x : X) → Y x → P with Y : X → Type
u x y = b(λ _ → y) -- But this line breaks with Y : X → Type.
g : X → populated₁ Y → P
-- po : (P : Type) → hprop P → (P → Y) → (Y → P) → P
g x po = po P hP (λ p → a p x) (λ y → u x y)
hs : X → Y
hs x = a (g x (h x)) x
mixed-AC : {X Y : Type} → (X → hinhabited Y) → populated₁(X → Y)
mixed-AC f = pAC (λ x → hinhabited-is-populated₁(f x))
weak-mixed-AC : {X Y : Type} → (X → hinhabited Y) → nonempty(X → Y)
weak-mixed-AC {X} {Y} p = populated₁-is-nonempty (mixed-AC p)
DN : {R X Y : Type} → (X → Y) → ((X → R) → R) → ((Y → R) → R)
DN f = contra-positive(contra-positive f)
weak-hAC : hEM → {X Y : Type} → (X → hinhabited Y) → hinhabited(X → Y)
weak-hAC hem {X} {Y} h = f hEM-special-case
where
hEM-special-case : hinhabited(X → Y) + empty(hinhabited(X → Y))
hEM-special-case = hem (hinhabited(X → Y)) hprop-hinhabited
fact : nonempty(X → Y)
fact = weak-mixed-AC h
claim : nonempty(X → Y) → nonempty(hinhabited(X → Y))
claim = DN η
f : hinhabited(X → Y) + empty(hinhabited(X → Y)) → hinhabited(X → Y)
f (in₀ hi) = hi
f (in₁ nhi) = ∅-elim(claim fact nhi)
very-weak-hAC : hEM → {X : Type} → hinhabited(hstable X)
very-weak-hAC hem {X} = weak-hAC hem id
\end{code}
Does {X : Type} → hinhabited(hstable X) imply hEM?
More modestly, does {X Y : Type} → (X → hinhabited Y) → hinhabited(X → Y)
imply hEM?
Actually, this is not more modest (26 Mar 2013):
\begin{code}
hh→hh : ((X : Type) → hinhabited(hstable X)) → (X Y : Type) → (X → hinhabited Y) → hinhabited(X → Y)
hh→hh hh X Y f = hinhabited-functor (λ p → (π₁ p) ∘ (π₀ p)) lemma
where
lemma : hinhabited ((X → hinhabited Y) × (hinhabited Y → Y))
lemma = hinhabited-strength (f , hh Y)
hh←hh : ((X Y : Type) → (X → hinhabited Y) → hinhabited(X → Y)) → (X : Type) → hinhabited(hstable X)
hh←hh hh X = hh (hinhabited X) X id
\end{code}
A d d e n d u m (22 Mar 2013)
A local version of Hedberg's theorem, using J' (Paulin-Mohring)
instead of J to get the localization (compare with the proof of
path-collapsible-is-hset above):
\begin{code}
local-hedberg : {X : Type} → (x : X)
→ ({y : X} → collapsible(x ≡ y))
→ (y : X) → hprop(x ≡ y)
local-hedberg {X} x pc y p q = claim₂
where
f : {y : X} → x ≡ y → x ≡ y
f = π₀ pc
g : {y : X} (p q : x ≡ y) → f p ≡ f q
g = π₁ pc
claim₀ : {y : X} (r : x ≡ y) → r ≡ (f refl)⁻¹ • (f r)
claim₀ = J' x (λ r → r ≡ ((f refl)⁻¹) • (f r)) (sym-is-inverse(f refl))
claim₁ : (f refl)⁻¹ • (f p) ≡ (f refl)⁻¹ • (f q)
claim₁ = ap (λ h → (f refl)⁻¹ • h) (g p q)
claim₂ : p ≡ q
claim₂ = (claim₀ p) • claim₁ • (claim₀ q)⁻¹
path-collapsible-is-hset-as-a-special-case : {X : Type} → path-collapsible X → hset X
path-collapsible-is-hset-as-a-special-case {X} pc {x} {y} p q = local-hedberg x (λ {y} → (π₀(pc {x} {y})) , (π₁(pc {x} {y}))) y p q
\end{code}
So, for instance, if x is isolated in the sense that equality x ≡ y is
decidable for all y, then x ≡ y is an hprop for all y. And example is
the set ℕ∞ defined elsewhere, in which ∞ is not isolated but all
finite points are isolated. This example is not very good because ℕ∞
is an hset anyway (shown in another file).
A d d e n d u m (30 March 2013)
--------------------------------
We have seen that the hstability of all types is a HoTT taboo. But
actually it is already a constructive taboo that implies the HoTT
taboo.
The main lemma says that if the type
(a₀ ≡ x) + (a₁ ≡ x)
is hstable for every x : X, then the type a₀ ≡ a₁ is decidable. We
formulate this in a more convenient way:
\begin{code}
global-choice-lemma : (X : Type) → (a : ₂ → X) → ({x : X} → hstable(Σ \(i : ₂) → a i ≡ x)) → decidable(a ₀ ≡ a ₁)
global-choice-lemma X a choice = equal-or-different
where
E : Type
E = Σ \(x : X) → hinhabited(Σ \(i : ₂) → a i ≡ x)
r : ₂ → E
r i = a i , η(i , refl)
r-Σ-≡s : (e : E) → Σ \(i : ₂) → r i ≡ e
r-Σ-≡s (x , p) = π₀ p' , Σ-≡ (a(π₀ p')) x (η((π₀ p') , refl)) p (π₁ p') (hprop-hinhabited _ p)
where
p' : Σ \(i : ₂) → a i ≡ x
p' = choice p
s : E → ₂
s e = π₀(r-Σ-≡s e)
r-retract : (e : E) → r(s e) ≡ e
r-retract e = π₁(r-Σ-≡s 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 = Σ-≡ (a i) (a j) (η(i , refl)) (η(j , refl)) p (hprop-hinhabited _ (η(j , refl)))
r-a : (i j : ₂) → r i ≡ r j → a i ≡ a j
r-a i j q = ap π₀ q
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(₂-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))
global-choice-constructive-taboo : ({X : Type} → hinhabited X → X) → (X : Type) → discrete X
global-choice-constructive-taboo global-choice X {a₀} {a₁} = global-choice-lemma X a (λ {x} → global-choice)
where
a : ₂ → X
a ₀ = a₀
a ₁ = a₁
\end{code}
Remark: This uses only MLTT extended with hinhabited. But actually not
even this is needed, because if every type has a constant endomap
(another formulation of global choice) then hinhabited is definable. See
http://www.cs.bham.ac.uk/~mhe/GeneralizedHedberg/ConstantChoice/ConstantChoice.html
So "every type has a constant endomap" (global choice) implies the
discreteness of all types without any extension to intensional MLTT.
A d d e n d u m (2 April 2013)
--------------------------------
Another way of seeing something already observed above.
\begin{code}
p→h : {X : Type} → populated₁ X → hinhabited(hinhabited X → X) → hinhabited X
p→h {X} po = hinhabited-elim (hinhabited X → X) (hinhabited X) hprop-hinhabited lemma
where
lemma : (hinhabited X → X) → hinhabited X
lemma s = po (hinhabited X) hprop-hinhabited s η
h→p : {X : Type} → (hinhabited(hinhabited X → X) → hinhabited X) → populated₁ X
h→p {X} φ P h a b = b'(lemma(a ∘ b'))
where
b' : hinhabited X → P
b' = hinhabited-elim X P h b
lemma : (hinhabited X → X) → hinhabited X
lemma = φ ∘ η
\end{code}
This gives another way of seeing directly why (X*->X)* gives populated X → hinhabited X:
Another possible small definition of populated is
populated X = (X* → X)* → X*
A d d e n d u m (3 April 2013)
--------------------------------
Our hypothesis is that (X*->X)* for every type X. We show that it is
equivalent to hpropositional choice:
(P : Type)(Y : P → Type) → hprop P → ((p : P) → (Y p)*) → ((p : P) → Y p)*
\begin{code}
hprop-choice-gives-hypothesis :
((P : Type)(Y : P → Type) → hprop P → ((p : P) → hinhabited(Y p)) → hinhabited((p : P) → Y p))
→ ((X : Type) → hinhabited(hinhabited X → X))
hprop-choice-gives-hypothesis hprop-AC X = hprop-AC (hinhabited X) (λ p → X) hprop-hinhabited id
Σ-hinhabited-shift : {X : Type} {Y : X → Type} → (Σ \(x : X) → hinhabited(Y x)) → hinhabited(Σ \(x : X) → Y x)
Σ-hinhabited-shift {X} {Y} (x , h) = lemma x h
where
lemma : ∀(x : X) → hinhabited(Y x) → hinhabited(Σ \(x : X) → Y x)
lemma x = hinhabited-functor(λ y → (x , y))
hypothesis-gives-hprop-choice :
((X : Type) → hinhabited(hinhabited X → X))
→ (P : Type)(Y : P → Type) → hprop P → ((p : P) → hinhabited(Y p)) → hinhabited((p : P) → Y p)
hypothesis-gives-hprop-choice φ P Y h f = hinhabited-functor claim₅ claim₄
where
-- f : (p : P) → hinhabited (Y p)
X : Type
X = Σ \(p : P) → Y p
φ' : hinhabited(hinhabited X → X)
φ' = φ X
claim₀ : (p : P) → Σ \(p' : P) → hinhabited(Y p')
claim₀ p = (p , f p)
claim₁ : P → hinhabited X
claim₁ p = Σ-hinhabited-shift(claim₀ p)
claim₂ : hinhabited((P → hinhabited X) × (hinhabited X → X))
claim₂ = hinhabited-strength(claim₁ , φ')
claim₃ : (P → hinhabited X) × (hinhabited X → X) → P → X
claim₃ (g , h) = h ∘ g
claim₄ : hinhabited(P → X)
claim₄ = hinhabited-functor claim₃ claim₂
claim₅ : (P → X) → (p : P) → Y p
claim₅ ψ p = transport {P} {Y} e y
where
p' : P
p' = π₀(ψ p)
y : Y p'
y = π₁ (ψ p)
e : p' ≡ p
e = h p' p
\end{code}
Combining this with the type-theoretic theorem of choice, we get a
more familiar looking (equivalent) version of choice (Spector):
\begin{code}
tt-TC : {X : Type}{Y : X → Type}{A : (x : X) → Y x → Type}
→ (∀(x : X) → Σ \(y : Y x) → A x y) → Σ \(f : (x : X) → Y x) → ∀(x : X) → A x (f x)
tt-TC f = (λ x → π₀(f x)) , (λ x → π₁(f x))
∃ : {X : Type}(Y : X → Type) → Type
∃ Y = hinhabited(Σ Y)
hypothesis-gives-hprop-choice' :
((X : Type) → hinhabited(hinhabited X → X))
→ (P : Type)(Y : P → Type) → (A : (p : P) → Y p → Type) → hprop P
→ (∀(p : P) → ∃ \(y : Y p) → A p y) → ∃ \(f : (p : P) → Y p) → ∀(p : P) → A p (f p)
hypothesis-gives-hprop-choice' φ P Y A h = hinhabited-functor tt-TC ∘ hshift
where
hshift : (∀(p : P) → hinhabited(Σ \(y : Y p) → A p y)) → hinhabited(∀(p : P) → Σ \(y : Y p) → A p y)
hshift = hypothesis-gives-hprop-choice φ P (λ p → Σ \(y : Y p) → A p y) h
\end{code}
Part of the above doesn't use the fact that P is an hprop:
\begin{code}
hypothesis-gives-funny-choice :
((Z : Type) → hinhabited(hinhabited Z → Z))
→ (X : Type)(Y : X → Type) → ((x : X) → hinhabited(Y x)) → hinhabited(X → Σ \(x : X) → Y x)
hypothesis-gives-funny-choice φ X Y f = claim₄
where
-- f : (x : X) → hinhabited (Y x)
Z : Type
Z = Σ \(x : X) → Y x
φ' : hinhabited(hinhabited Z → Z)
φ' = φ Z
claim₀ : (x : X) → Σ \(x' : X) → hinhabited(Y x')
claim₀ x = (x , f x)
claim₁ : X → hinhabited Z
claim₁ x = Σ-hinhabited-shift(claim₀ x)
claim₂ : hinhabited((X → hinhabited Z) × (hinhabited Z → Z))
claim₂ = hinhabited-strength(claim₁ , φ')
claim₃ : (X → hinhabited Z) × (hinhabited Z → Z) → X → Z
claim₃ (g , h) = h ∘ g
claim₄ : hinhabited(X → Z)
claim₄ = hinhabited-functor claim₃ claim₂
\end{code}
Added 26 July after a useful discussion in the HoTT
mailing list:
Let's change terminology to match the HoTT list discussion (and the
TLCA'2013 paper):
\begin{code}
∥_∥ : Type → Type
∥ X ∥ = hinhabited X
∣_∣ : {X : Type} → X → ∥ X ∥
∣ x ∣ = η x
postulate hprop-hprop : {X : Type} → hprop(hprop X) -- Standard fact. A proof will be included.
\end{code}
We introduce a sub-module with the purpose of saying "let ... then ..."
\begin{code}
module HoTT-list-discussion
(X : Type)
(f : X → X)
(s : ∥ constant f ∥)
where
\end{code}
Recall that we defined above
constant f = (x y : X) → f x ≡ f y
fix f = Σ \x → x ≡ f x
\begin{code}
lemma₀ : constant f → hprop(fix f)
lemma₀ = Kraus-Lemma f
lemma₁ : ∥ constant f ∥ → hprop(fix f)
lemma₁ = hinhabited-elim (constant f) (hprop(fix f)) hprop-hprop lemma₀
F : constant f → X → fix f
F κ x = f x , κ x (f x)
G : ∥ constant f ∥ → X → fix f
G s x = hinhabited-elim (constant f) (fix f) (lemma₁ s) (λ κ → F κ x) s
\end{code}
So the inhabitation of ∥ constant f ∥ suffices to extract an element
of X as soon as we have ∥ X ∥:
\begin{code}
choice : ∥ X ∥ → X
choice t = π₀ (hinhabited-elim X (fix f) (lemma₁ s) (G s) t)
\end{code}
But we can say more:
\begin{code}
g : X → X
g x = π₀(G s x)
g-fixes-f : (x : X) → g x ≡ f(g x)
g-fixes-f x = π₁(G s x)
g-constant : constant g
g-constant x y = ap π₀ p
where
p : G s x ≡ G s y
p = lemma₁ s _ _
g-is-f-truncated : ∥ ((x : X) → g x ≡ f x) ∥
g-is-f-truncated = hinhabited-functor conditional-agreement s
where
conditional-agreement : constant f → (x : X) → g x ≡ f x
conditional-agreement κ x = g-fixes-f x • κ (g x) x
\end{code}