Solution to some propositional truncation problems :)

EgbertPropTrunc.agda

-- twitter thread: https://twitter.com/EgbertRijke/status/1349865209591173120

{-# OPTIONS --cubical #-}

open import Cubical.HITs.PropositionalTruncation using (∥_∥; ∣_∣; squash; rec)
open import Cubical.Relation.Nullary
open import Cubical.Foundations.Function using (_∘_; idfun)
open import Cubical.Data.Sigma using (_×_; fst; snd)
import Cubical.Data.Empty as ⊥ using (elim)

variable A : Set

infix 1 _<->_
_<->_ : Set -> Set -> Set
A <-> B = (A -> B) × (B -> A)

exA : ∥ A ∥ <-> ∥ ∥ A ∥ ∥
exA .fst a = ∣ a ∣
exA .snd = rec squash (idfun _)

exA' : ∥ ∥ A ∥ ∥ ≡ ∥ A ∥
exA' = propTruncIdempotent propTruncIsProp

exB : Dec ∥ A ∥ <-> ∥ Dec A ∥
exB .fst (yes p) = rec squash (∣_∣ ∘ yes) p
exB .fst (no np) = ∣ no (np ∘ ∣_∣) ∣
exB .snd = rec (isPropDec squash) f where
 f : Dec A → Dec ∥ A ∥
 f (yes p) = yes ∣ p ∣
 f (no np) = no (rec ⊥.elim np)

exC : Dec A -> ∥ A ∥ -> A
exC (yes p) _ = p
exC (no np) = ⊥.elim ∘ rec (\ ()) np

exC' : Dec A -> ∥ A ∥ -> A
exC' d = Dec→Stable d ∘ notEmptyPopulated ∘ populatedBy

-- exD : NonEmpty ∥ A ∥ <-> NonEmpty A
exD : ¬ ¬ ∥ A ∥ <-> ¬ ¬ A
exD .fst p = p ∘ rec (\ ())
exD .snd p x = p (x ∘ ∣_∣)