------------------------------------------------------------------------
-- Propositional truncation
------------------------------------------------------------------------

{-# OPTIONS --cubical --safe #-}

-- Partly following the HoTT book.

-- The module is parametrised by a notion of equality. The higher
-- constructor of the HIT defining the propositional truncation uses
-- path equality, but the supplied notion of equality is used for many
-- other things.

import Equality.Path as P

module H-level.Truncation.Propositional
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq hiding (elim)

open import Dec
open import Prelude
open import Logical-equivalence using (_⇔_)

open import Bijection equality-with-J as Bijection using (_↔_)
open import Embedding equality-with-J as Embedding hiding (id; _∘_)
open import Equality.Decidable-UIP equality-with-J
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq
  using (_≃_; Is-equivalence)
open import Equivalence.Erased equality-with-J using (_≃ᴱ_)
open import Equivalence.Erased.Contractible-preimages equality-with-J
  as ECP using (_⁻¹ᴱ_)
open import Equivalence-relation equality-with-J
open import Erased.Cubical eq as E
  using (Erased; erased; Very-stableᴱ-≡; Erased-singleton)
import Erased.Stability equality-with-J as ES
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level equality-with-J as H-level
open import H-level.Closure equality-with-J
import H-level.Truncation.Church equality-with-J as Trunc
open import H-level.Truncation.Propositional.Erased eq as TE
  using (∥_∥ᴱ; Surjectiveᴱ)
open import Injection equality-with-J using (_↣_)
open import Monad equality-with-J
open import Preimage equality-with-J as Preimage using (_⁻¹_)
open import Surjection equality-with-J as Surjection
  using (_↠_; Split-surjective)

private
  variable
    a b c d p r ℓ       : Level
    A A₁ A₂ B B₁ B₂ C D : Type a
    P Q                 : A → Type p
    R                   : A → A → Type r
    A↠B f k s x y       : A

-- Propositional truncation.

data ∥_∥ (A : Type a) : Type a where
  ∣_∣                        : A → ∥ A ∥
  truncation-is-propositionᴾ : P.Is-proposition ∥ A ∥

-- The truncation produces propositions.

truncation-is-proposition : Is-proposition ∥ A ∥
truncation-is-proposition =
  _↔_.from (H-level↔H-level 1) truncation-is-propositionᴾ

-- A dependent eliminator, expressed using paths.

record Elimᴾ′ {A : Type a} (P : ∥ A ∥ → Type p) : Type (a ⊔ p) where
  no-eta-equality
  field
    ∣∣ʳ : (x : A) → P ∣ x ∣

    truncation-is-propositionʳ :
      (p : P x) (q : P y) →
      P.[ (λ i → P (truncation-is-propositionᴾ x y i)) ] p ≡ q

open Elimᴾ′ public

elimᴾ′ : Elimᴾ′ P → (x : ∥ A ∥) → P x
elimᴾ′ {A = A} {P = P} e = helper
  where
  module E′ = Elimᴾ′ e

  helper : (x : ∥ A ∥) → P x
  helper ∣ x ∣                              = E′.∣∣ʳ x
  helper (truncation-is-propositionᴾ x y i) =
    E′.truncation-is-propositionʳ (helper x) (helper y) i

-- A possibly more useful dependent eliminator, expressed using paths.

record Elimᴾ {A : Type a} (P : ∥ A ∥ → Type p) : Type (a ⊔ p) where
  no-eta-equality
  field
    ∣∣ʳ : (x : A) → P ∣ x ∣

    truncation-is-propositionʳ :
      (x : ∥ A ∥) → P.Is-proposition (P x)

open Elimᴾ public

elimᴾ : Elimᴾ P → (x : ∥ A ∥) → P x
elimᴾ e = elimᴾ′ e′
  where
  module E′ = Elimᴾ e

  e′ : Elimᴾ′ _
  e′ .∣∣ʳ                            = E′.∣∣ʳ
  e′ .truncation-is-propositionʳ _ _ =
    P.heterogeneous-irrelevance E′.truncation-is-propositionʳ

-- A non-dependent eliminator, expressed using paths.

record Recᴾ (A : Type a) (B : Type b) : Type (a ⊔ b) where
  no-eta-equality
  field
    ∣∣ʳ                        : A → B
    truncation-is-propositionʳ : P.Is-proposition B

open Recᴾ public

recᴾ : Recᴾ A B → ∥ A ∥ → B
recᴾ r = elimᴾ e
  where
  module R = Recᴾ r

  e : Elimᴾ _
  e .∣∣ʳ                          = R.∣∣ʳ
  e .truncation-is-propositionʳ _ = R.truncation-is-propositionʳ

-- A dependently typed eliminator.

record Elim′ {A : Type a} (P : ∥ A ∥ → Type p) : Type (a ⊔ p) where
  no-eta-equality
  field
    ∣∣ʳ : (x : A) → P ∣ x ∣

    truncation-is-propositionʳ :
      (x : ∥ A ∥) → Is-proposition (P x)

open Elim′ public

elim′ : Elim′ P → (x : ∥ A ∥) → P x
elim′ e = elimᴾ e′
  where
  module E′ = Elim′ e

  e′ : Elimᴾ _
  e′ .∣∣ʳ                        = E′.∣∣ʳ
  e′ .truncation-is-propositionʳ =
    _↔_.to (H-level↔H-level 1) ∘ E′.truncation-is-propositionʳ

elim :
  (P : ∥ A ∥ → Type p) →
  (∀ x → Is-proposition (P x)) →
  ((x : A) → P ∣ x ∣) →
  (x : ∥ A ∥) → P x
elim _ p f = elim′ λ where
  .∣∣ʳ                        → f
  .truncation-is-propositionʳ → p

-- Primitive "recursion".

record Rec′ (A : Type a) (B : Type b) : Type (a ⊔ b) where
  no-eta-equality
  field
    ∣∣ʳ                        : A → B
    truncation-is-propositionʳ : Is-proposition B

open Rec′ public

rec′ : Rec′ A B → ∥ A ∥ → B
rec′ r = recᴾ r′
  where
  module R = Rec′ r

  r′ : Recᴾ _ _
  r′ .∣∣ʳ                        = R.∣∣ʳ
  r′ .truncation-is-propositionʳ =
    _↔_.to (H-level↔H-level 1) R.truncation-is-propositionʳ

rec : Is-proposition B → (A → B) → ∥ A ∥ → B
rec p f = rec′ λ where
  .∣∣ʳ                        → f
  .truncation-is-propositionʳ → p

-- A map function.

∥∥-map : (A → B) → ∥ A ∥ → ∥ B ∥
∥∥-map f = rec truncation-is-proposition (∣_∣ ∘ f)

-- The propositional truncation defined here is isomorphic to the one
-- defined in H-level.Truncation.Church.

∥∥↔∥∥ :
  ∀ ℓ {a} {A : Type a} →
  ∥ A ∥ ↔ Trunc.∥ A ∥ 1 (a ⊔ ℓ)
∥∥↔∥∥ ℓ = record
  { surjection = record
    { logical-equivalence = record
      { to   = rec (Trunc.truncation-has-correct-h-level 1 ext)
                   Trunc.∣_∣₁
      ; from = lower {ℓ = ℓ} ∘
               Trunc.rec 1
                         (↑-closure 1 truncation-is-proposition)
                         (lift ∘ ∣_∣)
      }
    ; right-inverse-of = λ _ →
        Trunc.truncation-has-correct-h-level 1 ext _ _
    }
  ; left-inverse-of = λ _ → truncation-is-proposition _ _
  }

-- If A is merely inhabited (with erased proofs), then A is merely
-- inhabited.

∥∥ᴱ→∥∥ : ∥ A ∥ᴱ → ∥ A ∥
∥∥ᴱ→∥∥ = TE.rec λ where
  .TE.∣∣ʳ                        → ∣_∣
  .TE.truncation-is-propositionʳ → truncation-is-proposition

-- In an erased context the propositional truncation operator defined
-- in H-level.Truncation.Propositional.Erased is equivalent to the one
-- defined here.

@0 ∥∥ᴱ≃∥∥ : ∥ A ∥ᴱ ≃ ∥ A ∥
∥∥ᴱ≃∥∥ = Eq.⇔→≃
  TE.truncation-is-proposition
  truncation-is-proposition
  ∥∥ᴱ→∥∥
  (rec TE.truncation-is-proposition TE.∣_∣)

mutual

  -- If A and B are logically equivalent, then functions of any kind can
  -- be constructed from ∥ A ∥ to ∥ B ∥.

  ∥∥-cong-⇔ : ∀ {k} → A ⇔ B → ∥ A ∥ ↝[ k ] ∥ B ∥
  ∥∥-cong-⇔ A⇔B = ∥∥-cong-⇔′ (∣_∣ ∘ _⇔_.to A⇔B) (∣_∣ ∘ _⇔_.from A⇔B)

  -- A variant of the previous result.

  ∥∥-cong-⇔′ : ∀ {k} → (A → ∥ B ∥) → (B → ∥ A ∥) → ∥ A ∥ ↝[ k ] ∥ B ∥
  ∥∥-cong-⇔′ A→∥B∥ B→∥A∥ =
    from-equivalence $
    Eq.⇔→≃
      truncation-is-proposition
      truncation-is-proposition
      (rec truncation-is-proposition A→∥B∥)
      (rec truncation-is-proposition B→∥A∥)

-- The truncation operator preserves all kinds of functions.

private

  ∥∥-cong-↣ : A ↣ B → ∥ A ∥ ↣ ∥ B ∥
  ∥∥-cong-↣ f = record
    { to        = ∥∥-map (_↣_.to f)
    ; injective = λ _ → truncation-is-proposition _ _
    }

∥∥-cong : A ↝[ k ] B → ∥ A ∥ ↝[ k ] ∥ B ∥
∥∥-cong {k = implication}         = ∥∥-map
∥∥-cong {k = logical-equivalence} = ∥∥-cong-⇔
∥∥-cong {k = surjection}          = ∥∥-cong-⇔ ∘ _↠_.logical-equivalence
∥∥-cong {k = bijection}           = ∥∥-cong-⇔ ∘ from-isomorphism
∥∥-cong {k = equivalence}         = ∥∥-cong-⇔ ∘ from-isomorphism
∥∥-cong {k = equivalenceᴱ}        = ∥∥-cong-⇔ ∘ _≃ᴱ_.logical-equivalence
∥∥-cong {k = injection}           = ∥∥-cong-↣
∥∥-cong {k = embedding}           =
  _↔_.to (↣↔Embedding ext
            (mono₁ 1 truncation-is-proposition)
            (mono₁ 1 truncation-is-proposition)) ∘
  ∥∥-cong-↣ ∘ Embedding.injection

-- A form of idempotence for binary sums.

idempotent : ∥ A ⊎ A ∥ ↔ ∥ A ∥
idempotent = ∥∥-cong-⇔ (record { to = [ id , id ]; from = inj₁ })

-- A generalised flattening lemma.

flatten′ :
  (F : (Type ℓ → Type ℓ) → Type f) →
  (∀ {G H} → (∀ {A} → G A → H A) → F G → F H) →
  (F ∥_∥ → ∥ F id ∥) →
  ∥ F ∥_∥ ∥ ↔ ∥ F id ∥
flatten′ _ map f = record
  { surjection = record
    { logical-equivalence = record
      { to   = rec truncation-is-proposition f
      ; from = ∥∥-map (map ∣_∣)
      }
    ; right-inverse-of = λ _ → truncation-is-proposition _ _
    }
  ; left-inverse-of = λ _ → truncation-is-proposition _ _
  }

-- Nested truncations can be flattened.

flatten : ∥ ∥ A ∥ ∥ ↔ ∥ A ∥
flatten {A = A} = flatten′ (λ F → F A) (λ f → f) id

private

  -- Another flattening lemma, given as an example of how flatten′ can
  -- be used.

  ∥∃∥∥∥↔∥∃∥ : {B : A → Type b} →
              ∥ ∃ (∥_∥ ∘ B) ∥ ↔ ∥ ∃ B ∥
  ∥∃∥∥∥↔∥∃∥ {B = B} =
    flatten′ (λ F → ∃ (F ∘ B))
             (λ f → Σ-map id f)
             (uncurry λ x → ∥∥-map (x ,_))

-- A universe-polymorphic variant of bind.

infixl 5 _>>=′_

_>>=′_ : ∥ A ∥ → (A → ∥ B ∥) → ∥ B ∥
x >>=′ f = _↔_.to flatten (∥∥-map f x)

-- The universe-polymorphic variant of bind is associative.

>>=′-associative :
  (x : ∥ A ∥) {f : A → ∥ B ∥} {g : B → ∥ C ∥} →
  x >>=′ (λ x → f x >>=′ g) ≡ x >>=′ f >>=′ g
>>=′-associative x {f} {g} = elim
  (λ x → x >>=′ (λ x₁ → f x₁ >>=′ g) ≡ x >>=′ f >>=′ g)
  (λ _ → ⇒≡ 1 truncation-is-proposition)
  (λ _ → refl _)
  x

instance

  -- The propositional truncation operator is a monad.

  raw-monad : ∀ {ℓ} → Raw-monad (∥_∥ {a = ℓ})
  Raw-monad.return raw-monad = ∣_∣
  Raw-monad._>>=_  raw-monad = _>>=′_

  monad : ∀ {ℓ} → Monad (∥_∥ {a = ℓ})
  Monad.raw-monad monad           = raw-monad
  Monad.left-identity monad x f   = refl _
  Monad.associativity monad x _ _ = >>=′-associative x
  Monad.right-identity monad      = elim
    _
    (λ _ → ⇒≡ 1 truncation-is-proposition)
    (λ _ → refl _)

-- Surjectivity.

Surjective :
  {A : Type a} {B : Type b} →
  (A → B) → Type (a ⊔ b)
Surjective f = ∀ b → ∥ f ⁻¹ b ∥

-- The property Surjective f is a proposition.

Surjective-propositional : {f : A → B} → Is-proposition (Surjective f)
Surjective-propositional =
  Π-closure ext 1 λ _ →
  truncation-is-proposition

-- In an erased context surjectivity with erased proofs is equivalent
-- to surjectivity.
--
-- It appears to me as if neither direction of this equivalence can be
-- established if the erasure annotation is removed.

@0 Surjectiveᴱ≃Surjective : Surjectiveᴱ f ≃ Surjective f
Surjectiveᴱ≃Surjective {f = f} =
  (∀ y → ∥ f ⁻¹ᴱ y ∥ᴱ)  ↝⟨ (∀-cong ext λ _ → ∥∥ᴱ≃∥∥) ⟩
  (∀ y → ∥ f ⁻¹ᴱ y ∥)   ↝⟨ (∀-cong ext λ _ → ∥∥-cong (inverse ECP.⁻¹≃⁻¹ᴱ)) ⟩□
  (∀ y → ∥ f ⁻¹  y ∥)   □

-- The function ∣_∣ is surjective.

∣∣-surjective : Surjective (∣_∣ {A = A})
∣∣-surjective = elim
  _
  (λ _ → truncation-is-proposition)
  (λ x → ∣ x , refl _ ∣)

-- Split surjective functions are surjective.

Split-surjective→Surjective :
  {f : A → B} → Split-surjective f → Surjective f
Split-surjective→Surjective s = λ b → ∣ s b ∣

-- Being both surjective and an embedding is equivalent to being an
-- equivalence.
--
-- This is Corollary 4.6.4 from the first edition of the HoTT book
-- (the proof is perhaps not quite identical).

surjective×embedding≃equivalence :
  {f : A → B} →
  (Surjective f × Is-embedding f) ≃ Is-equivalence f
surjective×embedding≃equivalence {f = f} =
  (Surjective f × Is-embedding f)          ↔⟨ ∀-cong ext (λ _ → ∥∥↔∥∥ lzero) ×-cong F.id ⟩
  (Trunc.Surjective _ f × Is-embedding f)  ↝⟨ Trunc.surjective×embedding≃equivalence lzero ext ⟩□
  Is-equivalence f                         □

-- If the underlying type is a proposition, then truncations of the
-- type are isomorphic to the type itself.

∥∥↔ : Is-proposition A → ∥ A ∥ ↔ A
∥∥↔ A-prop = record
  { surjection = record
    { logical-equivalence = record
      { to   = rec A-prop id
      ; from = ∣_∣
      }
    ; right-inverse-of = λ _ → refl _
    }
  ; left-inverse-of = λ _ → truncation-is-proposition _ _
  }

-- A type is a proposition if it is equivalent to the propositional
-- truncation of some type.

≃∥∥→Is-proposition : A ≃ ∥ B ∥ → Is-proposition A
≃∥∥→Is-proposition A≃∥B∥ a₁ a₂ =     $⟨ truncation-is-proposition _ _ ⟩
  _≃_.to A≃∥B∥ a₁ ≡ _≃_.to A≃∥B∥ a₂  ↝⟨ Eq.≃-≡ A≃∥B∥ ⟩□
  a₁ ≡ a₂                            □

-- A simple isomorphism involving propositional truncation.

∥∥×↔ : ∥ A ∥ × A ↔ A
∥∥×↔ =
  drop-⊤-left-× λ a →
  _⇔_.to contractible⇔↔⊤ $
    propositional⇒inhabited⇒contractible
      truncation-is-proposition
      ∣ a ∣

-- A variant of ∥∥×↔, introduced to ensure that the right-inverse-of
-- proof is, by definition, simple.

∥∥×≃ : (∥ A ∥ × A) ≃ A
∥∥×≃ = Eq.↔→≃
  proj₂
  (λ x → ∣ x ∣ , x)
  refl
  (λ _ → cong (_, _) (truncation-is-proposition _ _))

_ : _≃_.right-inverse-of ∥∥×≃ x ≡ refl _
_ = refl _

-- ∥_∥ commutes with _×_.

∥∥×∥∥↔∥×∥ : (∥ A ∥ × ∥ B ∥) ↔ ∥ A × B ∥
∥∥×∥∥↔∥×∥ = record
  { surjection = record
    { logical-equivalence = record
      { from = λ p → ∥∥-map proj₁ p , ∥∥-map proj₂ p
      ; to   = λ { (x , y) →
                   rec truncation-is-proposition
                       (λ x → rec truncation-is-proposition
                                  (λ y → ∣ x , y ∣)
                                  y)
                       x }
      }
    ; right-inverse-of = λ _ → truncation-is-proposition _ _
    }
  ; left-inverse-of = λ _ →
      ×-closure 1 truncation-is-proposition
                  truncation-is-proposition
        _ _
  }

-- Variants of proj₁-closure.

private

  H-level-×₁-lemma :
    (A → ∥ B ∥) →
    ∀ n → H-level (suc n) (A × B) → H-level (suc n) A
  H-level-×₁-lemma inhabited n h =
    [inhabited⇒+]⇒+ n λ a →
    rec (H-level-propositional ext (suc n))
        (λ b → proj₁-closure (λ _ → b) (suc n) h)
        (inhabited a)

H-level-×₁ :
  (A → ∥ B ∥) →
  ∀ n → H-level n (A × B) → H-level n A
H-level-×₁ inhabited zero h =
  propositional⇒inhabited⇒contractible
    (H-level-×₁-lemma inhabited 0 (mono₁ 0 h))
    (proj₁ (proj₁ h))
H-level-×₁ inhabited (suc n) =
  H-level-×₁-lemma inhabited n

H-level-×₂ :
  (B → ∥ A ∥) →
  ∀ n → H-level n (A × B) → H-level n B
H-level-×₂ {B = B} {A = A} inhabited n =
  H-level n (A × B)  ↝⟨ H-level.respects-surjection (from-bijection ×-comm) n ⟩
  H-level n (B × A)  ↝⟨ H-level-×₁ inhabited n ⟩□
  H-level n B        □

-- If A is merely inhabited, then the truncation of A is isomorphic to
-- the unit type.

inhabited⇒∥∥↔⊤ : ∥ A ∥ → ∥ A ∥ ↔ ⊤
inhabited⇒∥∥↔⊤ ∥a∥ =
  _⇔_.to contractible⇔↔⊤ $
    propositional⇒inhabited⇒contractible
      truncation-is-proposition
      ∥a∥

-- If A is not inhabited, then the propositional truncation of A is
-- isomorphic to the empty type.

not-inhabited⇒∥∥↔⊥ : ¬ A → ∥ A ∥ ↔ ⊥ {ℓ = ℓ}
not-inhabited⇒∥∥↔⊥ {A = A} =
  ¬ A        ↝⟨ (λ ¬a ∥a∥ → rec ⊥-propositional ¬a ∥a∥) ⟩
  ¬ ∥ A ∥    ↝⟨ inverse ∘ Bijection.⊥↔uninhabited ⟩□
  ∥ A ∥ ↔ ⊥  □

-- The negation of the truncation of A is isomorphic to the negation
-- of A.

¬∥∥↔¬ : ¬ ∥ A ∥ ↔ ¬ A
¬∥∥↔¬ {A = A} = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ f → f ∘ ∣_∣
      ; from = rec ⊥-propositional
      }
    ; right-inverse-of = λ _ → ¬-propositional ext _ _
    }
  ; left-inverse-of = λ _ → ¬-propositional ext _ _
  }

-- The function λ R x y → ∥ R x y ∥ preserves Is-equivalence-relation.

∥∥-preserves-Is-equivalence-relation :
  Is-equivalence-relation R →
  Is-equivalence-relation (λ x y → ∥ R x y ∥)
∥∥-preserves-Is-equivalence-relation R-equiv = record
  { reflexive  = ∣ reflexive ∣
  ; symmetric  = symmetric ⟨$⟩_
  ; transitive = λ p q → transitive ⟨$⟩ p ⊛ q
  }
  where
  open Is-equivalence-relation R-equiv

mutual

  -- The propositional truncation's universal property.

  universal-property :
    Is-proposition B →
    (∥ A ∥ → B) ≃ (A → B)
  universal-property B-prop = universal-property-Π (λ _ → B-prop)

  -- A generalisation of the universal property.

  universal-property-Π :
    (∀ x → Is-proposition (P x)) →
    ((x : ∥ A ∥) → P x) ≃ ((x : A) → P ∣ x ∣)
  universal-property-Π {A = A} {P = P} P-prop =
    ((x : ∥ A ∥) → P x)      ↝⟨ Eq.⇔→≃ prop truncation-is-proposition
                                  (λ f → ∣ f ∘ ∣_∣ ∣) (rec prop (elim _ P-prop)) ⟩
    ∥ ((x : A) → P ∣ x ∣) ∥  ↔⟨ ∥∥↔ (Π-closure ext 1 λ _ → P-prop _) ⟩□
    ((x : A) → P ∣ x ∣)      □
    where
    prop = Π-closure ext 1 λ _ → P-prop _

private

  -- The universal property computes in the right way.

  _ :
    (B-prop : Is-proposition B)
    (f : ∥ A ∥ → B) →
    _≃_.to (universal-property B-prop) f ≡ f ∘ ∣_∣
  _ = λ _ _ → refl _

  _ :
    (B-prop : Is-proposition B)
    (f : A → B) (x : A) →
    _≃_.from (universal-property B-prop) f ∣ x ∣ ≡ f x
  _ = λ _ _ _ → refl _

-- If there is a function f : A → ∥ B ∥, then f is an equivalence if
-- and only if the second projection from A × B is an equivalence.

equivalence-to-∥∥≃proj₂-equivalence :
  (f : A → ∥ B ∥) →
  Is-equivalence f ≃ Is-equivalence (proj₂ ⦂ (A × B → B))
equivalence-to-∥∥≃proj₂-equivalence {A = A} {B = B} f = Eq.⇔→≃
  (Eq.propositional ext _)
  (Eq.propositional ext _)
  (λ eq → _≃_.is-equivalence
            (A × B      ↝⟨ (×-cong₁ λ _ → Eq.⟨ _ , eq ⟩) ⟩
             ∥ B ∥ × B  ↝⟨ ∥∥×≃ ⟩□
             B          □))
  from
  where
  from : Is-equivalence proj₂ → Is-equivalence f
  from eq = _≃_.is-equivalence $ Eq.⇔→≃
    A-prop
    truncation-is-proposition
    _
    (rec A-prop (proj₁ ∘ _≃_.from Eq.⟨ _ , eq ⟩))
    where
    A-prop₁ : B → Is-proposition A
    A-prop₁ b a₁ a₂ =                  $⟨ refl _ ⟩
      b ≡ b                            ↔⟨⟩
      proj₂ (a₁ , b) ≡ proj₂ (a₂ , b)  ↔⟨ Eq.≃-≡ Eq.⟨ _ , eq ⟩ ⟩
      (a₁ , b) ≡ (a₂ , b)              ↝⟨ cong proj₁ ⟩□
      a₁ ≡ a₂                          □

    A-prop : Is-proposition A
    A-prop = [inhabited⇒+]⇒+ 0
      (A                 ↝⟨ f ⟩
       ∥ B ∥             ↝⟨ rec (H-level-propositional ext 1) A-prop₁ ⟩□
       Is-proposition A  □)

-- There is an equivalence between "A is equivalent to ∥ B ∥" and
-- "there is a function from A to ∥ B ∥ and the second projection is
-- an equivalence from A × B to B".

≃∥∥≃→∥∥×proj₂-equivalence :
  (A ≃ ∥ B ∥) ≃ ((A → ∥ B ∥) × Is-equivalence (proj₂ ⦂ (A × B → B)))
≃∥∥≃→∥∥×proj₂-equivalence {A = A} {B = B} =
  A ≃ ∥ B ∥                                           ↔⟨ Eq.≃-as-Σ ⟩
  (∃ λ (f : A → ∥ B ∥) → Is-equivalence f)            ↝⟨ ∃-cong equivalence-to-∥∥≃proj₂-equivalence ⟩□
  (A → ∥ B ∥) × Is-equivalence (proj₂ ⦂ (A × B → B))  □

-- The following three results come from "Generalizations of Hedberg's
-- Theorem" by Kraus, Escardó, Coquand and Altenkirch.

-- Types with constant endofunctions are "h-stable" (meaning that
-- "mere inhabitance" implies inhabitance).

constant-endofunction⇒h-stable : {f : A → A} → Constant f → ∥ A ∥ → A
constant-endofunction⇒h-stable {A = A} {f = f} c =
  ∥ A ∥                    ↝⟨ rec (fixpoint-lemma f c) (λ x → f x , c (f x) x) ⟩
  (∃ λ (x : A) → f x ≡ x)  ↝⟨ proj₁ ⟩□
  A                        □

-- Having a constant endofunction is logically equivalent to being
-- h-stable.

constant-endofunction⇔h-stable :
  (∃ λ (f : A → A) → Constant f) ⇔ (∥ A ∥ → A)
constant-endofunction⇔h-stable = record
  { to = λ { (_ , c) → constant-endofunction⇒h-stable c }
  ; from = λ f → f ∘ ∣_∣ , λ x y →

      f ∣ x ∣  ≡⟨ cong f $ truncation-is-proposition _ _ ⟩∎
      f ∣ y ∣  ∎
  }

-- A type is a set if and only if it is "h-separated" (which means
-- that all its equality types are h-stable).

Is-set⇔h-separated :
  Is-set A ⇔ ((x y : A) → ∥ x ≡ y ∥ → x ≡ y)
Is-set⇔h-separated {A = A} = record
  { to   = λ A-set _ _ → rec A-set id
  ; from =
      ((x y : A) → ∥ x ≡ y ∥ → x ≡ y)                     ↝⟨ (∀-cong _ λ _ → ∀-cong _ λ _ →
                                                              _⇔_.from constant-endofunction⇔h-stable) ⟩
      ((x y : A) → ∃ λ (f : x ≡ y → x ≡ y) → Constant f)  ↝⟨ constant⇒set ⟩□
      Is-set A                                            □
  }

-- If A is decided, then ∥ A ∥ is decided.

Dec→Dec-∥∥ : Dec A → Dec ∥ A ∥
Dec→Dec-∥∥ (yes a) = yes ∣ a ∣
Dec→Dec-∥∥ (no ¬A) = no (_↔_.from ¬∥∥↔¬ ¬A)

-- If a binary relation can be decided, then the propositional
-- truncation of the relation can also be decided.

decidable→decidable-∥∥ :
  {P : A → B → Type p} →
  ((x : A) (y : B) → Dec (P x y)) →
  ((x : A) (y : B) → Dec ∥ P x y ∥)
decidable→decidable-∥∥ dec =
  λ x y → Dec→Dec-∥∥ (dec x y)

-- If A is decided, then one can convert between ∥ A ∥ and A.

Dec→∥∥⇔ :
  Dec A → ∥ A ∥ ⇔ A
Dec→∥∥⇔ _       ._⇔_.from = ∣_∣
Dec→∥∥⇔ (yes a) ._⇔_.to   = λ _ → a
Dec→∥∥⇔ (no ¬A) ._⇔_.to   = ⊥-elim ∘ rec ⊥-propositional ¬A

-- Variants of the following two lemmas were communicated to me by
-- Nicolai Kraus. They are closely related to Lemma 2.1 in his paper
-- "The General Universal Property of the Propositional Truncation".

-- A variant of ∥∥×≃.

drop-∥∥ :
  {B : A → Type b} →
  (A → ∥ C ∥) →
  (∥ C ∥ → ∀ x → B x) ≃ (∀ x → B x)
drop-∥∥ {C = C} {B = B} inh =
  Eq.with-other-inverse
    ((∥ C ∥ → ∀ a → B a)  ↔⟨ Π-comm ⟩
     (∀ a → ∥ C ∥ → B a)  ↝⟨ (∀-cong ext λ a → drop-⊤-left-Π ext (inhabited⇒∥∥↔⊤ (inh a))) ⟩□
     (∀ a → B a)          □)
    (λ f _ → f)
    (λ f → ⟨ext⟩ λ _ → ⟨ext⟩ λ a →
       _    ≡⟨ subst-const _ ⟩∎
       f a  ∎)

-- Another variant of ∥∥×≃.

push-∥∥ :
  {B : A → Type b} {C : (∀ x → B x) → Type c} →
  (A → ∥ D ∥) →
  (∥ D ∥ → ∃ λ (f : ∀ x → B x) → C f) ≃
  (∃ λ (f : ∀ x → B x) → ∥ D ∥ → C f)
push-∥∥ {D = D} {B = B} {C = C} inh =
  (∥ D ∥ → ∃ λ (f : ∀ c → B c) → C f)            ↔⟨ ΠΣ-comm ⟩
  (∃ λ (f : ∥ D ∥ → ∀ c → B c) → ∀ b → C (f b))  ↝⟨ (Σ-cong-contra (inverse $ drop-∥∥ inh) λ _ → F.id) ⟩□
  (∃ λ (f : ∀ c → B c) → ∥ D ∥ → C f)            □

-- Having a coherently constant function into a groupoid is equivalent
-- to having a function from a propositionally truncated type into the
-- groupoid. This result is Proposition 2.3 in "The General Universal
-- Property of the Propositional Truncation" by Kraus.

Coherently-constant :
  {A : Type a} {B : Type b} →
  (A → B) → Type (a ⊔ b)
Coherently-constant f =
  ∃ λ (c : Constant f) →
  ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃

coherently-constant-function≃∥inhabited∥⇒inhabited :
  {A : Type a} {B : Type b} →
  H-level 3 B →
  (∃ λ (f : A → B) → Coherently-constant f) ≃ (∥ A ∥ → B)
coherently-constant-function≃∥inhabited∥⇒inhabited
  {a = a} {b = b} {A = A} {B} B-groupoid =

  (∃ λ (f : A → B) → Coherently-constant f)  ↝⟨ Trunc.coherently-constant-function≃∥inhabited∥⇒inhabited lzero ext B-groupoid ⟩
  (Trunc.∥ A ∥ 1 (a ⊔ b) → B)                ↝⟨ →-cong₁ ext (inverse $ ∥∥↔∥∥ (a ⊔ b)) ⟩□
  (∥ A ∥ → B)                                □

private

  -- One direction of the proposition above computes in the right way.

  to-coherently-constant-function≃∥inhabited∥⇒inhabited :
    (h : H-level 3 B)
    (f : ∃ λ (f : A → B) → Coherently-constant f) (x : A) →
    _≃_.to (coherently-constant-function≃∥inhabited∥⇒inhabited h)
      f ∣ x ∣ ≡
    proj₁ f x
  to-coherently-constant-function≃∥inhabited∥⇒inhabited _ _ _ = refl _

-- Having a constant function into a set is equivalent to having a
-- function from a propositionally truncated type into the set. The
-- statement of this result is that of Proposition 2.2 in "The General
-- Universal Property of the Propositional Truncation" by Kraus, but
-- it uses a different proof: as observed by Kraus this result follows
-- from Proposition 2.3.

constant-function≃∥inhabited∥⇒inhabited :
  {A : Type a} {B : Type b} →
  Is-set B →
  (∃ λ (f : A → B) → Constant f) ≃ (∥ A ∥ → B)
constant-function≃∥inhabited∥⇒inhabited
  {a = a} {b = b} {A = A} {B} B-set =

  (∃ λ (f : A → B) → Constant f)  ↝⟨ Trunc.constant-function≃∥inhabited∥⇒inhabited lzero ext B-set ⟩
  (Trunc.∥ A ∥ 1 (a ⊔ b) → B)     ↝⟨ →-cong₁ ext (inverse $ ∥∥↔∥∥ (a ⊔ b)) ⟩□
  (∥ A ∥ → B)                     □

private

  -- One direction of the proposition above computes in the right way.

  to-constant-function≃∥inhabited∥⇒inhabited :
    (B-set : Is-set B)
    (f : ∃ λ (f : A → B) → Constant f) (x : A) →
    _≃_.to (constant-function≃∥inhabited∥⇒inhabited B-set) f ∣ x ∣ ≡
    proj₁ f x
  to-constant-function≃∥inhabited∥⇒inhabited _ _ _ = refl _

-- The axiom of choice, in one of the alternative forms given in the
-- HoTT book (§3.8).

Axiom-of-choice : (a b : Level) → Type (lsuc (a ⊔ b))
Axiom-of-choice a b =
  {A : Type a} {B : A → Type b} →
  Is-set A → (∀ x → ∥ B x ∥) → ∥ (∀ x → B x) ∥

-- The axiom of choice can be turned into a bijection.

choice-bijection :
  {A : Type a} {B : A → Type b} →
  Axiom-of-choice a b → Is-set A →
  (∀ x → ∥ B x ∥) ↔ ∥ (∀ x → B x) ∥
choice-bijection choice A-set = record
  { surjection = record
    { logical-equivalence = record
      { to   = choice A-set
      ; from = λ f x → ∥∥-map (_$ x) f
      }
    ; right-inverse-of = λ _ → truncation-is-proposition _ _
    }
  ; left-inverse-of = λ _ →
      (Π-closure ext 1 λ _ →
       truncation-is-proposition) _ _
  }

-- The axiom of countable choice, stated in a corresponding way.

Axiom-of-countable-choice : (b : Level) → Type (lsuc b)
Axiom-of-countable-choice b =
  {B : ℕ → Type b} → (∀ x → ∥ B x ∥) → ∥ (∀ x → B x) ∥

-- The axiom of countable choice can be turned into a bijection.

countable-choice-bijection :
  {B : ℕ → Type b} →
  Axiom-of-countable-choice b →
  (∀ x → ∥ B x ∥) ↔ ∥ (∀ x → B x) ∥
countable-choice-bijection cc = record
  { surjection = record
    { logical-equivalence = record
      { to   = cc
      ; from = λ f x → ∥∥-map (_$ x) f
      }
    ; right-inverse-of = λ _ → truncation-is-proposition _ _
    }
  ; left-inverse-of = λ _ →
      (Π-closure ext 1 λ _ →
       truncation-is-proposition) _ _
  }

------------------------------------------------------------------------
-- Definitions related to truncated binary sums

-- Truncated binary sums.

infixr 1 _∥⊎∥_

_∥⊎∥_ : Type a → Type b → Type (a ⊔ b)
A ∥⊎∥ B = ∥ A ⊎ B ∥

-- Introduction rules.

∣inj₁∣ : A → A ∥⊎∥ B
∣inj₁∣ = ∣_∣ ∘ inj₁

∣inj₂∣ : B → A ∥⊎∥ B
∣inj₂∣ = ∣_∣ ∘ inj₂

-- _∥⊎∥_ is pointwise propositional.

∥⊎∥-propositional : Is-proposition (A ∥⊎∥ B)
∥⊎∥-propositional = truncation-is-proposition

-- _∥⊎∥_ preserves all kinds of functions.

infixr 1 _∥⊎∥-cong_

_∥⊎∥-cong_ : A₁ ↝[ k ] A₂ → B₁ ↝[ k ] B₂ → A₁ ∥⊎∥ B₁ ↝[ k ] A₂ ∥⊎∥ B₂
A₁↝A₂ ∥⊎∥-cong B₁↝B₂ = ∥∥-cong (A₁↝A₂ ⊎-cong B₁↝B₂)

-- _∥⊎∥_ is commutative.

∥⊎∥-comm : A ∥⊎∥ B ↔ B ∥⊎∥ A
∥⊎∥-comm = ∥∥-cong ⊎-comm

-- If one truncates the types to the left or right of _∥⊎∥_, then one
-- ends up with an isomorphic type.

truncate-left-∥⊎∥ : A ∥⊎∥ B ↔ ∥ A ∥ ∥⊎∥ B
truncate-left-∥⊎∥ =
  inverse $ flatten′ (λ F → F _ ⊎ _) (λ f → ⊎-map f id) [ ∥∥-map inj₁ , ∣inj₂∣ ]

truncate-right-∥⊎∥ : A ∥⊎∥ B ↔ A ∥⊎∥ ∥ B ∥
truncate-right-∥⊎∥ {A = A} {B = B} =
  A ∥⊎∥ B      ↝⟨ ∥⊎∥-comm ⟩
  B ∥⊎∥ A      ↝⟨ truncate-left-∥⊎∥ ⟩
  ∥ B ∥ ∥⊎∥ A  ↝⟨ ∥⊎∥-comm ⟩□
  A ∥⊎∥ ∥ B ∥  □

-- _∥⊎∥_ is associative.

∥⊎∥-assoc : A ∥⊎∥ (B ∥⊎∥ C) ↔ (A ∥⊎∥ B) ∥⊎∥ C
∥⊎∥-assoc {A = A} {B = B} {C = C} =
  ∥ A ⊎ ∥ B ⊎ C ∥ ∥  ↝⟨ inverse truncate-right-∥⊎∥ ⟩
  ∥ A ⊎ B ⊎ C ∥      ↝⟨ ∥∥-cong ⊎-assoc ⟩
  ∥ (A ⊎ B) ⊎ C ∥    ↝⟨ truncate-left-∥⊎∥ ⟩□
  ∥ ∥ A ⊎ B ∥ ⊎ C ∥  □

-- ⊥ is a left and right identity of _∥⊎∥_ if the other argument is a
-- proposition.

∥⊎∥-left-identity : Is-proposition A → ⊥ {ℓ = ℓ} ∥⊎∥ A ↔ A
∥⊎∥-left-identity {A = A} A-prop =
  ∥ ⊥ ⊎ A ∥  ↝⟨ ∥∥-cong ⊎-left-identity ⟩
  ∥ A ∥      ↝⟨ ∥∥↔ A-prop ⟩□
  A          □

∥⊎∥-right-identity : Is-proposition A → A ∥⊎∥ ⊥ {ℓ = ℓ} ↔ A
∥⊎∥-right-identity {A = A} A-prop =
  A ∥⊎∥ ⊥  ↔⟨ ∥⊎∥-comm ⟩
  ⊥ ∥⊎∥ A  ↔⟨ ∥⊎∥-left-identity A-prop ⟩□
  A        □

-- _∥⊎∥_ is idempotent for propositions.

∥⊎∥-idempotent : Is-proposition A → A ∥⊎∥ A ↔ A
∥⊎∥-idempotent {A = A} A-prop =
  ∥ A ⊎ A ∥  ↝⟨ idempotent ⟩
  ∥ A ∥      ↝⟨ ∥∥↔ A-prop ⟩□
  A          □

-- Sometimes a truncated binary sum is isomorphic to one of its
-- summands.

drop-left-∥⊎∥ :
  Is-proposition B → (A → B) → A ∥⊎∥ B ↔ B
drop-left-∥⊎∥ B-prop A→B =
  _≃_.bijection $
  Eq.⇔→≃ ∥⊎∥-propositional B-prop
    (rec B-prop [ to-implication A→B , id ]) ∣inj₂∣

drop-right-∥⊎∥ :
  Is-proposition A → (B → A) → A ∥⊎∥ B ↔ A
drop-right-∥⊎∥ {A = A} {B = B} A-prop B→A =
  A ∥⊎∥ B  ↝⟨ ∥⊎∥-comm ⟩
  B ∥⊎∥ A  ↝⟨ drop-left-∥⊎∥ A-prop B→A ⟩□
  A        □

drop-⊥-right-∥⊎∥ :
  Is-proposition A → ¬ B → A ∥⊎∥ B ↔ A
drop-⊥-right-∥⊎∥ A-prop ¬B =
  drop-right-∥⊎∥ A-prop (⊥-elim ∘ ¬B)

drop-⊥-left-∥⊎∥ :
  Is-proposition B → ¬ A → A ∥⊎∥ B ↔ B
drop-⊥-left-∥⊎∥ B-prop ¬A =
  drop-left-∥⊎∥ B-prop (⊥-elim ∘ ¬A)

-- A type of functions from a truncated binary sum to a family of
-- propositions can be expressed as a binary product of function
-- types.

Π∥⊎∥↔Π×Π :
  (∀ x → Is-proposition (P x)) →
  ((x : A ∥⊎∥ B) → P x)
    ↔
  ((x : A) → P (∣inj₁∣ x)) × ((y : B) → P (∣inj₂∣ y))
Π∥⊎∥↔Π×Π {A = A} {B = B} {P = P} P-prop =
  ((x : A ∥⊎∥ B) → P x)                                ↔⟨ universal-property-Π P-prop ⟩
  ((x : A ⊎ B) → P ∣ x ∣)                              ↝⟨ Π⊎↔Π×Π ext ⟩□
  ((x : A) → P (∣inj₁∣ x)) × ((y : B) → P (∣inj₂∣ y))  □

-- Two distributivity laws for Σ and _∥⊎∥_.

Σ-∥⊎∥-distrib-left :
  Is-proposition A →
  Σ A (λ x → P x ∥⊎∥ Q x) ↔ Σ A P ∥⊎∥ Σ A Q
Σ-∥⊎∥-distrib-left {P = P} {Q = Q} A-prop =
  (∃ λ x → ∥ P x ⊎ Q x ∥)      ↝⟨ inverse $ ∥∥↔ (Σ-closure 1 A-prop λ _ → ∥⊎∥-propositional) ⟩
  ∥ (∃ λ x → ∥ P x ⊎ Q x ∥) ∥  ↝⟨ flatten′ (λ F → (∃ λ x → F (P x ⊎ Q x))) (λ f → Σ-map id f) (uncurry λ x → ∥∥-map (x ,_)) ⟩
  ∥ (∃ λ x → P x ⊎ Q x) ∥      ↝⟨ ∥∥-cong ∃-⊎-distrib-left ⟩□
  ∥ ∃ P ⊎ ∃ Q ∥                □

Σ-∥⊎∥-distrib-right :
  (∀ x → Is-proposition (P x)) →
  Σ (A ∥⊎∥ B) P ↔ Σ A (P ∘ ∣inj₁∣) ∥⊎∥ Σ B (P ∘ ∣inj₂∣)
Σ-∥⊎∥-distrib-right {A = A} {B = B} {P = P} P-prop =
  _≃_.bijection $
  Eq.⇔→≃ prop₂ prop₁
    (uncurry $
     elim _ (λ _ → Π-closure ext 1 λ _ → prop₁) λ where
       (inj₁ x) y → ∣ inj₁ (x , y) ∣
       (inj₂ x) y → ∣ inj₂ (x , y) ∣)
    (rec prop₂ [ Σ-map ∣inj₁∣ id , Σ-map ∣inj₂∣ id ])
  where
  prop₁ = ∥⊎∥-propositional
  prop₂ = Σ-closure 1 ∥⊎∥-propositional P-prop

-- A variant of one of De Morgan's laws.

¬∥⊎∥¬↔¬× :
  Dec (¬ A) → Dec (¬ B) →
  ¬ A ∥⊎∥ ¬ B ↔ ¬ (A × B)
¬∥⊎∥¬↔¬× {A = A} {B = B} dec-¬A dec-¬B = record
  { surjection = record
    { logical-equivalence = record
      { to   = rec (¬-propositional ext) ¬⊎¬→׬
      ; from = ∣_∣ ∘ _↠_.from (¬⊎¬↠¬× ext dec-¬A dec-¬B)
      }
    ; right-inverse-of = λ _ → ¬-propositional ext _ _
    }
  ; left-inverse-of = λ _ → ∥⊎∥-propositional _ _
  }

-- If ∥ A ∥ is decided, then A ∥⊎∥ B is equivalent to A ∥⊎∥ ¬ A × B.

∥⊎∥≃∥⊎∥¬× :
  Dec ∥ A ∥ →
  (A ∥⊎∥ B) ≃ (A ∥⊎∥ ¬ A × B)
∥⊎∥≃∥⊎∥¬× (yes ∥A∥) = Eq.⇔→≃
  ∥⊎∥-propositional
  ∥⊎∥-propositional
  (const (∥∥-map inj₁ ∥A∥))
  (id ∥⊎∥-cong proj₂)
∥⊎∥≃∥⊎∥¬× (no ¬∥A∥) = Eq.⇔→≃
  ∥⊎∥-propositional
  ∥⊎∥-propositional
  (id ∥⊎∥-cong (¬∥A∥ ∘ ∣_∣) ,_)
  (id ∥⊎∥-cong proj₂)

-- If ∥ B ∥ is decided, then A ∥⊎∥ B is equivalent to ¬ B × A ∥⊎∥ B.

∥⊎∥≃¬×∥⊎∥ :
  Dec ∥ B ∥ →
  (A ∥⊎∥ B) ≃ (¬ B × A ∥⊎∥ B)
∥⊎∥≃¬×∥⊎∥ {B = B} {A = A} dec-∥B∥ =
  A ∥⊎∥ B        ↔⟨ ∥⊎∥-comm ⟩
  B ∥⊎∥ A        ↝⟨ ∥⊎∥≃∥⊎∥¬× dec-∥B∥ ⟩
  B ∥⊎∥ ¬ B × A  ↔⟨ ∥⊎∥-comm ⟩□
  ¬ B × A ∥⊎∥ B  □

------------------------------------------------------------------------
-- Code related to Erased-singleton

-- A corollary of erased-singleton-with-erased-center-propositional.

↠→↔Erased-singleton :
  {@0 y : B}
  (A↠B : A ↠ B) →
  Very-stableᴱ-≡ B →
  ∥ (∃ λ (x : A) → Erased (_↠_.to A↠B x ≡ y)) ∥ ↔ Erased-singleton y
↠→↔Erased-singleton {A = A} {y = y} A↠B s =
  ∥ (∃ λ (x : A) → Erased (_↠_.to A↠B x ≡ y)) ∥  ↝⟨ ∥∥-cong-⇔ (Surjection.Σ-cong-⇔ A↠B λ _ → F.id) ⟩
  ∥ Erased-singleton y ∥                         ↝⟨ ∥∥↔ (E.erased-singleton-with-erased-center-propositional s) ⟩□
  Erased-singleton y                             □

mutual

  -- The right-to-left direction of the previous lemma does not depend
  -- on the assumption of stability.

  ↠→Erased-singleton→ :
    {@0 y : B}
    (A↠B : A ↠ B) →
    Erased-singleton y →
    ∥ (∃ λ (x : A) → Erased (_↠_.to A↠B x ≡ y)) ∥
  ↠→Erased-singleton→ = _  -- Agda can infer the definition.

  _ : _↔_.from (↠→↔Erased-singleton A↠B s) x ≡
      ↠→Erased-singleton→ A↠B x
  _ = refl _

-- A corollary of Σ-Erased-Erased-singleton↔ and ↠→↔Erased-singleton.

Σ-Erased-∥-Σ-Erased-≡-∥↔ :
  (A↠B : A ↠ B) →
  Very-stableᴱ-≡ B →
  (∃ λ (x : Erased B) →
     ∥ (∃ λ (y : A) → Erased (_↠_.to A↠B y ≡ erased x)) ∥) ↔
  B
Σ-Erased-∥-Σ-Erased-≡-∥↔ {A = A} {B = B} A↠B s =
  (∃ λ (x : Erased B) →
     ∥ (∃ λ (y : A) → Erased (_↠_.to A↠B y ≡ erased x)) ∥)  ↝⟨ (∃-cong λ _ → ↠→↔Erased-singleton A↠B s) ⟩

  (∃ λ (x : Erased B) → Erased-singleton (erased x))        ↝⟨ E.Σ-Erased-Erased-singleton↔ ⟩□

  B                                                         □

mutual

  -- Again the right-to-left direction of the previous lemma does not
  -- depend on the assumption of stability.

  →Σ-Erased-∥-Σ-Erased-≡-∥ :
    (A↠B : A ↠ B) →
    B →
    ∃ λ (x : Erased B) →
      ∥ (∃ λ (y : A) → Erased (_↠_.to A↠B y ≡ erased x)) ∥
  →Σ-Erased-∥-Σ-Erased-≡-∥ = _  -- Agda can infer the definition.

  _ : _↔_.from (Σ-Erased-∥-Σ-Erased-≡-∥↔ A↠B s) x ≡
      →Σ-Erased-∥-Σ-Erased-≡-∥ A↠B x
  _ = refl _

-- In an erased context the left-to-right direction of
-- Σ-Erased-∥-Σ-Erased-≡-∥↔ returns the erased first component.

@0 to-Σ-Erased-∥-Σ-Erased-≡-∥↔≡ :
  ∀ (A↠B : A ↠ B) (s : Very-stableᴱ-≡ B) x →
  _↔_.to (Σ-Erased-∥-Σ-Erased-≡-∥↔ A↠B s) x ≡ erased (proj₁ x)
to-Σ-Erased-∥-Σ-Erased-≡-∥↔≡ A↠B s (E.[ x ] , y) =
  _↔_.to (Σ-Erased-∥-Σ-Erased-≡-∥↔ A↠B s) (E.[ x ] , y)  ≡⟨⟩
  proj₁ (_↔_.to (↠→↔Erased-singleton A↠B s) y)           ≡⟨ erased (proj₂ (_↔_.to (↠→↔Erased-singleton A↠B s) y)) ⟩∎
  x                                                      ∎