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.