```------------------------------------------------------------------------
-- Propositional truncation
------------------------------------------------------------------------

{-# OPTIONS --erased-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 Accessibility equality-with-J as A using (Acc)
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.Path-split equality-with-J as PS
using (Is-∞-extendable-along-[_]; _-Null_)
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; Dec-Erased; Very-stableᴱ-≡; Erased-singleton)
import Erased.Stability equality-with-J as ES
open import Extensionality equality-with-J
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 Modality.Basics equality-with-J
import Nat equality-with-J as Nat
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

------------------------------------------------------------------------
-- The type constructor and some eliminators

-- 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} {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 lemma

-- A map function.

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

------------------------------------------------------------------------
-- The axiom of choice, and the axiom of countable choice

-- 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) _ _
}

------------------------------------------------------------------------
-- Propositional truncation is an accessible modality

-- Propositional truncation is a modality.
--
-- This proof is based on "Modalities in Homotopy Type Theory" by
-- Rijke, Shulman and Spitters.

∥∥-modality : Modality ℓ
∥∥-modality {ℓ} = λ where
.◯                   → ∥_∥
.η                   → ∣_∣
.Modal               → Is-proposition
.Modal-propositional → λ ext → H-level-propositional ext 1
.Modal-◯             → truncation-is-proposition
.Modal-respects-≃    → H-level-cong _ 1
.extendable-along-η  → extendable
where
open Modality

extendable :
{A : Type ℓ} {P : ∥ A ∥ → Type ℓ} →
(∀ x → Is-proposition (P x)) →
Is-∞-extendable-along-[ ∣_∣ ] P
extendable {A} {P} =
(∀ x → Is-proposition (P x))                          →⟨ (λ prop →
_≃_.is-equivalence \$
Eq.↔→≃
_
(elim _ prop)
refl
(λ f → ⟨ext⟩ \$
elim
_
(⇒≡ 1 ∘ prop)
(λ _ → refl _))) ⟩
Is-equivalence (λ (f : (x : ∥ A ∥) → P x) → f ∘ ∣_∣)  ↔⟨ inverse \$ PS.Is-∞-extendable-along≃Is-equivalence ext ⟩□
Is-∞-extendable-along-[ ∣_∣ ] P                       □

-- The propositional truncation modality is accessible.
--
-- This proof is based on "Modalities in Homotopy Type Theory" by
-- Rijke, Shulman and Spitters.

∥∥-accessible : Accessible (∥∥-modality {ℓ = ℓ})
∥∥-accessible {ℓ} =
↑ ℓ ⊤
, (λ _ → ↑ ℓ Bool)
, (λ A →
Is-proposition A                                 ↝⟨ record { from = from; to = to } ⟩
(λ (_ : ↑ ℓ ⊤) → ↑ ℓ Bool) -Null A               ↔⟨ inverse \$ PS.Π-Is-∞-extendable-along≃Null ext ⟩□
(↑ ℓ ⊤ → Is-∞-extendable-along-[ _ ] (λ _ → A))  □)

where
to : Is-proposition A → (λ (_ : ↑ ℓ ⊤) → ↑ ℓ Bool) -Null A
to prop _ =
_≃_.is-equivalence \$
Eq.⇔→≃
prop
(Π-closure ext 1 λ _ → prop)
_
(_\$ lift true)

from : (λ (_ : ↑ ℓ ⊤) → ↑ ℓ Bool) -Null A → Is-proposition A
from {A} null x y =
x                                           ≡⟨⟩
case true ⦂ Bool of if_then x else y        ≡⟨ cong (_\$ true) \$ sym \$ EB→.right-inverse-of _ ⟩
EB→.to (EB→.from (if_then x else y)) true   ≡⟨⟩
EB→.from (if_then x else y)                 ≡⟨⟩
EB→.to (EB→.from (if_then x else y)) false  ≡⟨ cong (_\$ false) \$ EB→.right-inverse-of _ ⟩
case false ⦂ Bool of if_then x else y       ≡⟨⟩
y                                           ∎
where
≃Bool→ : A ≃ (Bool → A)
≃Bool→ =
A               ↝⟨ Eq.⟨ _ , null _ ⟩ ⟩
(↑ ℓ Bool → A)  ↝⟨ Eq.↔→≃ (_∘ lift) (_∘ lower) refl refl ⟩□
(Bool → A)      □

module EB→ = _≃_ ≃Bool→

-- The propositional truncation modality is empty-modal.

∥∥-empty-modal : Empty-modal (∥∥-modality {ℓ = ℓ})
∥∥-empty-modal = ⊥-propositional

-- The modality is not left exact.
--
-- This result is mentioned by Rijke, Shulman and Spitters in
-- "Modalities in Homotopy Type Theory".

¬-∥∥-left-exact : ¬ Left-exact (∥_∥ {a = a})
¬-∥∥-left-exact {a} =
Empty-modal→Is-proposition-◯→¬-Left-exact
∥∥-empty-modal truncation-is-proposition
where
open Modality (∥∥-modality {ℓ = a})

-- The modality is not very modal.

¬-∥∥-very-modal : ¬ Very-modal (∥∥-modality {ℓ = ℓ})
¬-∥∥-very-modal {ℓ} =
Very-modal (∥∥-modality {ℓ = ℓ})       ↔⟨⟩
({A : Type ℓ} → ∥ Is-proposition A ∥)  →⟨ (λ hyp → hyp) ⟩
∥ Is-proposition (↑ ℓ Bool) ∥          →⟨ ◯-map (⊥-elim ∘ ¬-Bool-propositional ∘ H-level-cong _ 1 Bijection.↑↔) ⟩
∥ ⊥ ∥                                  →⟨ ⊥-elim ∘ Modal→Stable ∥∥-empty-modal ⟩□
⊥                                      □
where
open Modality (∥∥-modality {ℓ = ℓ})

-- The modality is W-modal.

∥∥-W-modal : W-modal (∥∥-modality {ℓ = ℓ})
∥∥-W-modal = W-closure ext 0

-- The modality is not accessibility-modal.

¬-∥∥-accessibility-modal :
¬ Modality.Accessibility-modal (∥∥-modality {ℓ = ℓ})
¬-∥∥-accessibility-modal {ℓ} =
Is-proposition-◯→¬-Accessibility-modal
truncation-is-proposition
where
open Modality (∥∥-modality {ℓ = ℓ})

-- The modality is accessibility-modal for propositional types and
-- relations.

Is-proposition→∥∥-accessibility-modal :
{A : Type ℓ} {_<_ : A → A → Type ℓ} →
Is-proposition A →
(∀ x y → Is-proposition (x < y)) →
Modality.Accessibility-modal-for ∥∥-modality _<_
Is-proposition→∥∥-accessibility-modal {ℓ} p₁ p₂ =
(λ acc →
Modal→Acc→Acc-[]◯-η
p₁
(rec′ λ where
.∣∣ʳ                        → id
.truncation-is-propositionʳ → p₂ _ _)
acc)
, (rec′ λ where
.∣∣ʳ                        → id
.truncation-is-propositionʳ → A.Acc-propositional ext)
where
open Modality (∥∥-modality {ℓ = ℓ})

-- If the modality is accessibility-modal for all relations for a
-- type A, then all values of type A are not not equal.

∥∥-accessibility-modal→¬¬≡ :
{x y : A} →
({_<_ : A → A → Type ℓ} →
Modality.Accessibility-modal-for ∥∥-modality _<_) →
¬ ¬ x ≡ y
∥∥-accessibility-modal→¬¬≡ {ℓ} {A} {x} {y} acc x≢y =
\$⟨ (A.acc λ _ x≡y → ⊥-elim \$ x≢y x≡y) ⟩
Acc _<_ x              →⟨ Acc-[]◯-η acc ⟩
Acc _[ _<_ ]◯_ ∣ x ∣   →⟨ (λ acc →
A.Acc-map
(λ _ → ∣ y , y
, truncation-is-proposition _ _
, truncation-is-proposition _ _
, refl _
∣)
acc) ⟩
Acc (λ _ _ → ⊤) ∣ x ∣  →⟨ A.<→¬-Acc _ ⟩□
⊥                      □
where
open Modality (∥∥-modality {ℓ = ℓ})

_<_ : A → A → Type ℓ
_ < z = z ≡ y

-- The modality commutes with Σ.

∥∥-commutes-with-Σ : Modality.Commutes-with-Σ (∥∥-modality {ℓ = ℓ})
∥∥-commutes-with-Σ = Modality.commutes-with-Σ ∥∥-modality ext

-- If the axiom of choice holds, then the modality has choice for
-- families over sets.

∥∥-has-choice-for-sets :
{A : Type ℓ} →
Axiom-of-choice ℓ ℓ →
Is-set A →
Modality.Has-choice-for (∥∥-modality {ℓ = ℓ}) A
∥∥-has-choice-for-sets choice set =
_≃_.from (Has-choice-for≃Is-equivalence-◯Π→Π◯ ext) \$
_≃_.is-equivalence \$
Eq.with-other-function
(from-bijection \$ inverse \$ choice-bijection choice set)
_
(λ _ → (Π-closure ext 1 λ _ →
truncation-is-proposition)
_ _)
where
open Modality ∥∥-modality

-- If the axiom of countable choice holds, then the modality has
-- choice for families over ℕ (lifted).

∥∥-has-choice-for-ℕ :
Axiom-of-countable-choice ℓ →
Modality.Has-choice-for (∥∥-modality {ℓ = ℓ}) (↑ ℓ ℕ)
∥∥-has-choice-for-ℕ choice =
_≃_.from (Has-choice-for≃Is-equivalence-◯Π→Π◯ ext) λ {P = P} →
_≃_.is-equivalence \$
Eq.with-other-function
(∥ ((n : ↑ _ ℕ) → P n) ∥     ↝⟨ (◯-cong-≃ \$ Π-cong ext Bijection.↑↔ λ _ → F.id) ⟩
∥ ((n : ℕ) → P (lift n)) ∥  ↔⟨ inverse \$ countable-choice-bijection choice ⟩
((n : ℕ) → ∥ P (lift n) ∥)  ↝⟨ (Π-cong ext (inverse Bijection.↑↔) λ _ → F.id) ⟩□
((n : ↑ _ ℕ) → ∥ P n ∥)     □)
_
(λ _ → (Π-closure ext 1 λ _ →
truncation-is-proposition)
_ _)
where
open Modality ∥∥-modality

------------------------------------------------------------------------
-- Various lemmas

-- 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.∣_∣)

-- One can convert from Dec ∥ A ∥ᴱ to Dec-Erased ∥ A ∥.

Dec-∥∥ᴱ→Dec-Erased-∥∥ : Dec ∥ A ∥ᴱ → Dec-Erased ∥ A ∥
Dec-∥∥ᴱ→Dec-Erased-∥∥ =
E.Dec→Dec-Erased ∘ Dec-map₀ ∥∥ᴱ→∥∥ (_≃_.from ∥∥ᴱ≃∥∥)

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} = 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} =
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.

_
(λ _ → ⇒≡ 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} =
(∀ 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} =
(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 _

-- A variant of ∥∥×≃.

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

_ : _≃_.right-inverse-of Erased-∥∥×≃ 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
_ _
}

-- A zip function.

∥∥-zip : (A → B → C) → ∥ A ∥ → ∥ B ∥ → ∥ C ∥
∥∥-zip {A} {B} {C} f = curry
(∥ A ∥ × ∥ B ∥  ↔⟨ ∥∥×∥∥↔∥×∥ ⟩
∥ A × B ∥      →⟨ ∥∥-map (uncurry f) ⟩□
∥ C ∥          □)

-- 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} {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∥ → 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} = 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} {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} {B} f = Eq.⇔→≃
(Is-equivalence-propositional ext)
(Is-equivalence-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} {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} {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} = 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 is decided (with erased proofs), then ∥ A ∥ is decided (with
-- erased proofs).

Dec-Erased→Dec-Erased-∥∥ : Dec-Erased A → Dec-Erased ∥ A ∥
Dec-Erased→Dec-Erased-∥∥ {A} =
Dec-Erased A        →⟨ E.Dec-Erased↔Dec-Erased _ ⟩
Dec (Erased A)      →⟨ Dec→Dec-∥∥ ⟩
Dec ∥ Erased A ∥    →⟨ Dec-map₀
(rec′ λ where
.Rec′.∣∣ʳ →
E.map ∣_∣
.Rec′.truncation-is-propositionʳ →
E.H-level-Erased 1 truncation-is-proposition)
(λ (E.[ x ]) → ∥∥-map E.[_]→ x) ⟩
Dec (Erased ∥ A ∥)  →⟨ _⇔_.from (E.Dec-Erased↔Dec-Erased _) ⟩□
Dec-Erased ∥ A ∥    □

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

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

-- A variant of ΠΠ-Dec→ΠΠ-Dec-∥∥ for Dec-Erased.

ΠΠ-Dec-Erased→ΠΠ-Dec-Erased-∥∥ :
{P : A → B → Type p} →
((x : A) (y : B) → Dec-Erased (P x y)) →
((x : A) (y : B) → Dec-Erased ∥ P x y ∥)
ΠΠ-Dec-Erased→ΠΠ-Dec-Erased-∥∥ dec =
λ x y → Dec-Erased→Dec-Erased-∥∥ (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

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

Dec→Erased-∥∥⇔ : Dec A → Erased ∥ A ∥ ⇔ A
Dec→Erased-∥∥⇔ {A} dec =
Erased ∥ A ∥  ↝⟨ record { to = E.Dec→Stable (Dec→Dec-∥∥ dec); from = E.[_]→ } ⟩
∥ A ∥         ↝⟨ Dec→∥∥⇔ dec ⟩□
A             □

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

Dec→∥Erased∥⇔ : Dec A → ∥ Erased A ∥ ⇔ A
Dec→∥Erased∥⇔ {A} dec =
∥ Erased A ∥  ↝⟨ Dec→∥∥⇔ (E.Dec-Erased↔Dec-Erased _ (E.Dec→Dec-Erased dec)) ⟩
Erased A      ↝⟨ record { to = E.Dec→Stable dec; from = E.[_]→ } ⟩□
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} {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} {B} {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} {b} {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} {b} {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 _

------------------------------------------------------------------------
-- 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} {B} =
A ∥⊎∥ B      ↝⟨ ∥⊎∥-comm ⟩
B ∥⊎∥ A      ↝⟨ truncate-left-∥⊎∥ ⟩
∥ B ∥ ∥⊎∥ A  ↝⟨ ∥⊎∥-comm ⟩□
A ∥⊎∥ ∥ B ∥  □

-- _∥⊎∥_ is associative.

∥⊎∥-assoc : A ∥⊎∥ (B ∥⊎∥ C) ↔ (A ∥⊎∥ B) ∥⊎∥ C
∥⊎∥-assoc {A} {B} {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-prop =
∥ ⊥ ⊎ A ∥  ↝⟨ ∥∥-cong ⊎-left-identity ⟩
∥ A ∥      ↝⟨ ∥∥↔ A-prop ⟩□
A          □

∥⊎∥-right-identity : Is-proposition A → A ∥⊎∥ ⊥ {ℓ = ℓ} ↔ A
∥⊎∥-right-identity {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-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} {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} {B} {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} {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} {B} {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} {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} {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} {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} {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                                                      ∎

------------------------------------------------------------------------
-- Some properties that hold for Erased do not hold for every
-- accessible modality

-- It is not the case that, for all types A, ∥ Is-proposition A ∥
-- holds.
--
-- Compare with Erased.Stability.Erased-Very-stable.

¬∥Is-proposition∥ : ¬ ({A : Type a} → ∥ Is-proposition A ∥)
¬∥Is-proposition∥ {a} =
({A : Type a} → ∥ Is-proposition A ∥)  →⟨ (λ hyp → hyp) ⟩
∥ Is-proposition (↑ a Bool) ∥          →⟨ ∥∥-map (H-level-cong _ 1 Bijection.↑↔) ⟩
∥ Is-proposition Bool ∥                →⟨ ∥∥-map ¬-Bool-propositional ⟩
∥ ⊥ ∥                                  ↔⟨ ∥∥↔ ⊥-propositional ⟩□
⊥                                      □

-- It is not the case that, for all types A and B and functions
-- f : A → B, "f is ∥∥-connected" implies ∥ Is-equivalence f ∥.

¬[∥∥-connected→∥Is-equivalence∥] :
¬ ({A : Type a} {B : Type b} {f : A → B} →
(∀ y → Contractible ∥ f ⁻¹ y ∥) → ∥ Is-equivalence f ∥)
¬[∥∥-connected→∥Is-equivalence∥] hyp =
\$⟨ (λ _ → ∣ lift true , refl _ ∣) ⟩

((y : ↑ _ ⊤) → ∥ (const (lift tt) ⦂ (↑ _ Bool → ↑ _ ⊤)) ⁻¹ y ∥)  →⟨ (∀-cong _ λ _ →
propositional⇒inhabited⇒contractible truncation-is-proposition) ⟩
((y : ↑ _ ⊤) →
Contractible ∥ (const (lift tt) ⦂ (↑ _ Bool → ↑ _ ⊤)) ⁻¹ y ∥)   →⟨ hyp ⟩

∥ Is-equivalence (const (lift tt) ⦂ (↑ _ Bool → ↑ _ ⊤)) ∥        ↔⟨ ∥∥↔ (Is-equivalence-propositional ext) ⟩

Is-equivalence (const (lift tt) ⦂ (↑ _ Bool → ↑ _ ⊤))            →⟨ Eq.⟨ _ ,_⟩ ⟩

↑ _ Bool ≃ ↑ _ ⊤                                                 →⟨ (λ eq → Eq.↔⇒≃ Bijection.↑↔ F.∘ eq F.∘ Eq.↔⇒≃ (inverse Bijection.↑↔)) ⟩

Bool ≃ ⊤                                                         →⟨ (λ eq → H-level-cong _ 1 (inverse eq) (mono₁ 0 ⊤-contractible)) ⟩

Is-proposition Bool                                              →⟨ ¬-Bool-propositional ⟩□

⊥                                                                □

-- It is not the case that, for all types A and B and functions
-- f : A → B, "f is ∥∥-connected" is equivalent to
-- ∥ Is-equivalence f ∥.
--
-- Compare with
-- Erased.Level-1.[]-cong₂-⊔.Erased-connected↔Erased-Is-equivalence.

¬[∥∥-connected≃∥Is-equivalence∥] :
¬ ({A : Type a} {B : Type b} {f : A → B} →
(∀ y → Contractible ∥ f ⁻¹ y ∥) ≃ ∥ Is-equivalence f ∥)
¬[∥∥-connected≃∥Is-equivalence∥] hyp =
¬[∥∥-connected→∥Is-equivalence∥] (_≃_.to hyp)

-- If (x : A) → ∥ P x ∥ implies ∥ ((x : A) → P x) ∥ for all types A
-- and type families P over A, then the axiom of choice holds.

[Π∥∥→∥Π∥]→Axiom-of-choice :
({A : Type a} {P : A → Type p} →
((x : A) → ∥ P x ∥) → ∥ ((x : A) → P x) ∥) →
Axiom-of-choice a p
[Π∥∥→∥Π∥]→Axiom-of-choice hyp = λ _ → hyp

-- If ∥ ((x : A) → P x) ∥ is isomorphic to (x : A) → ∥ P x ∥ for all
-- types A and type families P over A, then the axiom of choice holds.
--
-- Compare with Erased.Level-1.Erased-Π↔Π.

[∥Π∥↔Π∥∥]→Axiom-of-choice :
({A : Type a} {P : A → Type p} →
∥ ((x : A) → P x) ∥ ↔ ((x : A) → ∥ P x ∥)) →
Axiom-of-choice a p
[∥Π∥↔Π∥∥]→Axiom-of-choice hyp =
[Π∥∥→∥Π∥]→Axiom-of-choice (_↔_.from hyp)

-- If ∥ A ∥ → ∥ B ∥ implies ∥ (A → B) ∥ for all types A and B in the
-- same universe, then ∥ (∥ A ∥ → A) ∥ holds for every type A in this
-- universe. This is a variant of the axiom of choice of which Kraus
-- et al. state that "We expect that this makes it possible to show
-- that, in MLTT with weak propositional truncation, [a logically
-- equivalent variant of the axiom] is not derivable" (see "Notions of
-- Anonymous Existence in Martin-Löf Type Theory").

[[∥∥→∥∥]→∥→∥]→Axiom-of-choice :
({A B : Type a} → (∥ A ∥ → ∥ B ∥) → ∥ (A → B) ∥) →
({A : Type a} → ∥ (∥ A ∥ → A) ∥)
[[∥∥→∥∥]→∥→∥]→Axiom-of-choice hyp {A} =
\$⟨ rec truncation-is-proposition id ⟩
(∥ ∥ A ∥ ∥ → ∥ A ∥)  →⟨ hyp ⟩□
∥ (∥ A ∥ → A) ∥      □

-- If ∥ (A → B) ∥ is isomorphic to ∥ A ∥ → ∥ B ∥ for all types A and B
-- in the same universe, then ∥ (∥ A ∥ → A) ∥ holds for every type A
-- in this universe. This is a variant of the axiom of choice of which
-- Kraus et al. state that "We expect that this makes it possible to
-- show that, in MLTT with weak propositional truncation, [a logically
-- equivalent variant of the axiom] is not derivable" (see "Notions of
-- Anonymous Existence in Martin-Löf Type Theory").
--
-- Compare with Erased.Level-1.Erased-Π↔Π-Erased.

[∥→∥↔[∥∥→∥∥]]→Axiom-of-choice :
({A B : Type a} → ∥ (A → B) ∥ ↔ (∥ A ∥ → ∥ B ∥)) →
({A : Type a} → ∥ (∥ A ∥ → A) ∥)
[∥→∥↔[∥∥→∥∥]]→Axiom-of-choice hyp =
[[∥∥→∥∥]→∥→∥]→Axiom-of-choice (_↔_.from hyp)

-- It is not the case that, for every type A, if A is Is-proposition,
-- then A is (λ (A : Type a) → Is-proposition A)-null.

¬[Is-proposition→Is-proposition-Null] :
¬ ({A : Type a} →
Is-proposition A → (λ (A : Type a) → Is-proposition A) -Null A)
¬[Is-proposition→Is-proposition-Null] hyp =                     \$⟨ ⊥-propositional ⟩
Is-proposition ⊥                                              →⟨ hyp ⟩
(∀ A → Is-equivalence (const ⦂ (⊥ → Is-proposition A → ⊥)))   →⟨ _\$ _ ⟩
Is-equivalence (const ⦂ (⊥ → Is-proposition (↑ _ Bool) → ⊥))  →⟨ Eq.⟨ _ ,_⟩ ⟩
⊥ ≃ (Is-proposition (↑ _ Bool) → ⊥)                           →⟨ →-cong ext
(Eq.↔⇒≃ \$ inverse \$
Bijection.⊥↔uninhabited (¬-Bool-propositional ∘ ↑⁻¹-closure 1))
Eq.id F.∘_ ⟩
⊥ ≃ (⊥₀ → ⊥)                                                  →⟨ Π⊥↔⊤ ext F.∘_ ⟩
⊥ ≃ ⊤                                                         →⟨ (λ eq → ⊥-elim \$ _≃_.from eq _) ⟩□
⊥                                                             □

-- It is not the case that, for every type A, there is an equivalence
-- between "A is Is-proposition" and
-- (λ (A : Type a) → Is-proposition A) -Null A.
--
-- Compare with Erased.Stability.Very-stable≃Very-stable-Null.

¬[Is-proposition≃Is-proposition-Null] :
¬ ({A : Type a} →
Is-proposition A ≃ (λ (A : Type a) → Is-proposition A) -Null A)
¬[Is-proposition≃Is-proposition-Null] hyp =
¬[Is-proposition→Is-proposition-Null] (_≃_.to hyp)

-- It is not the case that, for every type A : Type a and proof of
-- Extensionality a a, there is an equivalence between "A is
-- Is-proposition" and (λ (A : Type a) → Is-proposition A) -Null A.
--
-- Compare with Erased.Stability.Very-stable≃Very-stable-Null.

¬[Is-proposition≃Is-proposition-Null]′ :
¬ ({A : Type a} →
Extensionality a a →
Is-proposition A ≃ (λ (A : Type a) → Is-proposition A) -Null A)
¬[Is-proposition≃Is-proposition-Null]′ hyp =
¬[Is-proposition≃Is-proposition-Null] (hyp ext)
```