------------------------------------------------------------------------
-- A variant of the propositional truncation operator with an erased
-- truncation constructor
------------------------------------------------------------------------

-- Partly following the HoTT book, but adapted for erasure.

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

-- The module is parametrised by a notion of equality. The higher
-- constructor of the HIT defining the propositional truncation
-- operator 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.Erased
  {e⁺} (eq :  {a p}  P.Equality-with-paths a p e⁺) where

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

open import Prelude as P
open import Logical-equivalence using (_⇔_)

open import Accessibility equality-with-J as A using (Acc)
open import Bijection equality-with-J as Bijection using (_↔_)
import Colimit.Sequential.Very-erased eq as C
open import Embedding equality-with-J as Emb using (Is-embedding)
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 as EEq
  using (_≃ᴱ_; Is-equivalenceᴱ)
open import Equivalence.Erased.Contractible-preimages equality-with-J
  as ECP using (Contractibleᴱ; _⁻¹ᴱ_)
open import Equivalence.Path-split equality-with-J as PS
  using (Is-∞-extendable-along-[_])
open import Equivalence-relation equality-with-J
open import Erased.Cubical eq as Er
  using (Erased; [_]; erased; Very-stableᴱ-≡; Erased-singleton)
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
open import H-level.Truncation.Propositional.One-step eq as O
  using (∥_∥¹-out-^)
import H-level.Truncation.Propositional.Non-recursive.Erased eq as N
open import Modality.Basics equality-with-J
open import Monad equality-with-J
import Nat equality-with-J as Nat
open import Preimage equality-with-J using (_⁻¹_)
open import Surjection equality-with-J as S
  using (_↠_; Split-surjective)

private
  variable
    a b  p r         : Level
    A A₁ A₂ B B₁ B₂ C : Type a
    P Q               : A  Type p
    R                 : A  A  Type r
    f g k x y         : A

------------------------------------------------------------------------
-- The type former

-- A propositional truncation operator with an erased higher
-- constructor.

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

-- The truncation produces propositions (in erased contexts).

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

------------------------------------------------------------------------
-- Eliminators

-- 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 

    @0 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 

    @0 truncation-is-propositionʳ :
      (x :  A ∥ᴱ)  P.Is-proposition (P x)

open Elimᴾ public

elimᴾ : Elimᴾ P  (x :  A ∥ᴱ)  P x
elimᴾ e = elimᴾ′ λ where
    .∣∣ʳ                             E.∣∣ʳ
    .truncation-is-propositionʳ _ _ 
      P.heterogeneous-irrelevance E.truncation-is-propositionʳ
  where
  module E = Elimᴾ e

-- 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
    @0 truncation-is-propositionʳ : P.Is-proposition B

open Recᴾ public

recᴾ : Recᴾ A B   A ∥ᴱ  B
recᴾ r = elimᴾ λ where
    .∣∣ʳ                           R.∣∣ʳ
    .truncation-is-propositionʳ _  R.truncation-is-propositionʳ
  where
  module R = Recᴾ r

-- 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 

    @0 truncation-is-propositionʳ :
      (x :  A ∥ᴱ)  Is-proposition (P x)

open Elim public

elim : Elim P  (x :  A ∥ᴱ)  P x
elim e = elimᴾ λ where
    .∣∣ʳ                         E.∣∣ʳ
    .truncation-is-propositionʳ 
      _↔_.to (H-level↔H-level 1)  E.truncation-is-propositionʳ
  where
  module E = Elim e

-- Primitive "recursion".

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

open Rec public

rec : Rec A B   A ∥ᴱ  B
rec r = recᴾ λ where
    .∣∣ʳ                         R.∣∣ʳ
    .truncation-is-propositionʳ 
      _↔_.to (H-level↔H-level 1) R.truncation-is-propositionʳ
  where
  module R = Rec r

------------------------------------------------------------------------
-- ∥_∥ᴱ is a modality

-- ∥_∥ᴱ and ∣_∣ form a modality, where a type A is modal if
-- Erased (Is-proposition A) holds.

∥∥ᴱ-modality : Modality 
∥∥ᴱ-modality {} = λ where
    .                    ∥_∥ᴱ
    .η                    ∣_∣
    .Modal A              Erased (Is-proposition A)
    .Modal-propositional  λ ext 
                             Er.H-level-Erased 1
                               (H-level-propositional ext 1)
    .Modal-◯              [ truncation-is-proposition ]
    .Modal-respects-≃     λ A≃B  Er.map (H-level-cong _ 1 A≃B)
    .extendable-along-η   extendable
  where
  open Modality

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

-- The modality is empty-modal.

∥∥ᴱ-empty-modal : Empty-modal (∥∥ᴱ-modality { = })
∥∥ᴱ-empty-modal = [ ⊥-propositional ]

-- The modality is not left exact.

¬-∥∥ᴱ-left-exact : ¬ Left-exact (∥_∥ᴱ {a = a})
¬-∥∥ᴱ-left-exact {a} =
  Er.Stable-¬
    [ 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 }   Erased (Is-proposition A) ∥ᴱ)  →⟨  hyp  hyp) 
   Erased (Is-proposition (  Bool)) ∥ᴱ          →⟨ ◯-map (Er.map (⊥-elim  ¬-Bool-propositional  H-level-cong _ 1 Bijection.↑↔)) 
   Erased  ∥ᴱ                                    →⟨ ◯-map (_↔_.to Er.Erased-⊥↔⊥) 
    ∥ᴱ                                           →⟨ ⊥-elim  Modal→Stable ∥∥ᴱ-empty-modal ⟩□
                                                  
  where
  open Modality (∥∥ᴱ-modality { = })

-- The modality is W-modal.

∥∥ᴱ-W-modal : W-modal (∥∥ᴱ-modality { = })
∥∥ᴱ-W-modal [ p ] = [ W-closure ext 0 p ]

-- The modality is not accessibility-modal.

¬-∥∥ᴱ-accessibility-modal :
  ¬ Modality.Accessibility-modal (∥∥ᴱ-modality { = })
¬-∥∥ᴱ-accessibility-modal {} acc =
  Er.Very-stable→Stable 0 Er.Very-stable-⊥
    [ Is-proposition-◯→¬-Accessibility-modal
        truncation-is-proposition acc
    ]
  where
  open Modality (∥∥ᴱ-modality { = })

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

Is-proposition→∥∥ᴱ-accessibility-modal :
  {A : Type } {_<_ : A  A  Type } 
  @0 Is-proposition A 
  @0 (∀ 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 =
  Er.Very-stable→Stable₀ Er.Very-stable-⊥
    [                        $⟨ (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

-- ∥_∥ᴱ commutes with Σ.

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

------------------------------------------------------------------------
-- Conversion functions

-- ∥_∥ᴱ is pointwise equivalent to N.∥_∥ᴱ.

∥∥ᴱ≃∥∥ᴱ :  A ∥ᴱ  N.∥ A ∥ᴱ
∥∥ᴱ≃∥∥ᴱ = Eq.↔→≃
  (rec λ where
     .∣∣ʳ                         N.∣_∣
     .truncation-is-propositionʳ  N.∥∥ᴱ-proposition)
  (N.elim λ where
     .N.∣∣ʳ                ∣_∣
     .N.is-propositionʳ _  truncation-is-proposition)
  (N.elim λ where
     .N.∣∣ʳ _              refl _
     .N.is-propositionʳ _  mono₁ 1 N.∥∥ᴱ-proposition)
  (elim λ where
     .∣∣ʳ _                         refl _
     .truncation-is-propositionʳ _  mono₁ 1 truncation-is-proposition)

------------------------------------------------------------------------
-- Some preservation lemmas and related results

-- A map function.

∥∥ᴱ-map : (A  B)   A ∥ᴱ   B ∥ᴱ
∥∥ᴱ-map f = rec λ where
  .∣∣ʳ                         ∣_∣  f
  .truncation-is-propositionʳ  truncation-is-proposition

mutual

  -- If A and B are logically equivalent, then there is an equivalence
  -- with erased proofs between ∥ A ∥ᴱ and ∥ B ∥ᴱ.

  ∥∥ᴱ-cong-⇔ : A  B   A ∥ᴱ ≃ᴱ  B ∥ᴱ
  ∥∥ᴱ-cong-⇔ A⇔B = ∥∥ᴱ-cong-⇔′ (∣_∣  _⇔_.to A⇔B) (∣_∣  _⇔_.from A⇔B)

  -- A variant of the previous result.

  ∥∥ᴱ-cong-⇔′ : (A   B ∥ᴱ)  (B   A ∥ᴱ)   A ∥ᴱ ≃ᴱ  B ∥ᴱ
  ∥∥ᴱ-cong-⇔′ A→∥B∥ B→∥A∥ = EEq.⇔→≃ᴱ
    truncation-is-proposition
    truncation-is-proposition
    (rec λ where
       .∣∣ʳ                         A→∥B∥
       .truncation-is-propositionʳ  truncation-is-proposition)
    (rec λ where
       .∣∣ʳ                         B→∥A∥
       .truncation-is-propositionʳ  truncation-is-proposition)

-- If there is a split surjection from A to B, then there is a split
-- surjection from ∥ A ∥ᴱ to ∥ B ∥ᴱ.

∥∥ᴱ-cong-↠ : A  B   A ∥ᴱ   B ∥ᴱ
∥∥ᴱ-cong-↠ A↠B = record
  { logical-equivalence = record
    { to   = ∥∥ᴱ-map (_↠_.to   A↠B)
    ; from = ∥∥ᴱ-map (_↠_.from A↠B)
    }
  ; right-inverse-of = elim λ where
      .∣∣ʳ x 
         _↠_.to A↠B (_↠_.from A↠B x)   ≡⟨ cong ∣_∣ (_↠_.right-inverse-of A↠B x) ⟩∎
         x                             
      .truncation-is-propositionʳ _ 
        mono₁ 1 truncation-is-proposition
  }

private

  ∥∥ᴱ-cong-↔ : A  B   A ∥ᴱ   B ∥ᴱ
  ∥∥ᴱ-cong-↔ A↔B = record
    { surjection      = ∥∥ᴱ-cong-↠ (_↔_.surjection A↔B)
    ; left-inverse-of = elim λ where
        .∣∣ʳ x 
           _↔_.from A↔B (_↔_.to A↔B x)   ≡⟨ cong ∣_∣ (_↔_.left-inverse-of A↔B x) ⟩∎
           x                             
        .truncation-is-propositionʳ _ 
          mono₁ 1 truncation-is-proposition
    }

-- The truncation operator preserves "symmetric" functions.

∥∥ᴱ-cong : A ↝[  k ⌋-sym ] B   A ∥ᴱ ↝[  k ⌋-sym ]  B ∥ᴱ
∥∥ᴱ-cong {k = logical-equivalence} = _≃ᴱ_.logical-equivalence 
                                     ∥∥ᴱ-cong-⇔
∥∥ᴱ-cong {k = bijection}           = ∥∥ᴱ-cong-↔
∥∥ᴱ-cong {k = equivalence}         = from-isomorphism  ∥∥ᴱ-cong-↔ 
                                     from-isomorphism
∥∥ᴱ-cong {k = equivalenceᴱ}        = ∥∥ᴱ-cong-⇔ 
                                     _≃ᴱ_.logical-equivalence

------------------------------------------------------------------------
-- Some bijections/erased equivalences

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

∥∥ᴱ↔ : @0 Is-proposition A   A ∥ᴱ  A
∥∥ᴱ↔ A-prop = record
  { surjection = record
    { logical-equivalence = record
      { to   = rec λ where
          .∣∣ʳ                         id
          .truncation-is-propositionʳ  A-prop
      ; from = ∣_∣
      }
    ; right-inverse-of = λ _  refl _
    }
  ; left-inverse-of = elim λ where
      .∣∣ʳ _                         refl _
      .truncation-is-propositionʳ _  mono₁ 1 truncation-is-proposition
  }

-- If A is merely inhabited, then the truncation of A is equivalent
-- (with erased proofs) to the unit type.

inhabited⇒∥∥ᴱ≃ᴱ⊤ :  A ∥ᴱ   A ∥ᴱ ≃ᴱ 
inhabited⇒∥∥ᴱ≃ᴱ⊤ ∥a∥ =
  EEq.inhabited→Is-proposition→≃ᴱ⊤ ∥a∥ truncation-is-proposition

-- 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  rec λ where
                           .∣∣ʳ                         ¬a
                           .truncation-is-propositionʳ  ⊥-propositional) 
  ¬  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 = λ ¬A  rec λ where
                        .∣∣ʳ                         ¬A
                        .truncation-is-propositionʳ  ⊥-propositional
      }
    ; right-inverse-of = λ _  ¬-propositional ext _ _
    }
  ; left-inverse-of = λ _  ¬-propositional ext _ _
  }

-- A form of idempotence for binary sums.

idempotent :  A  A ∥ᴱ ≃ᴱ  A ∥ᴱ
idempotent = ∥∥ᴱ-cong-⇔ (record { to = P.[ id , id ]; from = inj₁ })

------------------------------------------------------------------------
-- The universal property, and some related results

mutual

  -- The propositional truncation operator's universal property.
  --
  -- See also Quotient.Erased.Σ→Erased-Constant≃∥∥ᴱ→.

  universal-property :
    @0 Is-proposition B 
    ( A ∥ᴱ  B)  (A  B)
  universal-property B-prop = universal-property-Π  _  B-prop)

  -- A generalisation of the universal property.

  universal-property-Π :
    @0 (∀ x  Is-proposition (P x)) 
    ((x :  A ∥ᴱ)  P x)  ((x : A)  P  x )
  universal-property-Π {A} {P} P-prop =
    ((x :  A ∥ᴱ)  P x)      ↝⟨ Eq.↔⇒≃ (record
                                   { surjection = record
                                     { logical-equivalence = record
                                       { to   = λ f   f  ∣_∣ 
                                       ; from = rec λ where
                                           .∣∣ʳ f  elim λ where
                                             .∣∣ʳ                         f
                                             .truncation-is-propositionʳ  P-prop
                                           .truncation-is-propositionʳ 
                                             Π-closure ext 1 λ _  P-prop _
                                       }
                                     ; right-inverse-of = elim λ where
                                         .∣∣ʳ _                         refl _
                                         .truncation-is-propositionʳ _ 
                                           mono₁ 1 truncation-is-proposition
                                     }
                                   ; left-inverse-of = λ f  ⟨ext⟩ $ elim λ where
                                       .∣∣ʳ _                         refl _
                                       .truncation-is-propositionʳ _ 
                                         mono₁ 1 (P-prop _)
                                   }) 
     ((x : A)  P  x ) ∥ᴱ  ↔⟨ ∥∥ᴱ↔ (Π-closure ext 1 λ _  P-prop _) ⟩□
    ((x : A)  P  x )       

-- The universal property computes in the "right" way.

_ :
  (@0 B-prop : Is-proposition B)
  (f :  A ∥ᴱ  B) 
  _≃_.to (universal-property B-prop) f  f  ∣_∣
_ = λ _ _  refl _

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

-- Functions from ∥ A ∥ᴱ can be expressed as functions from A along
-- with some erased data.

∥∥ᴱ→≃ :
  ( A ∥ᴱ  B)
    
  ( λ (f : A  B) 
     Erased ( λ (g :  n   A ∥¹-out-^ (suc n)  B) 
               (∀ x  g zero O.∣ x   f x) ×
               (∀ n x  g (suc n) O.∣ x   g n x)))
∥∥ᴱ→≃ {A} {B} =
  ( A ∥ᴱ  B)                                           ↝⟨ →-cong ext ∥∥ᴱ≃∥∥ᴱ F.id 

  (N.∥ A ∥ᴱ  B)                                         ↝⟨ C.universal-property ⟩□

  ( λ (f : A  B) 
     Erased ( λ (g :  n   A ∥¹-out-^ (suc n)  B) 
               (∀ x  g zero O.∣ x   f x) ×
               (∀ n x  g (suc n) O.∣ x   g n x)))     

-- A function of type (x : ∥ A ∥ᴱ) → P x, along with an erased proof
-- showing that the function is equal to some erased function, is
-- equivalent to a function of type (x : A) → P ∣ x ∣, along with an
-- erased equality proof.

Σ-Π-∥∥ᴱ-Erased-≡-≃ :
  {@0 g : (x :  A ∥ᴱ)  P x} 
  ( λ (f : (x :  A ∥ᴱ)  P x)  Erased (f  g)) 
  ( λ (f : (x : A)  P  x )  Erased (f  g  ∣_∣))
Σ-Π-∥∥ᴱ-Erased-≡-≃ {A} {P} {g} =
  ( λ (f : (x :  A ∥ᴱ)  P x)  Erased (f  g))       ↝⟨ (Σ-cong lemma λ _  Er.Erased-cong (inverse $ Eq.≃-≡ lemma)) 

  ( λ (f : (x : N.∥ A ∥ᴱ)  P (_≃_.from ∥∥ᴱ≃∥∥ᴱ x)) 
     Erased (f  g  _≃_.from ∥∥ᴱ≃∥∥ᴱ))                 ↝⟨ N.Σ-Π-∥∥ᴱ-Erased-≡-≃ ⟩□

  ( λ (f : (x : A)  P  x )  Erased (f  g  ∣_∣))  
  where
  lemma = Π-cong-contra ext (inverse ∥∥ᴱ≃∥∥ᴱ) λ _  Eq.id

------------------------------------------------------------------------
-- Some results based on "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}  @0 Constant f   A ∥ᴱ  A
constant-endofunction⇒h-stable {A} {f} c =
   A ∥ᴱ                            ↝⟨ (rec λ where
                                          .∣∣ʳ x  f x , [ c (f x) x ]
                                          .truncation-is-propositionʳ  prop) 
  ( λ (x : A)  Erased (f x  x))  ↝⟨ proj₁ ⟩□
  A                                 
  where
  @0 prop : _
  prop =                                       $⟨ fixpoint-lemma f c 
    Is-proposition ( λ x  f x  x)           ↝⟨ H-level-cong _ 1 (∃-cong λ _  inverse $ Er.erased Er.Erased↔)  (_  _) ⟩□
    Is-proposition ( λ x  Erased (f x  x))  

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

constant-endofunction⇔h-stable :
  ( λ (f : A  A)  Erased (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   )
           ]
  }

------------------------------------------------------------------------
-- Some results related to _×_

-- The cartesian product of the truncation of A and A is equivalent
-- (with erased "proofs") to A.

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

-- The application _≃ᴱ_.right-inverse-of ∥∥ᴱ×≃ᴱ x computes in a
-- certain way.

_ : _≃ᴱ_.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   = uncurry $ rec λ where
                 .∣∣ʳ x  rec λ where
                   .∣∣ʳ y                        x , y 
                   .truncation-is-propositionʳ 
                     truncation-is-proposition
                 .truncation-is-propositionʳ 
                   Π-closure ext 1 λ _ 
                   truncation-is-proposition
      }
    ; right-inverse-of = elim λ where
        .∣∣ʳ _                         refl _
        .truncation-is-propositionʳ _ 
          mono₁ 1 truncation-is-proposition
    }
  ; left-inverse-of = uncurry $ elim λ where
      .∣∣ʳ _  elim λ where
        .∣∣ʳ _  refl _
        .truncation-is-propositionʳ _ 
          mono₁ 1 $
          ×-closure 1 truncation-is-proposition
                      truncation-is-proposition
      .truncation-is-propositionʳ _ 
        Π-closure ext 1 λ _ 
        mono₁ 1 $
        ×-closure 1 truncation-is-proposition
                    truncation-is-proposition
  }

------------------------------------------------------------------------
-- Some results related to h-levels

-- 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 
    flip rec (inhabited a) λ where
      .∣∣ʳ b 
        proj₁-closure  _  b) (suc n) h
      .truncation-is-propositionʳ 
        H-level-propositional ext (suc n)

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        

------------------------------------------------------------------------
-- Flattening

-- A generalised flattening lemma.

flatten′ :
  (F : (Type   Type )  Type f)
  (map :  {G H}  (∀ {A}  G A  H A)  F G  F H)
  (f : F ∥_∥ᴱ   F id ∥ᴱ) 
  (∀ x  f (map ∣_∣ x)   x ) 
  (∀ x  ∥∥ᴱ-map (map ∣_∣) (f x)   x ) 
   F ∥_∥ᴱ ∥ᴱ   F id ∥ᴱ
flatten′ _ map f f-map map-f = record
  { surjection = record
    { logical-equivalence = record
      { to   = rec λ where
                 .∣∣ʳ                         f
                 .truncation-is-propositionʳ  truncation-is-proposition
      ; from = ∥∥ᴱ-map (map ∣_∣)
      }
    ; right-inverse-of = elim λ where
        .∣∣ʳ                           f-map
        .truncation-is-propositionʳ _ 
          mono₁ 1 truncation-is-proposition
    }
  ; left-inverse-of = elim λ where
      .∣∣ʳ                           map-f
      .truncation-is-propositionʳ _ 
        mono₁ 1 truncation-is-proposition
  }

-- Nested truncations can be flattened.

flatten :   A ∥ᴱ ∥ᴱ   A ∥ᴱ
flatten {A} = flatten′
   F  F A)
   f  f)
  id
   _  refl _)
  (elim λ where
     .∣∣ʳ _                         refl _
     .truncation-is-propositionʳ _  mono₁ 1 truncation-is-proposition)

private

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

  ∥∃∥∥ᴱ∥ᴱ↔∥∃∥ᴱ :   (∥_∥ᴱ  P) ∥ᴱ    P ∥ᴱ
  ∥∃∥∥ᴱ∥ᴱ↔∥∃∥ᴱ {P} = flatten′
     F   (F  P))
     f  Σ-map id f)
    (uncurry λ x  ∥∥ᴱ-map (x ,_))
     _  refl _)
    (uncurry λ _  elim λ where
       .∣∣ʳ _  refl _
       .truncation-is-propositionʳ _ 
         mono₁ 1 truncation-is-proposition)

-- A variant of flatten′ with _≃ᴱ_ instead of _↔_.

flatten-≃ᴱ :
  (F : (Type   Type )  Type f)
  (map :  {G H}  (∀ {A}  G A  H A)  F G  F H)
  (f : F ∥_∥ᴱ   F id ∥ᴱ) 
  @0 (∀ x  f (map ∣_∣ x)   x ) 
  @0 (∀ x  ∥∥ᴱ-map (map ∣_∣) (f x)   x ) 
   F ∥_∥ᴱ ∥ᴱ ≃ᴱ  F id ∥ᴱ
flatten-≃ᴱ _ map f f-map map-f = EEq.↔→≃ᴱ
  (rec λ where
     .∣∣ʳ                         f
     .truncation-is-propositionʳ  truncation-is-proposition)
  (∥∥ᴱ-map (map ∣_∣))
  (elim λ @0 where
     .∣∣ʳ                           f-map
     .truncation-is-propositionʳ _ 
       mono₁ 1 truncation-is-proposition)
  (elim λ @0 where
     .∣∣ʳ                           map-f
     .truncation-is-propositionʳ _ 
       mono₁ 1 truncation-is-proposition)

------------------------------------------------------------------------
-- The propositional truncation operator is a monad

-- 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 ∥ᴱ) 
  x >>=′  x  f x >>=′ g)  x >>=′ f >>=′ g
>>=′-associative = elim λ where
  .∣∣ʳ _                         refl _
  .truncation-is-propositionʳ _  ⇒≡ 1 truncation-is-proposition

instance

  -- The propositional truncation operator is a monad.

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

  monad : Monad (∥_∥ᴱ {a = a})
  Monad.raw-monad monad           = raw-monad
  Monad.left-identity monad _ _   = refl _
  Monad.associativity monad x _ _ = >>=′-associative x
  Monad.right-identity monad      = elim λ where
    .∣∣ʳ                        _  refl _
    .truncation-is-propositionʳ _  ⇒≡ 1 truncation-is-proposition

------------------------------------------------------------------------
-- Surjectivity

-- A variant of surjectivity with "erased proofs".

Surjectiveᴱ :
  {A : Type a} {B : Type b} 
  (A  B)  Type (a  b)
Surjectiveᴱ f =  y   f ⁻¹ᴱ y ∥ᴱ

-- The property Surjectiveᴱ f is a proposition (in erased contexts).

@0 Surjectiveᴱ-propositional : Is-proposition (Surjectiveᴱ f)
Surjectiveᴱ-propositional =
  Π-closure ext 1 λ _ 
  truncation-is-proposition

-- The function ∣_∣ is surjective (with erased proofs).

∣∣-surjective : Surjectiveᴱ (∣_∣ {A = A})
∣∣-surjective = elim λ where
  .∣∣ʳ x                          x , [ refl _ ] 
  .truncation-is-propositionʳ _  truncation-is-proposition

-- Split surjective functions are surjective (with erased proofs).

Split-surjective→Surjectiveᴱ :
  Split-surjective f  Surjectiveᴱ f
Split-surjective→Surjectiveᴱ s = λ y   ECP.⁻¹→⁻¹ᴱ (s y) 

-- Being both surjective (with erased proofs) and an embedding
-- (completely erased) is equivalent to being an equivalence (with
-- erased proofs).
--
-- This result, without erasure, is Corollary 4.6.4 from the first
-- edition of the HoTT book.

Surjectiveᴱ×Erased-Is-embedding≃ᴱIs-equivalenceᴱ :
  (Surjectiveᴱ f × Erased (Is-embedding f)) ≃ᴱ Is-equivalenceᴱ f
Surjectiveᴱ×Erased-Is-embedding≃ᴱIs-equivalenceᴱ {f} = EEq.⇔→≃ᴱ
  (×-closure 1
     Surjectiveᴱ-propositional
     (Er.H-level-Erased 1
        (Emb.Is-embedding-propositional ext)))
  (EEq.Is-equivalenceᴱ-propositional ext f)
   (is-surj , is-emb) 
     _⇔_.from EEq.Is-equivalenceᴱ⇔Is-equivalenceᴱ-CP $ λ y 
                              $⟨ is-surj y 
      f ⁻¹ᴱ y ∥ᴱ             ↝⟨ (rec λ where
                                    .∣∣ʳ p  ECP.inhabited→Is-proposition→Contractibleᴱ p
                                               (H-level-cong _ 1
                                                  ECP.⁻¹≃⁻¹ᴱ
                                                  (Emb.embedding→⁻¹-propositional (Er.erased is-emb) _))
                                    .truncation-is-propositionʳ 
                                      ECP.Contractibleᴱ-propositional ext) ⟩□
     Contractibleᴱ (f ⁻¹ᴱ y)  )
   is-eq@(inv , [ r-inv , _ ]) 
        y            $⟨ inv y , [ r-inv y ] 
          f ⁻¹ᴱ y       ↝⟨ ∣_∣ 
           f ⁻¹ᴱ y ∥ᴱ  )

     ,                            ($⟨ is-eq 
       Is-equivalenceᴱ f           ↝⟨ Er.[_]→ 
       Erased (Is-equivalenceᴱ f)  ↝⟨ Er.map EEq.Is-equivalenceᴱ→Is-equivalence 
       Erased (Is-equivalence f)   ↝⟨ Er.map Emb.Is-equivalence→Is-embedding ⟩□
       Erased (Is-embedding f)     ))

------------------------------------------------------------------------
-- Another lemma

-- 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

------------------------------------------------------------------------
-- 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₂

-- In erased contexts _∥⊎∥ᴱ_ is pointwise propositional.

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

-- The _∥⊎∥ᴱ_ operator preserves functions.

infixr 1 _∥⊎∥ᴱ-map_

_∥⊎∥ᴱ-map_ : (A₁  A₂)  (B₁  B₂)  A₁ ∥⊎∥ᴱ B₁  A₂ ∥⊎∥ᴱ B₂
f ∥⊎∥ᴱ-map g = ∥∥ᴱ-map (f ⊎-cong g)

-- The _∥⊎∥ᴱ_ operator preserves "symmetric" functions.

infixr 1 _∥⊎∥ᴱ-cong_

_∥⊎∥ᴱ-cong_ :
  A₁ ↝[  k ⌋-sym ] A₂  B₁ ↝[  k ⌋-sym ] B₂ 
  (A₁ ∥⊎∥ᴱ B₁) ↝[  k ⌋-sym ] (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)
    P.[ ∥∥ᴱ-map inj₁ , ∣inj₂∣ ]
    P.[  _  refl _) ,  _  refl _) ]
    P.[ (elim λ where
           .∣∣ʳ _  refl _
           .truncation-is-propositionʳ _ 
             mono₁ 1 ∥⊎∥ᴱ-propositional)
      ,  _  refl _)
      ]

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 : @0 Is-proposition A   { = } ∥⊎∥ᴱ A  A
∥⊎∥ᴱ-left-identity {A} A-prop =
     A ∥ᴱ  ↝⟨ ∥∥ᴱ-cong ⊎-left-identity 
   A ∥ᴱ      ↝⟨ ∥∥ᴱ↔ A-prop ⟩□
  A          

∥⊎∥ᴱ-right-identity : @0 Is-proposition A  A ∥⊎∥ᴱ  { = }  A
∥⊎∥ᴱ-right-identity {A} A-prop =
  A ∥⊎∥ᴱ   ↔⟨ ∥⊎∥ᴱ-comm 
   ∥⊎∥ᴱ A  ↔⟨ ∥⊎∥ᴱ-left-identity A-prop ⟩□
  A         

-- _∥⊎∥ᴱ_ is idempotent for propositions (up to equivalences with
-- erased proofs).

∥⊎∥ᴱ-idempotent : @0 Is-proposition A  (A ∥⊎∥ᴱ A) ≃ᴱ A
∥⊎∥ᴱ-idempotent {A} A-prop =
   A  A ∥ᴱ  ↝⟨ idempotent 
   A ∥ᴱ      ↔⟨ ∥∥ᴱ↔ A-prop ⟩□
  A           

-- Sometimes a truncated binary sum is equivalent (with erased proofs)
-- to one of its summands.

drop-left-∥⊎∥ᴱ :
  @0 Is-proposition B  (A  B)  (A ∥⊎∥ᴱ B) ≃ᴱ B
drop-left-∥⊎∥ᴱ B-prop A→B = EEq.⇔→≃ᴱ
  ∥⊎∥ᴱ-propositional
  B-prop
  (rec λ where
     .∣∣ʳ  P.[ A→B , id ]
     .truncation-is-propositionʳ  B-prop)
  ∣inj₂∣

drop-right-∥⊎∥ᴱ :
  @0 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        

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

drop-⊥-right-∥⊎∥ᴱ :
  @0 Is-proposition A  ¬ B  A ∥⊎∥ᴱ B  A
drop-⊥-right-∥⊎∥ᴱ A-prop ¬B = record
  { surjection = record
    { logical-equivalence = record
      { to = rec λ where
          .∣∣ʳ  P.[ id , ⊥-elim  ¬B ]
          .truncation-is-propositionʳ  A-prop
      ; from = ∣inj₁∣
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = elim λ where
      .∣∣ʳ  P.[  _  refl _) , ⊥-elim  ¬B ]
      .truncation-is-propositionʳ _ 
        mono₁ 1 ∥⊎∥ᴱ-propositional
  }

drop-⊥-left-∥⊎∥ᴱ :
  @0 Is-proposition B  ¬ A  A ∥⊎∥ᴱ B  B
drop-⊥-left-∥⊎∥ᴱ B-prop ¬A = record
  { surjection = record
    { logical-equivalence = record
      { to = rec λ where
          .∣∣ʳ  P.[ ⊥-elim  ¬A , id ]
          .truncation-is-propositionʳ  B-prop
      ; from = ∣inj₂∣
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = elim λ where
      .∣∣ʳ  P.[ ⊥-elim  ¬A ,  _  refl _) ]
      .truncation-is-propositionʳ _ 
        mono₁ 1 ∥⊎∥ᴱ-propositional
  }

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

Π∥⊎∥ᴱ↔Π×Π :
  @0 (∀ 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 :
  @0 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 ,_))
                                       _  refl _)
                                      (uncurry λ _  elim λ where
                                         .∣∣ʳ _  refl _
                                         .truncation-is-propositionʳ _ 
                                           mono₁ 1 truncation-is-proposition) 
   ( λ x  P x  Q x) ∥ᴱ       ↝⟨ ∥∥ᴱ-cong ∃-⊎-distrib-left ⟩□
    P   Q ∥ᴱ                 

Σ-∥⊎∥ᴱ-distrib-right :
  @0 (∀ x  Is-proposition (P x)) 
  Σ (A ∥⊎∥ᴱ B) P  Σ A (P  ∣inj₁∣) ∥⊎∥ᴱ Σ B (P  ∣inj₂∣)
Σ-∥⊎∥ᴱ-distrib-right {A} {B} {P} P-prop = record
  { surjection = record
    { logical-equivalence = record
      { to = uncurry $ elim λ where
          .∣∣ʳ  curry (∣_∣  _↔_.to ∃-⊎-distrib-right)
          .truncation-is-propositionʳ _ 
            Π-closure ext 1 λ _ 
            ∥⊎∥ᴱ-propositional
      ; from = rec λ where
          .∣∣ʳ  Σ-map ∣_∣ id  _↔_.from ∃-⊎-distrib-right
          .truncation-is-propositionʳ  prop
      }
    ; right-inverse-of = elim λ where
      .∣∣ʳ  P.[  _  refl _) ,  _  refl _) ]
      .truncation-is-propositionʳ _ 
        mono₁ 1 ∥⊎∥ᴱ-propositional
    }
  ; left-inverse-of = uncurry $ elim λ where
      .∣∣ʳ  P.[  _ _  refl _) ,  _ _  refl _) ]
      .truncation-is-propositionʳ _ 
        Π-closure ext 1 λ _ 
        mono₁ 1 prop
  }
  where
  @0 prop : _
  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 = EEq.⇔→≃ᴱ
  ∥⊎∥ᴱ-propositional
  (¬-propositional ext)
  (rec λ where
     .∣∣ʳ  ¬⊎¬→׬
     .truncation-is-propositionʳ  ¬-propositional ext)
  (∣_∣  _↠_.from (¬⊎¬↠¬× ext dec-¬A dec-¬B))

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

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

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

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

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

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

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

  ( λ (x : Erased B)  Erased-singleton (erased x))         ↔⟨ Er.Σ-Erased-Erased-singleton↔ ⟩□

  B                                                          

-- 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) x 
  _≃ᴱ_.to (Σ-Erased-∥-Σ-Erased-≡-∥≃ᴱ A↠B) x  erased (proj₁ x)
to-Σ-Erased-∥-Σ-Erased-≡-∥≃ᴱ≡ A↠B ([ x ] , y) =
  _≃ᴱ_.to (Σ-Erased-∥-Σ-Erased-≡-∥≃ᴱ A↠B) ([ x ] , y)  ≡⟨⟩
  proj₁ (_≃ᴱ_.to (↠→≃ᴱErased-singleton A↠B) y)         ≡⟨ erased (proj₂ (_≃ᴱ_.to (↠→≃ᴱErased-singleton A↠B) y)) ⟩∎
  x