{-

Based on Nicolai Kraus' blog post:
The Truncation Map |_| : ℕ -> ‖ℕ‖ is nearly Invertible
https://homotopytypetheory.org/2013/10/28/the-truncation-map-_-ℕ-‖ℕ‖-is-nearly-invertible/

Defines [recover], which definitionally satisfies recover ∣ x ∣ ≡ x ([recover∣∣]) for homogeneous types

Also see the follow-up post by Jason Gross:
Composition is not what you think it is! Why “nearly invertible” isn’t.
https://homotopytypetheory.org/2014/02/24/composition-is-not-what-you-think-it-is-why-nearly-invertible-isnt/

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Cubical.HITs.PropositionalTruncation.MagicTrick where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Path
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Pointed.Homogeneous

open import Cubical.HITs.PropositionalTruncation.Base
open import Cubical.HITs.PropositionalTruncation.Properties

module Recover {ℓ} (A∙ : Pointed ℓ) (h : isHomogeneous A∙) where
private
A = typ A∙
a = pt A∙

toEquivPtd : ∥ A ∥ → Σ[ B∙ ∈ Pointed ℓ ] (A , a) ≡ B∙
toEquivPtd = rec (isContr→isProp (isContrSingl _)) (λ x → (A , x) , h x)
private
B∙ : ∥ A ∥ → Pointed ℓ
B∙ tx = fst (toEquivPtd tx)

-- the key observation is that B∙ ∣ x ∣ is definitionally equal to (A , x)
private
obvs : ∀ x → B∙ ∣ x ∣ ≡ (A , x)
obvs x = refl -- try it: C-c C-n B∙ ∣ x ∣ gives (A , x)

-- thus any truncated element (of a homogeneous type) can be recovered by agda's normalizer!

recover : ∀ (tx : ∥ A ∥) → typ (B∙ tx)
recover tx = pt (B∙ tx)

recover∣∣ : ∀ (x : A) → recover ∣ x ∣ ≡ x
recover∣∣ x = refl -- try it: C-c C-n recover ∣ x ∣ gives x

private
-- notice that the following typechecks because typ (B∙ ∣ x ∣) is definitionally equal to to A, but
--  recover : ∥ A ∥ → A does not because typ (B∙ tx) is not definitionally equal to A (though it is
--  judegmentally equal to A by cong typ (snd (toEquivPtd tx)) : A ≡ typ (B∙ tx))
obvs2 : A → A
obvs2 = recover ∘ ∣_∣

-- one might wonder if (cong recover (squash ∣ x ∣ ∣ y ∣)) therefore has type x ≡ y, but thankfully
--  typ (B∙ (squash ∣ x ∣ ∣ y ∣ i)) is *not* A (it's a messy hcomp involving h x and h y)
recover-squash : ∀ x y → -- x ≡ y -- this raises an error
PathP (λ i → typ (B∙ (squash ∣ x ∣ ∣ y ∣ i))) x y
recover-squash x y = cong recover (squash ∣ x ∣ ∣ y ∣)

-- https://bitbucket.org/nicolaikraus/agda/src/e30d70c72c6af8e62b72eefabcc57623dd921f04/trunc-inverse.lagda

private
open import Cubical.Data.Nat
open Recover (ℕ , zero) (isHomogeneousDiscrete discreteℕ)

-- only ∣hidden∣ is exported, hidden is no longer in scope
module _ where
private
hidden : ℕ
hidden = 17

∣hidden∣ : ∥ ℕ ∥
∣hidden∣ = ∣ hidden ∣

-- we can still recover the value, even though agda can no longer see hidden!
test : recover ∣hidden∣ ≡ 17
test = refl -- try it: C-c C-n recover ∣hidden∣ gives 17
--         C-c C-n hidden gives an error

-- Finally, note that the definition of recover is independent of the proof that A is homogeneous. Thus we
--  still can definitionally recover information hidden by ∣_∣ as long as we permit holes. Try replacing
--  isHomogeneousDiscrete discreteℕ above with a hole (?) and notice that everything still works