Truncation magic trick

Magic.agda

{- A simple, general version of Kraus' magic trick, to recover truncated data. -}
{-# OPTIONS --cubical #-}
module Magic where
open import Cubical.Foundations.Everything
open import Cubical.HITs.PropositionalTruncation

-- Let A be an arbitrary type (not necessarily homogeneous).
module _ {ℓ : Level} {A : Type ℓ} where

-- Define a family of contractible types over A using contractibility of singletons.
  fam : ∥ A ∥₁ → TypeOfHLevel ℓ 0
  fam ∣ a ∣₁ = singl a , isContrSingl a
  fam (squash₁ a b i) = isPropHContr (fam a) (fam b) i

-- Now we can seemingly factor the identity map on A through the propositional truncation.
-- The idea is that fam ∣ a ∣₁ is a contractible type, so we can take its centre of contraction.
-- This centre of contraction is (a , refl). So the first component gives us back a.
  magic : A → A
  magic = fst ∘ fst ∘ str ∘ fam ∘ ∣_∣₁

-- magic computes as expected.
  magic≡id : (a : A) → magic a ≡ a
  magic≡id _ = refl

-- An example application.
open import Cubical.Data.Nat

-- We start with some truncated data. Imagine that ℕ is some very complicated type,
-- and we did a lot of work to produce a term hidden : ∥ ℕ ∥₁, where it was not clear
-- how to do without the truncation.
hidden : ∥ ℕ ∥₁
hidden = ∣ 17 ∣₁

-- Now we have un-truncated data!
not-hidden : ℕ
not-hidden = fst (fst (str (fam hidden)))

test : not-hidden ≡ 17
test = refl