The Nearly-Inverse of the Truncation Map ∣_∣ : ℕ → ∥ ℕ ∥
=======================================================
For a nontrivial class of types ("homogeneous" types) which
includes the natural numbers ℕ, I show how the map ∣_∣ from
the type into its propositional truncation can "nearly" be
inverted, in the following sense:
I define a term "myst" such that
id-factored : ℕ → ℕ
id-factored = myst ∘ ∣_∣
is a factorization of the identity map on ℕ through ℕ, and the
proof is very simple:
proof : (n : ℕ) → id-factored n == n
proof n = idp
Note that "idp" is the identity-path (aka refl).
This also implies that, if n is privately defined to be 17 and
only x ≡ ∣ n ∣ is accessible, the number 17 can be recovered by
applying 'myst' to 'x'.
I find this extremly counterintuitive as ∥ ℕ ∥ is equivalent to
the unit type, and ∣_∣ is (as I used to understand it) assumed
to hide information. My construction shows that ∣_∣ does not
do a good job at hiding.
My construction is correct with respect to the definitions in
the book. In this Agda file, I use propositional truncation as
defined in the HoTT-library. Martin Escardo has checked that the
construction also works if the truncation is defined in the
style of Voevodsky, i.e. by quantifying over all propositions.
The construction is inspired by Martin's insight on "judgmental
factorization of constant functions" and my earlier attempts to
related problems that used pointed types.
[Nicolai Kraus, October 2013]
\begin{code}
{-# OPTIONS --without-K #-}
module trunc-inverse where
open import lib.types.Nat
open import lib.Basics
open import lib.Univalence
open import lib.Funext
open import lib.types.Truncation
{- == Pointed types ==
A pointed type is a type (base) together with a chosen
element (pt). -}
Type• : (i : ULevel) → Type (lsucc i)
Type• i = Σ (Type i) (idf _)
module _ {i} (X : Type• i) where
base = fst X
pt = snd X
-- I later consider the type of pointed types that are
-- equal to X:
pathto : Type (lsucc i)
pathto = Σ (Type• i) (λ Y → Y == X)
-- As it is well-known, this type is contractible and
-- thereby propositional:
pathto-prop : is-prop pathto
pathto-prop = raise-level ⟨-2⟩ (pathto-is-contr X)
-- Let me call a pointed type (base,pt) 'homogeneous' iff,
-- for any x:base, the expressions (base,x) and (base,pt)
-- are equal as pointed types:
is-homogeneous : Type (lsucc i)
is-homogeneous = (x : base) → (base , x) == X
{- == Truncation ==
I only use propositional truncation. For a type X,
write ∥ X ∥ for its truncation, and ∣_∣ : X → ∥ X ∥ for the
constructor. -}
module _ {i} where
∥_∥ : Type i → Type i
∥_∥ = Trunc ⟨-1⟩
∣_∣ : {A : Type i} → A → ∥ A ∥
∣_∣ = [_]
{- == The "mysterious" construction for any homogeneous type == -}
module hom-myst {i} (ptX : Type• i) (t : is-homogeneous ptX) where
X = base ptX
x₀ = pt ptX
f : X → pathto (X , x₀)
f x = (X , x) , t x
f-lifted : ∥ X ∥ → pathto (X , x₀)
f-lifted = Trunc-rec (pathto-prop _) f
myst : (x : ∥ X ∥) → (fst ∘ fst ∘ f-lifted) x
myst = snd ∘ fst ∘ f-lifted
-- (the following two proofs will not be used later)
id-factor : (x : X) → myst ∣ x ∣ == x
id-factor x = idp
id-factor' : myst ∘ ∣_∣ == idf _
id-factor' = λ= id-factor
{- My first example of homogeneous types is the class of all tyoes
with decidable equality. -}
module dec-hom {i} (ptX : Type• i) (dec : has-dec-eq (base ptX)) where
X = base ptX
x₀ = pt ptX
module _ (x : X) where
-- I define a function X → X that switches x and x₀.
switch : X → X
switch = λ y → match dec y x₀
withl (λ _ → x)
withr (λ _ → match dec y x
withl (λ _ → x₀)
withr (λ _ → y))
-- Rather tedious to prove, but completely straightforward:
-- this map is its own inverse.
switch-selfinverse : (y : X) → switch (switch y) == y
switch-selfinverse y with dec y x₀
switch-selfinverse y | inl _ with dec x x₀
switch-selfinverse y | inl y-x₀ | inl x-x₀ = x-x₀ ∙ ! y-x₀
switch-selfinverse y | inl _ | inr _ with dec x x
switch-selfinverse y | inl y-x₀ | inr _ | inl _ = ! y-x₀
switch-selfinverse y | inl _ | inr _ | inr ¬x-x = Empty-elim {A = λ _ → x == y} (¬x-x idp)
switch-selfinverse y | inr _ with dec y x
switch-selfinverse y | inr _ | inl _ with dec x x₀
switch-selfinverse y | inr ¬x-x₀ | inl y-x | inl x-x₀ = Empty-elim (¬x-x₀ (y-x ∙ x-x₀))
switch-selfinverse y | inr _ | inl _ | inr _ with dec x₀ x₀
switch-selfinverse y | inr _ | inl y-x | inr _ | inl _ = ! y-x
switch-selfinverse y | inr _ | inl _ | inr _ | inr ¬x₀-x₀ = Empty-elim {A = λ _ → _ == y} (¬x₀-x₀ idp)
switch-selfinverse y | inr _ | inr _ with dec y x₀
switch-selfinverse y | inr ¬y-x₀ | inr _ | inl y-x₀ = Empty-elim {A = λ _ → x == y} (¬y-x₀ y-x₀)
switch-selfinverse y | inr _ | inr _ | inr _ with dec y x
switch-selfinverse y | inr _ | inr ¬y-x | inr _ | inl y-x = Empty-elim {A = λ _ → x₀ == y} (¬y-x y-x)
switch-selfinverse y | inr _ | inr _ | inr _ | inr _ = idp
switch-maps : switch x == x₀
switch-maps with dec x x₀
switch-maps | inl x-x₀ = x-x₀
switch-maps | inr _ with dec x x
switch-maps | inr _ | inl _ = idp
switch-maps | inr _ | inr ¬x-x = Empty-elim {A = λ _ → x == x₀} (¬x-x idp)
-- switch is an equivalence
switch-eq : X ≃ X
switch-eq = equiv switch switch
switch-selfinverse switch-selfinverse
-- It is easy to see how to use the above construction for
-- showing that X is homogeneous.
is-hom : is-homogeneous ptX
is-hom x = pair= (ua X-X) x-x₀ where
X-X : X ≃ X
X-X = switch-eq x
x-x₀ : PathOver (idf (Type i)) (ua X-X) x (snd ptX)
x-x₀ = ↓-idf-ua-in X-X (switch-maps x)
-- As an example, we do the case of ℕ explicitely.
module example-ℕ where
open hom-myst (ℕ , 0)
open dec-hom (ℕ , 0)
myst-ℕ = myst (dec-hom.is-hom _ ℕ-has-dec-eq)
-- I can now "factor" the identity map on ℕ:
id-factored : ℕ → ℕ
id-factored = myst-ℕ ∘ ∣_∣
proof : (n : ℕ) → id-factored n == n
proof n = idp
proof' : id-factored == idf ℕ
proof' = λ= proof
-- A very simple lemma: composing with an equality is an equivalence.
module _ {i} (A : Type i) (a b : A) where
∙-is-eq : (x : A) (p : x == a) → is-equiv (_∙_ {z = b} p)
∙-is-eq .a idp = idf-is-equiv _
{- My second example of homogeneous types is the class of (inhabited)
path spaces. -}
module path-hom {i} (A : Type i) (a₁ a₂ : A) (p : a₁ == a₂) where
is-hom : is-homogeneous (a₁ == a₂ , p)
is-hom q = pair= (ua eq) p-q where
eq : (a₁ == a₂) ≃ (a₁ == a₂)
eq = _∙_ (p ∙ ! q) , ∙-is-eq A a₁ a₂ a₁ (p ∙ ! q)
p-q : PathOver _ (ua eq) q p
p-q = ↓-idf-ua-in _ (–> eq q =⟨ idp ⟩
(p ∙ ! q) ∙ q =⟨ ∙-assoc p (! q) q ⟩
p ∙ ! q ∙ q =⟨ (ap (_∙_ p) (!-inv-l q)) ∙ ∙-unit-r _ ⟩
p ∎)
-- As an example, take any type X with any point x. The path space
-- x == x is trivially inhabited.
module example-path {i} (X : Type i) (x : X) where
open hom-myst (x == x , idp)
open path-hom X x x idp
myst-path = myst is-hom
-- again, the identity map on the path space can be factored through
-- ∣_∣, and we have never assumed that X is an h-set.
id-factored : (x == x) → (x == x)
id-factored = myst-path ∘ ∣_∣
proof : (p : x == x) → id-factored p == p
proof p = idp
proof' : id-factored == idf (x == x)
proof' = λ= proof
{- Let us go back to the example with natural numbers. The term 'myst'
can be used to reveal a secret that was hidden with ∣_∣. -}
module _ where
open example-ℕ
-- let us hide a number
module _ where
private
-- a hidden number:
seventeen : ℕ
seventeen = 17
-- a hidden number that is not even an actual number:
postulate a : ℕ
-- to the outside, only the truncated versions are revealed.
hidden₁ : ∥ ℕ ∥
hidden₁ = ∣ seventeen ∣
hidden₂ : ∥ ℕ ∥
hidden₂ = ∣ a ∣
-- It is impossble to refer to seventeen and a as they are
-- not visible any more. We can still reveal their secrets.
reveal : ℕ
reveal = myst-ℕ hidden₁
uncover : ℕ
uncover = myst-ℕ hidden₂
{- In Agda, we can normalize an expression with ctrl-c ctrl-n.
As it should be, we cannot check seventeen and a:
ctrl-c ctrl-n seventeen
result: [...] not in scope [...]
ctrl-c ctrl-n a
result: [...] not in scope [...]
However, I can still reveal the hidden information:
ctrl-c ctrl-n reveal
result: 17
ctrl-c ctrl-n uncover
result: .trunc-inverse._._.a
-}
\end{code}
The crux is, of course, that the type of 'myst' is not
∥ X ∥ → X. In fact, the type of 'myst' is rather complicated',
and it was already given above:
myst : (x : ∥ X ∥) → (fst ∘ fst ∘ f-lifted) x
The reason why the whole construction works is that, whenever x
is instantiated with ∣ a ∣ (which are actually the only elements
of ∥ X ∥ that we have), the expression in the "codomain" of myst
reduces to X (and, in particular, does not depend on ∣ a ∣).
Further, note that the term 'myst' is independent of the proof
that X is homogeneous. We can thus reveal information that was
hidden by ∣_∣ for any type. In general, we will not be able to
close all holes as we cannot show that an arbitrary type is
homogeneous, but the secret will be revealed nevertheless.