H-level.Truncation

------------------------------------------------------------------------
-- Truncation, defined as a HIT
------------------------------------------------------------------------

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

-- The beginning of this module follows the HoTT book rather closely.

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

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

import Erased.Basics as Er
open import Logical-equivalence using (_⇔_)
open import Prelude

import Accessibility equality-with-J as A
open import Bijection equality-with-J as B using (_↔_)
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 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
open import H-level.Truncation.Propositional eq as TP using (∥_∥)
open import Modality.Basics equality-with-J
open import Monad equality-with-J
open import Nat equality-with-J as Nat using (_≤_; min)
import Pointed-type equality-with-J as PT
open import Sphere eq
open import Suspension eq as Susp using (north)
open import Univalence-axiom equality-with-J

private
  variable
    a b ℓ p : Level
    A B C   : Type a
    P       : A → Type p
    e x y   : A
    f g r   : A → B
    m n     : ℕ
    k       : Isomorphism-kind

------------------------------------------------------------------------
-- The truncation operator

-- A truncation operator for positive h-levels.

data ∥_∥[1+_] (A : Type a) (n : ℕ) : Type a where
  ∣_∣    : A → ∥ A ∥[1+ n ]
  hub    : (r : 𝕊 n → ∥ A ∥[1+ n ]) → ∥ A ∥[1+ n ]
  spokeᴾ : (r : 𝕊 n → ∥ A ∥[1+ n ]) (x : 𝕊 n) → r x P.≡ hub r

-- Spoke equalities.

spoke : (r : 𝕊 n → ∥ A ∥[1+ n ]) (x : 𝕊 n) → r x ≡ hub r
spoke r x = _↔_.from ≡↔≡ (spokeᴾ r x)

-- The truncation operator produces types of the right h-level.

truncation-has-correct-h-level : ∀ n → H-level (1 + n) ∥ A ∥[1+ n ]
truncation-has-correct-h-level {A} n =
  _↔_.from +↔∀contractible𝕊→ᴮ c
  where
  c : ∀ x → Contractible ((𝕊 n , north) PT.→ᴮ (∥ A ∥[1+ n ] , x))
  c x =
      (const x , (const x (north {A = 𝕊 n})  ≡⟨⟩
                  x                          ∎))
    , λ { (f , fn≡x) → Σ-≡,≡→≡
            (⟨ext⟩ λ y →
               const x y  ≡⟨⟩
               x          ≡⟨ sym fn≡x ⟩
               f north    ≡⟨ spoke f north ⟩
               hub f      ≡⟨ sym $ spoke f y ⟩∎
               f y        ∎)
            (subst (λ f → f north ≡ x)
                   (⟨ext⟩ (λ y → trans (sym fn≡x)
                                   (trans (spoke f north)
                                      (sym (spoke f y)))))
                   (refl x)                                             ≡⟨ subst-ext ext ⟩

             subst (_≡ x)
                   (trans (sym fn≡x)
                      (trans (spoke f north) (sym (spoke f north))))
                   (refl x)                                             ≡⟨ cong (λ p → subst (_≡ x) (trans (sym fn≡x) p) (refl x)) $ trans-symʳ _ ⟩

             subst (_≡ x) (trans (sym fn≡x) (refl (f north))) (refl x)  ≡⟨ cong (λ p → subst (_≡ x) p (refl x)) $ trans-reflʳ _ ⟩

             subst (_≡ x) (sym fn≡x) (refl x)                           ≡⟨ subst-trans _ ⟩

             trans fn≡x (refl x)                                        ≡⟨ trans-reflʳ _ ⟩∎

             fn≡x                                                       ∎)
        }

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

-- A dependent eliminator, expressed using paths.

record Elimᴾ {A : Type a} (P : ∥ A ∥[1+ n ] → Type p) :
             Type (a ⊔ p) where
  no-eta-equality
  field
    ∣∣ʳ    : ∀ x → P ∣ x ∣
    hubʳ   : (r : 𝕊 n → ∥ A ∥[1+ n ]) →
             (∀ x → P (r x)) →
             P (hub r)
    spokeʳ : (r : 𝕊 n → ∥ A ∥[1+ n ])
             (p : ∀ x → P (r x))
             (x : 𝕊 n) →
             P.[ (λ i → P (spokeᴾ r x i)) ] p x ≡ hubʳ r p

open Elimᴾ public

elimᴾ : Elimᴾ P → ∀ x → P x
elimᴾ {P} e = helper
  where
  module E = Elimᴾ e

  helper : ∀ x → P x
  helper ∣ x ∣          = E.∣∣ʳ x
  helper (hub r)        = E.hubʳ r (λ x → helper (r x))
  helper (spokeᴾ r x i) = E.spokeʳ r (λ x → helper (r x)) x i

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

record Recᴾ (n : ℕ) (A : Type a) (B : Type b) : Type (a ⊔ b) where
  no-eta-equality
  field
    ∣∣ʳ    : A → B
    hubʳ   : (𝕊 n → ∥ A ∥[1+ n ]) → (𝕊 n → B) → B
    spokeʳ : (r : 𝕊 n → ∥ A ∥[1+ n ]) (p : 𝕊 n → B) (x : 𝕊 n) →
             p x P.≡ hubʳ r p

open Recᴾ public

recᴾ : Recᴾ n A B → ∥ A ∥[1+ n ] → B
recᴾ r = elimᴾ eᴾ
  where
  module R = Recᴾ r

  eᴾ : Elimᴾ _
  eᴾ .∣∣ʳ    = r .∣∣ʳ
  eᴾ .hubʳ   = r .hubʳ
  eᴾ .spokeʳ = r .spokeʳ

-- A dependent eliminator.

record Elim′ {A : Type a} (P : ∥ A ∥[1+ n ] → Type p) :
             Type (a ⊔ p) where
  no-eta-equality
  field
    ∣∣ʳ    : ∀ x → P ∣ x ∣
    hubʳ   : (r : 𝕊 n → ∥ A ∥[1+ n ]) →
             (∀ x → P (r x)) →
             P (hub r)
    spokeʳ : (r : 𝕊 n → ∥ A ∥[1+ n ])
             (p : ∀ x → P (r x))
             (x : 𝕊 n) →
             subst P (spoke r x) (p x) ≡ hubʳ r p

open Elim′ public

elim′ : Elim′ P → ∀ x → P x
elim′ e′ = elimᴾ eᴾ
  where
  module E′ = Elim′ e′

  eᴾ : Elimᴾ _
  eᴾ .∣∣ʳ          = E′.∣∣ʳ
  eᴾ .hubʳ         = E′.hubʳ
  eᴾ .spokeʳ r p x = subst≡→[]≡ (E′.spokeʳ r p x)

elim′-spoke :
  dcong (elim′ e) (spoke r x) ≡
  Elim′.spokeʳ e r (λ x → elim′ e (r x)) x
elim′-spoke = dcong-subst≡→[]≡ (refl _)

-- A non-dependent eliminator.

record Rec′ (n : ℕ) (A : Type a) (B : Type b) : Type (a ⊔ b) where
  no-eta-equality
  field
    ∣∣ʳ    : A → B
    hubʳ   : (𝕊 n → ∥ A ∥[1+ n ]) → (𝕊 n → B) → B
    spokeʳ : (r : 𝕊 n → ∥ A ∥[1+ n ]) (p : 𝕊 n → B) (x : 𝕊 n) →
             p x ≡ hubʳ r p

open Rec′ public

rec′ : Rec′ n A B → ∥ A ∥[1+ n ] → B
rec′ r′ = recᴾ rᴾ
  where
  module R′ = Rec′ r′

  rᴾ : Recᴾ _ _ _
  rᴾ .∣∣ʳ          = R′.∣∣ʳ
  rᴾ .hubʳ         = R′.hubʳ
  rᴾ .spokeʳ r p x = _↔_.to ≡↔≡ (R′.spokeʳ r p x)

rec′-spoke :
  cong (rec′ e) (spoke r x) ≡ Rec′.spokeʳ e r (λ x → rec′ e (r x)) x
rec′-spoke = cong-≡↔≡ (refl _)

-- A dependent eliminator that can be used when the motive is a family
-- of types, all of a certain h-level.

record Elim {A : Type a} (P : ∥ A ∥[1+ n ] → Type p) :
            Type (a ⊔ p) where
  no-eta-equality
  field
    ∣∣ʳ      : ∀ x → P ∣ x ∣
    h-levelʳ : ∀ x → H-level (1 + n) (P x)

open Elim public

elim : Elim {n = n} {A = A} P → ∀ x → P x
elim {n} {A} {P} e = elim′ e′
  where
  module _ (r : 𝕊 n → ∥ A ∥[1+ n ]) (p : ∀ x → P (r x)) where

    h′ : 𝕊 n → P (hub r)
    h′ x = subst P (spoke r x) (p x)

    h = h′ north

    lemma =                                                       $⟨ e .h-levelʳ ⟩
      (∀ x → H-level (1 + n) (P x))                               ↝⟨ _$ _ ⟩
      H-level (1 + n) (P (hub r))                                 ↔⟨ +↔∀contractible𝕊→ᴮ ⟩
      (∀ h → Contractible ((𝕊 n , north) PT.→ᴮ (P (hub r) , h)))  ↝⟨ _$ _ ⟩
      Contractible ((𝕊 n , north) PT.→ᴮ (P (hub r) , h))          ↝⟨ mono₁ _ ⟩□
      Is-proposition ((𝕊 n , north) PT.→ᴮ (P (hub r) , h))        □

    s = λ x →
      subst P (spoke r x) (p x)  ≡⟨⟩
      h′ x                       ≡⟨ cong (λ f → proj₁ f x) $ lemma (h′ , refl _) (const h , refl _) ⟩
      const h x                  ≡⟨⟩
      h                          ∎

  e′ : Elim′ _
  e′ .∣∣ʳ    = e .∣∣ʳ
  e′ .hubʳ   = h
  e′ .spokeʳ = s

-- A non-dependent eliminator that can be used when the motive is a
-- type of a certain h-level.

record Rec (n : ℕ) (A : Type a) (B : Type b) : Type (a ⊔ b) where
  no-eta-equality
  field
    ∣∣ʳ      : A → B
    h-levelʳ : H-level (1 + n) B

open Rec public

rec : Rec n A B → ∥ A ∥[1+ n ] → B
rec r = elim λ where
  .∣∣ʳ        → r .∣∣ʳ
  .h-levelʳ _ → r .h-levelʳ

------------------------------------------------------------------------
-- A universal property

-- Dependent functions into P that agree on the image of ∣_∣ agree
-- everywhere, if P is a family of types that all have a certain
-- h-level.

uniqueness′ :
  {f g : (x : ∥ A ∥[1+ n ]) → P x} →
  (∀ x → H-level (2 + n) (P x)) →
  ((x : A) → f ∣ x ∣ ≡ g ∣ x ∣) →
  ((x : ∥ A ∥[1+ n ]) → f x ≡ g x)
uniqueness′ {n} P-h f≡g = elim λ where
  .∣∣ʳ        → f≡g
  .h-levelʳ _ → +⇒≡ {n = suc n} (P-h _)

-- A special case of the previous property.

uniqueness :
  {f g : ∥ A ∥[1+ n ] → B} →
  H-level (1 + n) B →
  ((x : A) → f ∣ x ∣ ≡ g ∣ x ∣) →
  ((x : ∥ A ∥[1+ n ]) → f x ≡ g x)
uniqueness h = uniqueness′ (λ _ → mono₁ _ h)

-- The truncation operator's universal property.

universal-property :
  H-level (1 + n) B →
  (∥ A ∥[1+ n ] → B) ↔ (A → B)
universal-property h = record
  { surjection = record
    { logical-equivalence = record
      { to   = _∘ ∣_∣
      ; from = λ f → rec λ where
          .∣∣ʳ      → f
          .h-levelʳ → h
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = λ f → ⟨ext⟩ $ uniqueness h (λ x → f ∣ x ∣  ∎)
  }

------------------------------------------------------------------------
-- A map function and a zip function

-- The truncation operator ∥_∥[1+ n ] is a functor.

∥∥-map : (A → B) → ∥ A ∥[1+ n ] → ∥ B ∥[1+ n ]
∥∥-map f = rec λ where
  .∣∣ʳ x    → ∣ f x ∣
  .h-levelʳ → truncation-has-correct-h-level _

∥∥-map-id :
  (x : ∥ A ∥[1+ n ]) →
  ∥∥-map id x ≡ x
∥∥-map-id = uniqueness
  (truncation-has-correct-h-level _)
  (λ x → ∣ x ∣  ∎)

∥∥-map-∘ :
  (x : ∥ A ∥[1+ n ]) →
  ∥∥-map (f ∘ g) x ≡ ∥∥-map f (∥∥-map g x)
∥∥-map-∘ {f} {g} = uniqueness
  (truncation-has-correct-h-level _)
  (λ x → ∣ f (g x) ∣  ∎)

-- A zip function.

∥∥-zip : (A → B → C) → ∥ A ∥[1+ n ] → ∥ B ∥[1+ n ] → ∥ C ∥[1+ n ]
∥∥-zip f = rec λ where
  .∣∣ʳ x    → ∥∥-map (f x)
  .h-levelʳ → Π-closure ext _ λ _ →
              truncation-has-correct-h-level _

------------------------------------------------------------------------
-- Some equivalences/logical equivalences/bijections

-- A has h-level 1 + n if and only if it is isomorphic to
-- ∥ A ∥[1+ n ].

+⇔∥∥↔ : H-level (1 + n) A ⇔ (∥ A ∥[1+ n ] ↔ A)
+⇔∥∥↔ {n} {A} = record
  { to = λ h → record
    { surjection = record
      { logical-equivalence = record
        { from = ∣_∣
        ; to   = rec λ where
            .∣∣ʳ      → id
            .h-levelʳ → h
        }
      ; right-inverse-of = refl
      }
    ; left-inverse-of = elim λ where
        .∣∣ʳ x      → ∣ x ∣  ∎
        .h-levelʳ _ → ⇒≡ _ $ truncation-has-correct-h-level _
    }
  ; from =
      ∥ A ∥[1+ n ] ↔ A                                    ↝⟨ H-level-cong ext _ ⟩
      (H-level (1 + n) ∥ A ∥[1+ n ] ↔ H-level (1 + n) A)  ↝⟨ (λ hyp → _↔_.to hyp (truncation-has-correct-h-level _)) ⟩□
      H-level (1 + n) A                                   □
  }

-- The (1 + n)-truncation of x ≡ y, where x and y have type A, is
-- equivalent to the equality of ∣ x ∣ and ∣ y ∣ (as elements of the
-- (2 + n)-truncation of A), assuming univalence.
--
-- Along with the fact that this lemma computes in a certain way (see
-- below) this is more or less Theorem 7.3.12 from the HoTT book.

∥≡∥≃∣∣≡∣∣ :
  {A : Type a} {x y : A} →
  Univalence a →
  ∥ x ≡ y ∥[1+ n ] ≃ _≡_ {A = ∥ A ∥[1+ suc n ]} ∣ x ∣ ∣ y ∣
∥≡∥≃∣∣≡∣∣ {n} {A} univ = Eq.↔→≃
  (decode ∣ _ ∣ ∣ _ ∣)
  (encode ∣ _ ∣ ∣ _ ∣)
  (decode-encode _)
  (encode-decode _ _)
  where
  Eq : (_ _ : ∥ A ∥[1+ suc n ]) → ∃ λ (B : Type _) → H-level (suc n) B
  Eq = rec λ where
    .h-levelʳ →
      Π-closure ext (2 + n) λ _ →
      ∃-H-level-H-level-1+ ext univ (1 + n)
    .∣∣ʳ x → rec λ where
      .h-levelʳ → ∃-H-level-H-level-1+ ext univ (1 + n)
      .∣∣ʳ y →
        ∥ x ≡ y ∥[1+ n ] , truncation-has-correct-h-level n

  Eq-refl : (x : ∥ A ∥[1+ suc n ]) → proj₁ (Eq x x)
  Eq-refl = elim λ where
    .∣∣ʳ x      → ∣ refl x ∣
    .h-levelʳ x → mono₁ (1 + n) $ proj₂ (Eq x x)

  decode : ∀ x y → proj₁ (Eq x y) → x ≡ y
  decode = elim λ where
    .h-levelʳ _ →
      Π-closure ext (2 + n) λ _ →
      Π-closure ext (2 + n) λ _ →
      mono₁ (2 + n) $ truncation-has-correct-h-level (1 + n)
    .∣∣ʳ x → elim λ where
      .h-levelʳ _ →
        Π-closure ext (2 + n) λ _ →
        mono₁ (2 + n) $ truncation-has-correct-h-level (1 + n)
      .∣∣ʳ y → rec λ where
        .h-levelʳ → truncation-has-correct-h-level (1 + n)
        .∣∣ʳ      → cong ∣_∣

  encode : ∀ x y → x ≡ y → proj₁ (Eq x y)
  encode x y x≡y = subst (λ y → proj₁ (Eq x y)) x≡y (Eq-refl x)

  decode-encode : ∀ x (x≡y : x ≡ y) → decode x y (encode x y x≡y) ≡ x≡y
  decode-encode = elim λ where
    .h-levelʳ _ →
      Π-closure ext (2 + n) λ _ →
      mono₁ (3 + n) $ mono₁ (2 + n) $
      truncation-has-correct-h-level (1 + n)
    .∣∣ʳ x → elim¹
      (λ x≡y → decode _ _ (encode _ _ x≡y) ≡ x≡y)
      (decode (∣ x ∣) (∣ x ∣) (encode ∣ x ∣ ∣ x ∣ (refl ∣ x ∣))      ≡⟨⟩

       decode (∣ x ∣) (∣ x ∣)
         (subst (λ y → proj₁ (Eq ∣ x ∣ y)) (refl ∣ x ∣) ∣ refl x ∣)  ≡⟨ cong (decode _ _) $ subst-refl _ _ ⟩

       decode (∣ x ∣) (∣ x ∣) (∣ refl x ∣)                           ≡⟨⟩

       cong ∣_∣ (refl x)                                             ≡⟨ cong-refl _ ⟩∎

       refl ∣ x ∣                                                    ∎)

  encode-decode :
    ∀ x y (eq : proj₁ (Eq x y)) → encode x y (decode x y eq) ≡ eq
  encode-decode = elim λ where
    .h-levelʳ x →
       Π-closure ext (2 + n) λ y →
       Π-closure ext (2 + n) λ _ →
       mono₁ (2 + n) $ mono₁ (1 + n) $
       proj₂ (Eq x y)
    .∣∣ʳ x → elim λ where
      .h-levelʳ y →
        Π-closure ext (2 + n) λ _ →
        mono₁ (2 + n) $ mono₁ (1 + n) $
        proj₂ (Eq ∣ x ∣ y)
      .∣∣ʳ y → elim λ where
        .h-levelʳ _ →
          mono₁ (1 + n) $ truncation-has-correct-h-level n
        .∣∣ʳ eq →
          encode ∣ x ∣ ∣ y ∣ (decode (∣ x ∣) (∣ y ∣) (∣ eq ∣))         ≡⟨⟩
          subst (λ y → proj₁ (Eq ∣ x ∣ y)) (cong ∣_∣ eq) (∣ refl x ∣)  ≡⟨ sym $ subst-∘ _ _ _ ⟩
          subst (λ y → proj₁ (Eq ∣ x ∣ ∣ y ∣)) eq (∣ refl x ∣)         ≡⟨⟩
          subst (λ y → ∥ x ≡ y ∥[1+ n ]) eq (∣ refl x ∣)               ≡⟨ elim¹
                                                                            (λ eq → subst (λ y → ∥ x ≡ y ∥[1+ n ]) eq (∣ refl x ∣) ≡
                                                                                    ∣ subst (x ≡_) eq (refl x) ∣)
                                                                            (trans (subst-refl _ _) $
                                                                             cong ∣_∣ $ sym $ subst-refl _ _)
                                                                            _ ⟩
          ∣ subst (x ≡_) eq (refl x) ∣                                 ≡⟨ cong ∣_∣ $ sym trans-subst ⟩
          ∣ trans (refl x) eq ∣                                        ≡⟨ cong ∣_∣ $ trans-reflˡ _ ⟩∎
          ∣ eq ∣                                                       ∎

_ :
  {A : Type a} {x y : A} {univ : Univalence a}
  {x≡y : x ≡ y} →
  _≃_.to (∥≡∥≃∣∣≡∣∣ {n = n} univ) ∣ x≡y ∣ ≡ cong ∣_∣ x≡y
_ = refl _

-- The truncation operator commutes with _×_.
--
-- This result is similar to Theorem 7.3.8 from the HoTT book.

∥∥×∥∥≃∥×∥ : (∥ A ∥[1+ n ] × ∥ B ∥[1+ n ]) ≃ ∥ A × B ∥[1+ n ]
∥∥×∥∥≃∥×∥ {n} = Eq.↔→≃
  (uncurry $ rec λ where
     .h-levelʳ → Π-closure ext _ λ _ →
                 truncation-has-correct-h-level _
     .∣∣ʳ x    → rec λ where
       .h-levelʳ → truncation-has-correct-h-level _
       .∣∣ʳ y    → ∣ x , y ∣)
  (rec λ where
     .∣∣ʳ      → Σ-map ∣_∣ ∣_∣
     .h-levelʳ → s)
  (elim λ where
     .∣∣ʳ _      → refl _
     .h-levelʳ _ →
       mono₁ (1 + n) $ truncation-has-correct-h-level n)
  (uncurry $ elim λ where
     .h-levelʳ _ → Π-closure ext (1 + n) λ _ →
                   mono₁ (1 + n) s
     .∣∣ʳ _      → elim λ where
       .h-levelʳ _ → mono₁ (1 + n) s
       .∣∣ʳ _      → refl _)
  where
  s = ×-closure _
        (truncation-has-correct-h-level _)
        (truncation-has-correct-h-level _)

-- Nested truncations where the inner truncation's h-level is at least
-- as large as the outer truncation's h-level can be flattened.

flatten-≥ : m ≤ n → ∥ ∥ A ∥[1+ n ] ∥[1+ m ] ↔ ∥ A ∥[1+ m ]
flatten-≥ m≤n = record
  { surjection = record
    { logical-equivalence = record
      { from = ∥∥-map ∣_∣
      ; to   = rec λ where
          .h-levelʳ → truncation-has-correct-h-level _
          .∣∣ʳ      → rec λ where
            .∣∣ʳ      → ∣_∣
            .h-levelʳ → mono (Nat.suc≤suc m≤n)
                             (truncation-has-correct-h-level _)
      }
    ; right-inverse-of = uniqueness
        (truncation-has-correct-h-level _)
        (λ x → ∣ x ∣  ∎)
    }
  ; left-inverse-of = uniqueness
      (truncation-has-correct-h-level _)
      (uniqueness
         (mono (Nat.suc≤suc m≤n)
               (truncation-has-correct-h-level _))
         (λ x → ∣ ∣ x ∣ ∣  ∎))
  }

-- The remainder of this module is not based on the HoTT book.

-- Nested truncations where the inner truncation's h-level is at most
-- as large as the outer truncation's h-level can be flattened.

flatten-≤ : m ≤ n → ∥ ∥ A ∥[1+ m ] ∥[1+ n ] ↔ ∥ A ∥[1+ m ]
flatten-≤ m≤n = record
  { surjection = record
    { logical-equivalence = record
      { from = ∣_∣
      ; to   = rec λ where
          .∣∣ʳ      → id
          .h-levelʳ → mono (Nat.suc≤suc m≤n)
                           (truncation-has-correct-h-level _)
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = uniqueness
      (truncation-has-correct-h-level _)
      (λ x → ∣ x ∣  ∎)
  }

-- Nested truncations can be flattened.

flatten : ∥ ∥ A ∥[1+ m ] ∥[1+ n ] ↔ ∥ A ∥[1+ min m n ]
flatten {A} {m} {n} = case Nat.total m n of λ where
  (inj₁ m≤n) → ∥ ∥ A ∥[1+ m ] ∥[1+ n ]  ↝⟨ flatten-≤ m≤n ⟩
               ∥ A ∥[1+ m ]             ↝⟨ ≡⇒↝ _ $ cong ∥ A ∥[1+_] $ sym $ _⇔_.to Nat.≤⇔min≡ m≤n ⟩□
               ∥ A ∥[1+ min m n ]       □
  (inj₂ m≥n) → ∥ ∥ A ∥[1+ m ] ∥[1+ n ]  ↝⟨ flatten-≥ m≥n ⟩
               ∥ A ∥[1+ n ]             ↝⟨ ≡⇒↝ _ $ cong ∥ A ∥[1+_] $ sym $ _⇔_.to Nat.≤⇔min≡ m≥n ⟩
               ∥ A ∥[1+ min n m ]       ↝⟨ ≡⇒↝ _ $ cong ∥ A ∥[1+_] $ Nat.min-comm _ _ ⟩□
               ∥ A ∥[1+ min m n ]       □

-- The propositional truncation operator ∥_∥ is pointwise isomorphic
-- to ∥_∥[1+ 0 ].

∥∥↔∥∥ : ∥ A ∥ ↔ ∥ A ∥[1+ 0 ]
∥∥↔∥∥ = record
  { surjection = record
    { logical-equivalence = record
      { to   = TP.rec (truncation-has-correct-h-level 0) ∣_∣
      ; from = rec λ where
          .∣∣ʳ      → TP.∣_∣
          .h-levelʳ → TP.truncation-is-proposition
      }
    ; right-inverse-of = λ _ → truncation-has-correct-h-level 0 _ _
    }
  ; left-inverse-of = λ _ → TP.truncation-is-proposition _ _
  }

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

-- A universe-polymorphic variant of bind.

infixl 5 _>>=′_

_>>=′_ : ∥ A ∥[1+ n ] → (A → ∥ B ∥[1+ n ]) → ∥ B ∥[1+ n ]
_>>=′_ {A} {n} {B} = curry (
  ∥ A ∥[1+ n ] × (A → ∥ B ∥[1+ n ])  ↝⟨ uncurry (flip ∥∥-map) ⟩
  ∥ ∥ B ∥[1+ n ] ∥[1+ n ]            ↔⟨ flatten-≤ Nat.≤-refl ⟩□
  ∥ B ∥[1+ n ]                       □)

-- ∥_∥[1+ n ] is a monad.

instance

  monad : Monad {c = ℓ} (∥_∥[1+ n ])
  Raw-monad.return (Monad.raw-monad monad) = ∣_∣

  Raw-monad._>>=_ (Monad.raw-monad monad) = _>>=′_

  Monad.left-identity monad = λ _ _ → refl _

  Monad.right-identity monad =
    uniqueness (truncation-has-correct-h-level _) (λ _ → refl _)

  Monad.associativity monad = flip λ f → flip λ g → uniqueness
    (truncation-has-correct-h-level _)
    (λ x → f x >>=′ g  ∎)

------------------------------------------------------------------------
-- Some preservation lemmas

-- The truncation operator preserves logical equivalences.

∥∥-cong-⇔ : A ⇔ B → ∥ A ∥[1+ n ] ⇔ ∥ B ∥[1+ n ]
∥∥-cong-⇔ A⇔B = record
  { to   = ∥∥-map (_⇔_.to   A⇔B)
  ; from = ∥∥-map (_⇔_.from A⇔B)
  }

-- The truncation operator preserves bijections.

∥∥-cong : A ↔[ k ] B → ∥ A ∥[1+ n ] ↔[ k ] ∥ B ∥[1+ n ]
∥∥-cong {n} A↝B = from-bijection (record
  { surjection = record
    { logical-equivalence = record
      { to   = ∥∥-map (_↔_.to   A↔B)
      ; from = ∥∥-map (_↔_.from A↔B)
      }
    ; right-inverse-of = lemma A↔B
    }
  ; left-inverse-of = lemma (inverse A↔B)
  })
  where
  A↔B = from-isomorphism A↝B

  lemma :
    (A↔B : A ↔ B) (x : ∥ B ∥[1+ n ]) →
    ∥∥-map (_↔_.to A↔B) (∥∥-map (_↔_.from A↔B) x) ≡ x
  lemma A↔B x =
    ∥∥-map (_↔_.to A↔B) (∥∥-map (_↔_.from A↔B) x)  ≡⟨ sym $ ∥∥-map-∘ x ⟩
    ∥∥-map (_↔_.to A↔B ∘ _↔_.from A↔B) x           ≡⟨ cong (λ f → ∥∥-map f x) $ ⟨ext⟩ $ _↔_.right-inverse-of A↔B ⟩
    ∥∥-map id x                                    ≡⟨ ∥∥-map-id x ⟩∎
    x                                              ∎

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

-- ∥ A ∥[1+_] is downwards closed.

downwards-closed : m ≤ n → ∥ A ∥[1+ n ] → ∥ A ∥[1+ m ]
downwards-closed {m} {n} {A} m≤n =
  ∥ A ∥[1+ n ]             ↝⟨ ∥∥-map ∣_∣ ⟩
  ∥ ∥ A ∥[1+ m ] ∥[1+ n ]  ↔⟨ flatten-≤ m≤n ⟩□
  ∥ A ∥[1+ m ]             □

------------------------------------------------------------------------
-- The truncation modality

-- The truncation operator can be turned into a family of modalities.
--
-- This definition is based on "Modalities in Homotopy Type Theory" by
-- Rijke, Shulman and Spitters.

∥∥[1+_]-modality : ℕ → Modality ℓ
∥∥[1+_]-modality {ℓ} n = λ where
    .◯                   → ∥_∥[1+ n ]
    .η                   → ∣_∣
    .Modal               → H-level (1 + n)
    .Modal-propositional → λ ext → H-level-propositional ext (1 + n)
    .Modal-◯             → truncation-has-correct-h-level n
    .Modal-respects-≃    → H-level-cong _ (1 + n)
    .extendable-along-η  → extendable
  where
  open Modality

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

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

∥∥[1+_]-accessible : ∀ n → Accessible (∥∥[1+_]-modality {ℓ = ℓ} n)
∥∥[1+_]-accessible {ℓ} n =
    ↑ ℓ ⊤
  , (λ _ → ↑ ℓ (𝕊 n))
  , (λ A →
       H-level (1 + n) A                                ↔⟨ inverse 𝕊-1-Null≃H-level ⟩
       (λ (_ : ⊤) → 𝕊 n) -Null A                        ↔⟨ PS.Null-cong ext (λ _ → Eq.↔⇒≃ $ inverse B.↑↔) F.id ⟩
       (λ (_ : ⊤) → ↑ ℓ (𝕊 n)) -Null A                  ↔⟨ inverse $ PS.Π-Is-∞-extendable-along≃Null ext ⟩
       (⊤ → Is-∞-extendable-along-[ _ ] (λ _ → A))      ↔⟨ →-cong ext (inverse B.↑↔) F.id ⟩□
       (↑ ℓ ⊤ → Is-∞-extendable-along-[ _ ] (λ _ → A))  □)

-- The truncation modality is empty-modal.

∥∥[1+]-empty-modal : Empty-modal (∥∥[1+_]-modality {ℓ = ℓ} n)
∥∥[1+]-empty-modal = H-level.mono (Nat.m≤m+n 1 _) ⊥-propositional

-- The truncation modality is W-modal.

∥∥[1+]-W-modal : W-modal (∥∥[1+_]-modality {ℓ = ℓ} n)
∥∥[1+]-W-modal = W-closure ext _

-- The truncation modality ∥∥[1+ n ] is accessibility-modal for types
-- and relations with h-level n.

Is-proposition→∥∥[1+]-accessibility-modal :
  {A : Type ℓ} {_<_ : A → A → Type ℓ} →
  H-level (1 + n) A →
  (∀ x y → H-level (1 + n) (x < y)) →
  Modality.Accessibility-modal-for ∥∥[1+ n ]-modality _<_
Is-proposition→∥∥[1+]-accessibility-modal p₁ p₂ =
    (λ acc →
       Modal→Acc→Acc-[]◯-η
         p₁
         (rec λ where
            .∣∣ʳ      → id
            .h-levelʳ → p₂ _ _)
         acc)
  , (rec λ where
       .∣∣ʳ      → id
       .h-levelʳ →
         H-level.mono (Nat.m≤m+n 1 _) (A.Acc-propositional ext))
  where
  open Modality (∥∥[1+_]-modality _)