untruncate.agda

open import 1Lab.Prelude

open import Data.Nat
open import Data.Dec

module wip.untruncate where

Homogeneous : ∀ {ℓ} → Type ℓ → Type (lsuc ℓ)
Homogeneous T = Σ T λ c → ∀ c′ → Path (Type∙ _) (T , c) (T , c′)

discrete→homogeneous : ∀ {ℓ} {T : Type ℓ} → T → Discrete T → Homogeneous T
discrete→homogeneous {T = T} basep disc =
  basep , λ c′ →
    Σ-pathp (ua (swap.swap basep c′)) (path→ua-pathp _ (swap.to-swaps _ _))
  where module swap (α β : T) where
    to : T → T
    to x with disc x α
    ... | yes a = β
    ... | no ¬x=α with disc x β
    ... | yes x=β = α
    ... | no ¬x=β = x

    to-swaps : to α ≡ β
    to-swaps with disc α α
    ... | yes _ = refl
    ... | no ¬a=a = absurd (¬a=a refl)

    to-invol : ∀ x → to (to x) ≡ x
    to-invol x with disc x α
    to-invol x | yes x=α with disc α β
    to-invol x | yes x=α | yes α=β with disc β α
    to-invol x | yes x=α | yes α=β | yes β=α = β=α ∙ sym x=α
    to-invol x | yes x=α | yes α=β | no ¬β=a = absurd (¬β=a (sym α=β))
    to-invol x | yes x=α | no ¬α=β with disc β α
    to-invol x | yes x=α | no ¬α=β | yes β=α = absurd (¬α=β (sym β=α))
    to-invol x | yes x=α | no ¬α=β | no ¬β=α with disc β β
    to-invol x | yes x=α | no ¬α=β | no ¬β=α | yes β=β = sym x=α
    to-invol x | yes x=α | no ¬α=β | no ¬β=α | no ¬β=β = absurd (¬β=β refl)
    to-invol x | no ¬x=α with disc x β
    to-invol x | no ¬x=α | yes x=β with disc α α
    to-invol x | no ¬x=a | yes x=β | yes α=α = sym x=β
    to-invol x | no ¬x=a | yes x=β | no ¬α=α = absurd (¬α=α refl)
    to-invol x | no ¬x=α | no ¬x=β with disc x α
    to-invol x | no ¬x=α | no ¬x=β | yes x=α = absurd (¬x=α x=α)
    to-invol x | no ¬x=α | no ¬x=β | no ¬x=α′ with disc x β
    to-invol x | no ¬x=α | no ¬x=β | no ¬x=α′ | yes x=β = absurd (¬x=β x=β)
    to-invol x | no ¬x=α | no ¬x=β | no ¬x=α′ | no ¬x=β′ = refl

    swap = Iso→Equiv (to , iso to to-invol to-invol)

module Trick {ℓ} {T : Type ℓ} (h : Homogeneous T) where
  include : T → Singleton {A = Type∙ _} (T , h .fst)
  include x = (_ , x) , h .snd x

  include′ : ∥ T ∥ → Singleton {A = Type∙ _} (T , h .fst)
  include′ = ∥-∥-rec (is-contr→is-prop (contr _ Singleton-is-contr)) include

  Untruncate : ∥ T ∥ → Type _
  Untruncate x = include′ x .fst .fst

  untruncate : (x : ∥ T ∥) → Untruncate x
  untruncate x = include′ x .fst .snd

open Trick (discrete→homogeneous 0 Discrete-Nat)

_ : untruncate (inc 123) ≡ 123
_ = refl