------------------------------------------------------------------------
-- Idempotent monadic modalities
------------------------------------------------------------------------

-- Unless otherwise noted this code is based on "Modalities in
-- Homotopy Type Theory" by Rijke, Shulman and Spitters, and/or (some
-- version of) the corresponding Coq code. (Details may differ, and
-- perhaps there are some "obvious" results that do not have direct
-- counterparts in the work of Rijke, Shulman and Spitters, even
-- though there is no note about this.)

-- The definitions in this module are reexported from Modality.

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

open import Equality

module Modality.Basics
  {c⁺} (eq-J : ∀ {a p} → Equality-with-J a p c⁺) where

open Derived-definitions-and-properties eq-J

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

open import Accessibility eq-J as A using (Acc; Well-founded; _<W_)
open import Bijection eq-J as Bijection using (_↔_; Has-quasi-inverse)
open import Embedding eq-J as Emb using (Embedding; Is-embedding)
open import Equality.Decision-procedures eq-J
open import Equivalence eq-J as Eq using (_≃_; Is-equivalence)
open import Equivalence.Erased.Basics eq-J as EEq
  using (_≃ᴱ_; Is-equivalenceᴱ)
open import Equivalence.Erased.Contractible-preimages.Basics eq-J
  using (Contractibleᴱ; _⁻¹ᴱ_)
import Equivalence.Half-adjoint eq-J as HA
open import Equivalence.List eq-J
open import Equivalence.Path-split eq-J as PS
  using (_-Null_; Is-∞-extendable-along-[_])
open import Erased.Box-cong-axiomatisation eq-J
  using ([]-cong-axiomatisation)
open import Extensionality eq-J
open import For-iterated-equality eq-J
open import Function-universe eq-J as F hiding (id; _∘_)
open import H-level eq-J as H-level
open import H-level.Closure eq-J
open import Monad eq-J
open import Preimage eq-J as Preimage using (_⁻¹_)
open import Surjection eq-J using (_↠_; Split-surjective)
open import Univalence-axiom eq-J
open import Vec.Dependent eq-J as Vec using (Vec)

private
  variable
    a c d                                    : Level
    A B B₁ B₂ C                              : Type a
    eq f g i k m m₁ m₂ n p s x y z z₁ z₂ _<_ : A
    P Q                                      : A → Type p

------------------------------------------------------------------------
-- Modalities

private
 module Dummy where

  -- The following is a definition of "modality" based on that in (one
  -- version of) the Coq code accompanying "Modalities in Homotopy
  -- Type Theory".
  --
  -- One difference is that in the Coq code the proof showing that the
  -- modality predicate is propositional is allowed to make use of
  -- function extensionality for arbitrary universe levels.

  record Modality-record a : Type (lsuc a) where
    field
      -- The modal operator.
      ◯ : Type a → Type a

      -- The modal unit.
      η : A → ◯ A

      -- A type A is modal if Modal A is inhabited.
      Modal : Type a → Type a

      -- Modal A is propositional (assuming function extensionality).
      Modal-propositional :
        Extensionality a a →
        Is-proposition (Modal A)

      -- ◯ A is modal.
      Modal-◯ : Modal (◯ A)

      -- Modal respects equivalences.
      Modal-respects-≃ : A ≃ B → Modal A → Modal B

      -- Pointwise modal families of type ◯ A → Type a are
      -- ∞-extendable along η.
      extendable-along-η :
        {P : ◯ A → Type a} →
        (∀ x → Modal (P x)) →
        Is-∞-extendable-along-[ η ] P

open Dummy using (module Modality-record)
open Dummy public
  hiding (module Modality-record)
  renaming (Modality-record to Modality)

------------------------------------------------------------------------
-- Uniquely eliminating modalities

-- The following is a definition of "uniquely eliminating modality"
-- based on that in "Modalities in Homotopy Type Theory".

record Uniquely-eliminating-modality a : Type (lsuc a) where
  field
    ◯                    : Type a → Type a
    η                    : A → ◯ A
    uniquely-eliminating :
      Is-equivalence (λ (f : (x : ◯ A) → ◯ (P x)) → f ∘ η)

  ----------------------------------------------------------------------
  -- Some definitions and lemmas

  -- A type is modal if η is an equivalence for this type.

  Modal : Type a → Type a
  Modal A = Is-equivalence (η {A = A})

  -- If A is modal, then A is equivalent to ◯ A.

  Modal→≃◯ : Modal A → A ≃ ◯ A
  Modal→≃◯ m = Eq.⟨ _ , m ⟩

  -- The type (x : ◯ A) → ◯ (P x) is equivalent to
  -- (x : A) → ◯ (P (η x)).

  Π◯◯≃Π◯η : ((x : ◯ A) → ◯ (P x)) ≃ ((x : A) → ◯ (P (η x)))
  Π◯◯≃Π◯η = Eq.⟨ _ , uniquely-eliminating ⟩

  -- A type is stable if ◯ A implies A.

  Stable : Type a → Type a
  Stable A = ◯ A → A

  -- If A is stable, and the stability proof is a left inverse of η,
  -- then A is modal.

  Stable→left-inverse→Modal :
    (s : Stable A) → s ∘ η ≡ id → Modal A
  Stable→left-inverse→Modal {A = A} s s-η =
    _≃_.is-equivalence $
    Eq.↔→≃ η s
      (λ x → cong (_$ x) η-s)
      (λ x → cong (_$ x) s-η)
    where
    contr : Contractible ((λ (f : ◯ A → ◯ A) → f ∘ η) ⁻¹ η)
    contr = Preimage.bijection⁻¹-contractible (_≃_.bijection Π◯◯≃Π◯η) _

    η-s : η ∘ s ≡ id
    η-s =
      η ∘ s               ≡⟨ cong proj₁ $ sym $ contr .proj₂ (η ∘ s , (

        η ∘ s ∘ η              ≡⟨ cong (η ∘_) s-η ⟩
        η ∘ id                 ≡⟨⟩
        η                      ∎)) ⟩

      _≃_.from Π◯◯≃Π◯η η  ≡⟨ cong proj₁ $ contr .proj₂ (id , refl η) ⟩∎
      id                  ∎

  -- The type ◯ A is modal.

  Modal-◯ : Modal (◯ A)
  Modal-◯ {A = A} = Stable→left-inverse→Modal η⁻¹ η⁻¹-η
    where
    η⁻¹ : ◯ (◯ A) → ◯ A
    η⁻¹ = _≃_.from Π◯◯≃Π◯η id

    η⁻¹-η : η⁻¹ ∘ η ≡ id
    η⁻¹-η =
      _≃_.from Π◯◯≃Π◯η id ∘ η       ≡⟨⟩
      (_∘ η) (_≃_.from Π◯◯≃Π◯η id)  ≡⟨ _≃_.right-inverse-of Π◯◯≃Π◯η _ ⟩∎
      id                            ∎

  -- If P : ◯ A → Type a is pointwise modal, then it is ∞-extendable
  -- along η (assuming function extensionality).

  extendable-along-η :
    {P : ◯ A → Type a} →
    Extensionality a a →
    (∀ x → Modal (P x)) →
    Is-∞-extendable-along-[ η ] P
  extendable-along-η {A = A} {P = P} ext m =          $⟨ equiv ⟩
    Is-equivalence (λ (f : (x : ◯ A) → P x) → f ∘ η)  ↝⟨ inverse $ PS.Is-∞-extendable-along≃Is-equivalence ext ⟩□
    Is-∞-extendable-along-[ η ] P                     □
    where
    equiv : Is-equivalence (λ (f : (x : ◯ A) → P x) → f ∘ η)
    equiv =
      _≃_.is-equivalence $
      Eq.with-other-function
        (((x : ◯ A) → P x)        ↝⟨ ∀-cong ext (Modal→≃◯ ∘ m) ⟩
         ((x : ◯ A) → ◯ (P x))    ↝⟨ Π◯◯≃Π◯η ⟩
         ((x : A) → ◯ (P (η x)))  ↝⟨ ∀-cong ext (inverse ∘ Modal→≃◯ ∘ m ∘ η) ⟩□
         ((x : A) → P (η x))      □)
        (_∘ η)
        (λ f → apply-ext ext λ x →
           _≃_.from (Modal→≃◯ (m (η x))) (η (f (η x)))  ≡⟨ _≃_.left-inverse-of (Modal→≃◯ (m (η x))) _ ⟩∎
           f (η x)                                      ∎)

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

  -- A dependent eliminator for ◯.

  ◯-elim :
    {P : ◯ A → Type a} →
    (∀ x → Modal (P x)) →
    ((x : A) → P (η x)) →
    ((x : ◯ A) → P x)
  ◯-elim {A = A} {P = P} m =
    ((x : A) → P (η x))      →⟨ η ∘_ ⟩
    ((x : A) → ◯ (P (η x)))  ↔⟨ inverse Π◯◯≃Π◯η ⟩
    ((x : ◯ A) → ◯ (P x))    →⟨ _≃_.from (Modal→≃◯ (m _)) ∘_ ⟩□
    ((x : ◯ A) → P x)        □

  -- A "computation rule" for ◯-elim.

  ◯-elim-η :
    {P : ◯ A → Type a} {f : (x : A) → P (η x)}
    (m : ∀ x → Modal (P x)) →
    ◯-elim m f (η x) ≡ f x
  ◯-elim-η {x = x} {P = P} {f = f} m =
    _≃_.from (Modal→≃◯ (m _))
      (_≃_.from (Π◯◯≃Π◯η {P = P}) (η ∘ f) (η x))         ≡⟨⟩

    _≃_.from (Modal→≃◯ (m _))
      (((_∘ η) (_≃_.from (Π◯◯≃Π◯η {P = P}) (η ∘ f))) x)  ≡⟨ cong (_≃_.from (Modal→≃◯ (m _))) $ cong (_$ x) $
                                                            _≃_.right-inverse-of Π◯◯≃Π◯η _ ⟩

    _≃_.from (Modal→≃◯ (m _)) (η (f x))                  ≡⟨ _≃_.left-inverse-of (Modal→≃◯ (m _)) _ ⟩∎

    f x                                                  ∎

  -- A non-dependent eliminator for ◯.

  ◯-rec : Modal B → (A → B) → (◯ A → B)
  ◯-rec m = ◯-elim (λ _ → m)

  -- A "computation rule" for ◯-rec.

  ◯-rec-η : ∀ m → ◯-rec m f (η x) ≡ f x
  ◯-rec-η m = ◯-elim-η (λ _ → m)

  ----------------------------------------------------------------------
  -- More lemmas

  -- A map function for ◯.

  ◯-map : (A → B) → ◯ A → ◯ B
  ◯-map f = ◯-rec Modal-◯ (η ∘ f)

  -- A "computation rule" for ◯-map.

  ◯-map-η : ◯-map f (η x) ≡ η (f x)
  ◯-map-η = ◯-rec-η Modal-◯

  -- Modal respects equivalences (assuming function extensionality).

  Modal-respects-≃ :
    Extensionality a a →
    A ≃ B → Modal A → Modal B
  Modal-respects-≃ {A = A} {B = B} ext A≃B m =
    Stable→left-inverse→Modal
      (◯ B  →⟨ ◯-map (_≃_.from A≃B) ⟩
       ◯ A  →⟨ _≃_.from $ Modal→≃◯ m ⟩
       A    →⟨ _≃_.to A≃B ⟩□
       B    □)
      (apply-ext ext λ x →

       _≃_.to A≃B (_≃_.from (Modal→≃◯ m) (◯-map (_≃_.from A≃B) (η x)))  ≡⟨ cong (_≃_.to A≃B ∘ _≃_.from (Modal→≃◯ m)) ◯-map-η ⟩
       _≃_.to A≃B (_≃_.from (Modal→≃◯ m) (η (_≃_.from A≃B x)))          ≡⟨ cong (_≃_.to A≃B) $ _≃_.left-inverse-of (Modal→≃◯ m) _ ⟩
       _≃_.to A≃B (_≃_.from A≃B x)                                      ≡⟨ _≃_.right-inverse-of A≃B _ ⟩∎
       x                                                                ∎)

  -- A uniquely eliminating modality is a modality (assuming function
  -- extensionality).
  --
  -- See also Modality.uniquely-eliminating below.

  modality :
    Extensionality a a →
    Modality a
  modality ext = λ where
    .Modality-record.◯ → ◯

    .Modality-record.η → η

    .Modality-record.Modal → Modal

    .Modality-record.Modal-propositional →
      Is-equivalence-propositional

    .Modality-record.Modal-◯ → Modal-◯

    .Modality-record.Modal-respects-≃ → Modal-respects-≃ ext

    .Modality-record.extendable-along-η → extendable-along-η ext

------------------------------------------------------------------------
-- Σ-closed reflective subuniverses

-- The Coq code accompanying "Modalities in Homotopy Type Theory" uses
-- a somewhat different definition of reflective subuniverses than the
-- paper:
-- * The definition has been adapted to Coq's notion of universe
--   polymorphism.
-- * The proof showing that the modality predicate is propositional is
--   allowed to make use of function extensionality for arbitrary
--   universe levels.
-- * One extra property is assumed: if A and B are equivalent and A is
--   modal, then B is modal.
-- * The property stating that λ (f : ◯ A → B) → f ∘ η is an
--   equivalence for all types A and modal types B is replaced by a
--   property that is intended to avoid uses of extensionality. This
--   property is stated using Is-∞-extendable-along-[_].
-- (This refers to one version of the code, which seems to have
-- changed since I first looked at it.)
--
-- Here is a definition of Σ-closed reflective subuniverses that is
-- based on the definition of reflective subuniverses in (one version
-- of) the Coq code of Rijke et al. Note that Modal-propositional is
-- only given access to function extensionality for a given universe
-- level.

record Σ-closed-reflective-subuniverse a : Type (lsuc a) where
  field
    ◯     : Type a → Type a
    η     : A → ◯ A
    Modal : Type a → Type a

    Modal-propositional :
      Extensionality a a →
      Is-proposition (Modal A)

    Modal-◯ : Modal (◯ A)

    Modal-respects-≃ : A ≃ B → Modal A → Modal B

    extendable-along-η :
      Modal B → Is-∞-extendable-along-[ η ] (λ (_ : ◯ A) → B)

    Σ-closed : Modal A → (∀ x → Modal (P x)) → Modal (Σ A P)

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

  -- A non-dependent eliminator for ◯.

  ◯-rec : Modal B → (A → B) → (◯ A → B)
  ◯-rec m f = extendable-along-η m  .proj₁ f .proj₁

  -- A "computation rule" for ◯-rec.

  ◯-rec-η : ◯-rec m f (η x) ≡ f x
  ◯-rec-η = extendable-along-η _  .proj₁ _ .proj₂ _

  -- If f and g have type ◯ A → B, where B is modal, and f ∘ η and
  -- g ∘ η are pointwise equal, then f and g are pointwise equal.

  ∘η≡∘η→≡ :
    {f g : ◯ A → B} →
    Modal B →
    (∀ x → f (η x) ≡ g (η x)) →
    ∀ x → f x ≡ g x
  ∘η≡∘η→≡ m p =
    extendable-along-η m  .proj₂ _ _ .proj₁ p .proj₁

  -- A "computation rule" for ∘η≡∘η→≡.

  ∘η≡∘η→≡-η : ∘η≡∘η→≡ m p (η x) ≡ p x
  ∘η≡∘η→≡-η =
    extendable-along-η _  .proj₂ _ _ .proj₁ _ .proj₂ _

  -- A dependent eliminator for ◯.

  ◯-elim :
    {P : ◯ A → Type a} →
    (∀ x → Modal (P x)) →
    ((x : A) → P (η x)) →
    ((x : ◯ A) → P x)
  ◯-elim {A = A} {P = P} m f x =
    subst P (lemma x) (f′ x .proj₂)
    where
    f′ : ◯ A → Σ (◯ A) P
    f′ = ◯-rec (Σ-closed Modal-◯ m) (λ x → η x , f x)

    lemma : ∀ x → f′ x .proj₁ ≡ x
    lemma = ∘η≡∘η→≡ Modal-◯ λ x →
      ◯-rec (Σ-closed Modal-◯ m) (λ x → η x , f x) (η x) .proj₁  ≡⟨ cong proj₁ ◯-rec-η ⟩∎
      η x                                                        ∎

  -- A "computation rule" for ◯-elim.

  ◯-elim-η :
    {P : ◯ A → Type a}
    {m : ∀ x → Modal (P x)}
    {f : (x : A) → P (η x)} →
    ◯-elim m f (η x) ≡ f x
  ◯-elim-η {x = x} {P = P} {m = m} {f = f} =
    subst P (∘η≡∘η→≡ Modal-◯ (λ _ → cong proj₁ ◯-rec-η) (η x))
      (◯-rec (Σ-closed Modal-◯ m) (λ x → η x , f x) (η x) .proj₂)  ≡⟨ cong (flip (subst P) _) ∘η≡∘η→≡-η ⟩

    subst P (cong proj₁ ◯-rec-η)
      (◯-rec (Σ-closed Modal-◯ m) (λ x → η x , f x) (η x) .proj₂)  ≡⟨ sym $ subst-∘ _ _ _ ⟩

    subst (P ∘ proj₁) ◯-rec-η
      (◯-rec (Σ-closed Modal-◯ m) (λ x → η x , f x) (η x) .proj₂)  ≡⟨ elim₁
                                                                        (λ {y} eq → subst (P ∘ proj₁) eq (y .proj₂) ≡ f x)
                                                                        (subst-refl _ _)
                                                                        _ ⟩∎
    f x                                                            ∎

  ----------------------------------------------------------------------
  -- Some basic definitions and lemmas

  -- If η is an equivalence for A, then A is modal.

  Is-equivalence-η→Modal :
    Is-equivalence (η {A = A}) → Modal A
  Is-equivalence-η→Modal {A = A} =
    Is-equivalence (η {A = A})  →⟨ Eq.⟨ _ ,_⟩ ⟩
    A ≃ ◯ A                     →⟨ Modal-respects-≃ ∘ inverse ⟩
    (Modal (◯ A) → Modal A)     →⟨ _$ Modal-◯ ⟩□
    Modal A                     □

  -- A type is stable if ◯ A implies A.

  Stable : Type a → Type a
  Stable A = ◯ A → A

  -- If A is stable, and the stability proof is a left inverse of η,
  -- then A is modal.

  Stable→left-inverse→Modal :
    (s : Stable A) → (∀ x → s (η x) ≡ x) → Modal A
  Stable→left-inverse→Modal s eq =
    Is-equivalence-η→Modal $
    _≃_.is-equivalence $
    Eq.↔→≃
      _
      s
      (∘η≡∘η→≡ Modal-◯ (cong η ∘ eq))
      eq

  -- A type is separated if equality is modal for this type.
  --
  -- This definition is taken from "Localization in homotopy type
  -- theory" by Christensen, Opie, Rijke and Scoccola.

  Separated : Type a → Type a
  Separated = For-iterated-equality  Modal

  -- If a type is modal, then it is separated.

  Modal→Separated : Modal A → Separated A
  Modal→Separated m x y =
    Stable→left-inverse→Modal
      (◯ (x ≡ y)  →⟨ ∘η≡∘η→≡
                       {f = λ (_ : ◯ (x ≡ y)) → x}
                       {g = λ (_ : ◯ (x ≡ y)) → y}
                       m
                       id ⟩□
       x ≡ y      □)
      (λ _ → ∘η≡∘η→≡-η)

  -- One can strengthen extendable-along-η.

  stronger-extendable-along-η :
    {P : ◯ A → Type a} →
    (∀ x → Modal (P x)) →
    Is-∞-extendable-along-[ η ] P
  stronger-extendable-along-η m zero    = _
  stronger-extendable-along-η m (suc n) =
      (λ f → ◯-elim m f , λ _ → ◯-elim-η)
    , λ _ _ →
        stronger-extendable-along-η
          (λ x → Modal→Separated (m x) _ _) n

  -- A Σ-closed reflective subuniverse is a modality.
  --
  -- See also Modality.Σ-closed below.

  modality : Modality a
  modality = λ where
    .Modality-record.◯                   → ◯
    .Modality-record.η                   → η
    .Modality-record.Modal               → Modal
    .Modality-record.Modal-propositional → Modal-propositional
    .Modality-record.Modal-◯             → Modal-◯
    .Modality-record.Modal-respects-≃    → Modal-respects-≃
    .Modality-record.extendable-along-η  → stronger-extendable-along-η

------------------------------------------------------------------------
-- Connectedness

-- ◯ -Connected A means that A is ◯-connected.

_-Connected_ : (Type a → Type a) → Type a → Type a
◯ -Connected A = Contractible (◯ A)

-- ◯ -Connected-→ f means that f is ◯-connected.

_-Connected-→_ :
  {A B : Type a} →
  (Type a → Type a) → (A → B) → Type a
◯ -Connected-→ f = ∀ y → ◯ -Connected (f ⁻¹ y)

-- ◯ -Connected A is propositional (assuming function extensionality).

Connected-propositional :
  Extensionality a a →
  (◯ : Type a → Type a) →
  Is-proposition (◯ -Connected A)
Connected-propositional ext _ = H-level-propositional ext 

-- ◯ -Connected-→ f is propositional (assuming function
-- extensionality).

Connected-→-propositional :
  Extensionality a a →
  (◯ : Type a → Type a) →
  Is-proposition (◯ -Connected-→ f)
Connected-→-propositional ext ◯ =
  Π-closure ext  λ _ →
  Connected-propositional ext ◯

-- I did not take the remaining definitions in this section from
-- "Modalities in Homotopy Type Theory" or the corresponding Coq code.

-- _-Connectedᴱ_ is a variant of _-Connected_ that uses Contractibleᴱ
-- instead of Contractible.
--
-- See also Modality.Connectedᴱ-propositional.

_-Connectedᴱ_ : (Type a → Type a) → Type a → Type a
◯ -Connectedᴱ A = Contractibleᴱ (◯ A)

-- _-Connected-→ᴱ_ is a variant of _-Connected→_ that uses
-- _-Connectedᴱ_ instead of _-Connected_ and _⁻¹ᴱ_ instead of _⁻¹_.
--
-- See also Modality.Connected-→ᴱ-propositional.

_-Connected-→ᴱ_ :
  {A B : Type a} →
  (Type a → Type a) → (A → B) → Type a
◯ -Connected-→ᴱ f = ∀ y → ◯ -Connectedᴱ (f ⁻¹ᴱ y)

------------------------------------------------------------------------
-- Some definitions

-- A definition of what it means for a modality to be left exact,
-- based on Theorem 3.1 (i) in "Modalities in Homotopy Type Theory".

Left-exact : (Type a → Type a) → Type (lsuc a)
Left-exact {a = a} ◯ =
  {A : Type a} {x y : A} →
  ◯ -Connected A → ◯ -Connected (x ≡ y)

-- Left-exact ◯ is propositional (assuming function extensionality).

Left-exact-propositional :
  {◯ : Type a → Type a} →
  Extensionality (lsuc a) a →
  Is-proposition (Left-exact ◯)
Left-exact-propositional {◯ = ◯} ext =
  implicit-Π-closure ext   λ _ →
  implicit-Π-closure ext′  λ _ →
  implicit-Π-closure ext′  λ _ →
  Π-closure ext′  λ _ →
  Connected-propositional ext′ ◯
  where
  ext′ = lower-extensionality _ lzero ext

-- A definition of what it means for a modality to be accessible.
--
-- This definition is based on (one version of) the Coq code
-- accompanying "Modalities in Homotopy Type Theory". Originally I had
-- allowed I and P to target a different, possibly larger universe,
-- because I had missed that the two universe levels occurring in the
-- Coq code were not unconstrained. However, it was pointed out to me
-- by Felix Cherubini and Christian Sattler (and perhaps someone else)
-- that my definition was not correct.

Accessible : Modality a → Type (lsuc a)
Accessible {a = a} M =
  ∃ λ (I : Type a) →
  ∃ λ (P : I → Type a) →
    (A : Type a) →
    Modal A ⇔
    ∀ i →
    Is-∞-extendable-along-[ (λ (_ : P i) → lift tt) ]
      (λ (_ : ↑ a ⊤) → A)
  where
  open Modality-record M

-- A definition of what it means for a modality to be topological.
--
-- This definition is based on (one version of) the Coq code
-- accompanying "Modalities in Homotopy Type Theory".

Topological : Modality a → Type (lsuc a)
Topological M =
  ∃ λ ((_ , P , _) : Accessible M) →
    ∀ i → Is-proposition (P i)

-- A definition of what it means for a modality to be cotopological.

Cotopological : (Type a → Type a) → Type (lsuc a)
Cotopological {a = a} ◯ =
  Left-exact ◯ ×
  ({A : Type a} → Is-proposition A → ◯ -Connected A → Contractible A)

-- Cotopological ◯ is propositional (assuming function extensionality).

Cotopological-propositional :
  {◯ : Type a → Type a} →
  Extensionality (lsuc a) a →
  Is-proposition (Cotopological ◯)
Cotopological-propositional {◯ = ◯} ext =
  ×-closure  (Left-exact-propositional ext) $
  implicit-Π-closure ext   λ _ →
  Π-closure          ext′  λ _ →
  Π-closure          ext′  λ _ →
  H-level-propositional ext′ 
  where
  ext′ = lower-extensionality _ lzero ext

-- I did not take the remaining definitions in this section from
-- "Modalities in Homotopy Type Theory" or the corresponding Coq code
-- (but "Modal ⊥" is used in the Coq code).

-- A modality is called empty-modal if the empty type is modal.

Empty-modal : Modality a → Type a
Empty-modal M = Modal ⊥
  where
  open Modality-record M

-- Empty-modal M is propositional (assuming function extensionality).

Empty-modal-propositional :
  {M : Modality a} →
  Extensionality a a →
  Is-proposition (Empty-modal M)
Empty-modal-propositional {M = M} ext =
  Modal-propositional ext
  where
  open Modality-record M

-- A modality is called "very modal" if ◯ (Modal A) always holds.
--
-- I did not take this definition from "Modalities in Homotopy Type
-- Theory" or the corresponding Coq code.
--
-- See also Modality.Very-modal-propositional.

Very-modal : Modality a → Type (lsuc a)
Very-modal {a = a} M = {A : Type a} → ◯ (Modal A)
  where
  open Modality-record M

-- A modality of type Modality a is W-modal if W A P is modal whenever
-- A is modal (for any A : Type a and P : A → Type a).

W-modal : Modality a → Type (lsuc a)
W-modal {a = a} M =
  {A : Type a} {P : A → Type a} →
  Modal A → Modal (W A P)
  where
  open Modality-record M

-- W-modal M is propositional (assuming function extensionality).

W-modal-propositional :
  {M : Modality a} →
  Extensionality (lsuc a) (lsuc a) →
  Is-proposition (W-modal M)
W-modal-propositional {M = M} ext =
  implicit-Π-closure ext  λ _ →
  implicit-Π-closure (lower-extensionality lzero _ ext)  λ _ →
  Π-closure (lower-extensionality _ _ ext)  λ _ →
  Modal-propositional (lower-extensionality _ _ ext)
  where
  open Modality-record M

------------------------------------------------------------------------
-- Some results that hold for every modality

module Modality (M : Modality a) where

  open Modality-record M public

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

  -- The eliminators are abstract in order to make types printed by
  -- Agda potentially easier to read.

  abstract

    -- An eliminator for ◯.

    ◯-elim :
      {P : ◯ A → Type a} →
      (∀ x → Modal (P x)) →
      ((x : A) → P (η x)) →
      ((x : ◯ A) → P x)
    ◯-elim m f = extendable-along-η m  .proj₁ f .proj₁

    -- A "computation rule" for ◯-elim.

    ◯-elim-η : ◯-elim m f (η x) ≡ f x
    ◯-elim-η {m = m} {f = f} {x = x} =
      extendable-along-η m  .proj₁ f .proj₂ x

    -- A non-dependent eliminator for ◯.

    ◯-rec : Modal B → (A → B) → (◯ A → B)
    ◯-rec m = ◯-elim (λ _ → m)

    -- A "computation rule" for ◯-rec.

    ◯-rec-η : ◯-rec m f (η x) ≡ f x
    ◯-rec-η = ◯-elim-η

    -- If f and g have type (x : ◯ A) → P x, where P x is modal for
    -- all x, and f ∘ η and g ∘ η are pointwise equal, then f and g
    -- are pointwise equal.

    ∘η≡∘η→≡ :
      {f g : (x : ◯ A) → P x} →
      (∀ x → Modal (P x)) →
      (∀ x → f (η x) ≡ g (η x)) →
      ∀ x → f x ≡ g x
    ∘η≡∘η→≡ m p =
      extendable-along-η m  .proj₂ _ _ .proj₁ p .proj₁

    -- A "computation rule" for ∘η≡∘η→≡.

    ∘η≡∘η→≡-η : ∘η≡∘η→≡ m p (η x) ≡ p x
    ∘η≡∘η→≡-η {m = m} {p = p} =
      extendable-along-η m  .proj₂ _ _ .proj₁ p .proj₂ _

  ----------------------------------------------------------------------
  -- Some basic definitions and lemmas

  -- If η is an equivalence for A, then A is modal.

  Is-equivalence-η→Modal :
    Is-equivalence (η {A = A}) → Modal A
  Is-equivalence-η→Modal {A = A} =
    Is-equivalence (η {A = A})  →⟨ Eq.⟨ _ ,_⟩ ⟩
    A ≃ ◯ A                     →⟨ Modal-respects-≃ ∘ inverse ⟩
    (Modal (◯ A) → Modal A)     →⟨ _$ Modal-◯ ⟩□
    Modal A                     □

  -- A type is stable if ◯ A implies A.

  Stable : Type a → Type a
  Stable A = ◯ A → A

  -- If A is stable, and the stability proof is a left inverse of η,
  -- then A is modal.

  Stable→left-inverse→Modal :
    (s : Stable A) → (∀ x → s (η x) ≡ x) → Modal A
  Stable→left-inverse→Modal s eq =
    Is-equivalence-η→Modal $
    _≃_.is-equivalence $
    Eq.↔→≃
      _
      s
      (∘η≡∘η→≡ (λ _ → Modal-◯) (cong η ∘ eq))
      eq

  -- Stable propositions are modal.

  Stable→Is-proposition→Modal :
    Stable A → Is-proposition A → Modal A
  Stable→Is-proposition→Modal s prop =
    Stable→left-inverse→Modal s (λ _ → prop _ _)

  -- A type is separated if equality is modal for this type.
  --
  -- This definition is taken from "Localization in homotopy type
  -- theory" by Christensen, Opie, Rijke and Scoccola.

  Separated : Type a → Type a
  Separated = For-iterated-equality  Modal

  -- If a type is modal, then it is separated.

  Modal→Separated : Modal A → Separated A
  Modal→Separated m x y =
    Stable→left-inverse→Modal
      (◯ (x ≡ y)  →⟨ ∘η≡∘η→≡
                       {f = λ (_ : ◯ (x ≡ y)) → x}
                       {g = λ (_ : ◯ (x ≡ y)) → y}
                       (λ _ → m)
                       id ⟩□
       x ≡ y      □)
      (λ _ → ∘η≡∘η→≡-η)

  -- The type ◯ A is separated.

  Separated-◯ : Separated (◯ A)
  Separated-◯ = Modal→Separated Modal-◯

  -- If ◯ (x ≡ y) holds, then η x is equal to η y.

  η-cong : ◯ (x ≡ y) → η x ≡ η y
  η-cong = ◯-rec (Separated-◯ _ _) (cong η)

  -- A "computation rule" for η-cong.

  η-cong-η : η-cong (η p) ≡ cong η p
  η-cong-η = ◯-rec-η

  -- A is modal if and only if η is an equivalence for A.

  Modal≃Is-equivalence-η :
    Modal A ↝[ a ∣ a ] Is-equivalence (η {A = A})
  Modal≃Is-equivalence-η =
    generalise-ext?-prop
      (record
         { to = λ m →
             _≃_.is-equivalence $
             Eq.↔→≃
               _
               (◯-rec m id)
               (◯-elim
                  (λ _ → Separated-◯ _ _)
                  (λ _ → cong η ◯-rec-η))
               (λ _ → ◯-rec-η)
         ; from = Is-equivalence-η→Modal
         })
      Modal-propositional
      Is-equivalence-propositional

  -- If A is modal, then A is equivalent to ◯ A.

  Modal→≃◯ : Modal A → A ≃ ◯ A
  Modal→≃◯ m = Eq.⟨ _ , Modal≃Is-equivalence-η _ m ⟩

  -- If A is modal, then η is an embedding for A.

  Modal→Is-embedding-η :
    Modal A → Is-embedding (η ⦂ (A → ◯ A))
  Modal→Is-embedding-η m =
    Emb.Is-equivalence→Is-embedding
      (Modal≃Is-equivalence-η _ m)

  -- For modal types the function η has an inverse.

  η⁻¹ : Modal A → ◯ A → A
  η⁻¹ m = _≃_.from (Modal→≃◯ m)

  η-η⁻¹ : η (η⁻¹ m x) ≡ x
  η-η⁻¹ = _≃_.right-inverse-of (Modal→≃◯ _) _

  η⁻¹-η : η⁻¹ m (η x) ≡ x
  η⁻¹-η = _≃_.left-inverse-of (Modal→≃◯ _) _

  -- When proving that A is modal one can assume that ◯ A is
  -- inhabited.

  [◯→Modal]→Modal : (◯ A → Modal A) → Modal A
  [◯→Modal]→Modal m =
    Is-equivalence-η→Modal $
    HA.[inhabited→Is-equivalence]→Is-equivalence $
    Modal≃Is-equivalence-η _ ∘ m

  -- The function subst can sometimes be "pushed" through η.

  subst-η : subst (◯ ∘ P) eq (η p) ≡ η (subst P eq p)
  subst-η {P = P} {eq = eq} {p = p} =
    elim¹
      (λ eq → ∀ p → subst (◯ ∘ P) eq (η p) ≡ η (subst P eq p))
      (λ p →
         subst (◯ ∘ P) (refl _) (η p)  ≡⟨ subst-refl _ _ ⟩
         η p                           ≡⟨ cong η $ sym $ subst-refl _ _ ⟩∎
         η (subst P (refl _) p)        ∎)
      eq p

  ----------------------------------------------------------------------
  -- Some closure properties related to Modal

  -- The unit type (lifted) is modal.

  Modal-⊤ : Modal (↑ a ⊤)
  Modal-⊤ = Stable→left-inverse→Modal _ refl

  -- Modal is closed under "Π A" (assuming function
  -- extensionality).

  Modal-Π :
    {A : Type a} {P : A → Type a} →
    Extensionality a a →
    (∀ x → Modal (P x)) → Modal ((x : A) → P x)
  Modal-Π ext m =
    Stable→left-inverse→Modal
      (λ f x → ◯-rec (m x) (_$ x) f)
      (λ f → apply-ext ext λ x →
         ◯-rec (m x) (_$ x) (η f)  ≡⟨ ◯-rec-η ⟩∎
         f x                       ∎)

  -- Modal is closed under Σ.

  Modal-Σ : Modal A → (∀ x → Modal (P x)) → Modal (Σ A P)
  Modal-Σ {P = P} mA mP =
    Stable→left-inverse→Modal
      (λ p →
           ◯-rec mA proj₁ p
         , ◯-elim
             (mP ∘ ◯-rec mA proj₁)
             (subst P (sym ◯-rec-η) ∘ proj₂)
             p)
      (λ (x , y) →
         Σ-≡,≡→≡
           ◯-rec-η
           (subst P ◯-rec-η
              (◯-elim
                 (mP ∘ ◯-rec mA proj₁)
                 (subst P (sym ◯-rec-η) ∘ proj₂)
                 (η (x , y)))                          ≡⟨ cong (subst P ◯-rec-η) ◯-elim-η ⟩

            subst P ◯-rec-η (subst P (sym ◯-rec-η) y)  ≡⟨ subst-subst-sym _ _ _ ⟩∎

            y                                          ∎))

  -- A generalisation of Modal-Σ.

  Modal-Σ≃Π-Modal :
    Modal A →
    Modal (Σ A P) ↝[ a ∣ a ] (∀ x → Modal (P x))
  Modal-Σ≃Π-Modal {A = A} {P = P} m =
    generalise-ext?-prop
      (record
         { from = Modal-Σ m
         ; to   = flip λ x →
             Modal (Σ A P)                          ↝⟨ flip Modal-Σ (λ _ → Modal→Separated m _ _) ⟩
             Modal (∃ λ ((y , _) : Σ A P) → y ≡ x)  ↝⟨ Modal-respects-≃ $ from-bijection $ inverse Σ-assoc ⟩
             Modal (∃ λ (y : A) → P y × y ≡ x)      ↝⟨ Modal-respects-≃ $ from-bijection $ inverse $ ∃-intro _ _ ⟩□
             Modal (P x)                            □
         })
      Modal-propositional
      (λ ext →
         Π-closure ext  λ _ →
         Modal-propositional ext)

  -- If A is modal, then Contractible A is modal (assuming function
  -- extensionality).

  Modal-Contractible :
    Extensionality a a →
    Modal A → Modal (Contractible A)
  Modal-Contractible ext m =
    Modal-Σ m λ _ →
    Modal-Π ext λ _ →
    Modal→Separated m _ _

  -- If f has type A → B, where A is modal and B is separated, then
  -- f ⁻¹ y is modal.

  Modal-⁻¹ :
    {f : A → B} →
    Modal A →
    Separated B →
    Modal (f ⁻¹ y)
  Modal-⁻¹ m s = Modal-Σ m λ _ → s _ _

  -- If f has type A → B, where A and B are separated, then
  -- HA.Proofs f g is modal (assuming function extensionality).

  Modal-Half-adjoint-proofs :
    {f : A → B} →
    Extensionality a a →
    Separated A →
    Separated B →
    Modal (HA.Proofs f g)
  Modal-Half-adjoint-proofs ext sA sB =
    Modal-Σ (Modal-Π ext λ _ → sB _ _) λ _ →
    Modal-Σ (Modal-Π ext λ _ → sA _ _) λ _ →
    Modal-Π ext λ _ → Modal→Separated (sB _ _) _ _

  -- If f has type A → B, where A is modal and B is separated, then
  -- Is-equivalence f is modal (assuming function extensionality).

  Modal-Is-equivalence :
    {f : A → B} →
    Extensionality a a →
    Modal A →
    Separated B →
    Modal (Is-equivalence f)
  Modal-Is-equivalence ext m s =
    Modal-Σ (Modal-Π ext λ _ → m) λ _ →
    Modal-Half-adjoint-proofs ext (Modal→Separated m) s

  -- If A and B are modal, then A ≃ B is modal (assuming function
  -- extensionality).

  Modal-≃ :
    Extensionality a a →
    Modal A → Modal B → Modal (A ≃ B)
  Modal-≃ ext mA mB =
    Modal-respects-≃ (inverse $ Eq.↔⇒≃ Eq.≃-as-Σ) $
    Modal-Σ (Modal-Π ext λ _ → mB) λ _ →
    Modal-Is-equivalence ext mA (Modal→Separated mB)

  -- I did not take the remaining results in this section from
  -- "Modalities in Homotopy Type Theory" or the corresponding Coq
  -- code (but that does not mean that one cannot find something
  -- similar in those places).

  -- If A is "modal n levels up", then H-level′ n A is modal (assuming
  -- function extensionality).

  Modal-H-level′ :
    Extensionality a a →
    ∀ n →
    For-iterated-equality n Modal A →
    Modal (H-level′ n A)
  Modal-H-level′ {A = A} ext n =
    For-iterated-equality n Modal A                   ↝⟨ For-iterated-equality-cong₁ _ n (Modal-Contractible ext) ⟩
    For-iterated-equality n (Modal ∘ Contractible) A  ↝⟨ For-iterated-equality-commutes-← _ Modal n (Modal-Π ext) ⟩□
    Modal (H-level′ n A)                              □

  -- If A is "modal n levels up", then H-level n A is modal (assuming
  -- function extensionality).

  Modal-H-level :
    Extensionality a a →
    ∀ n →
    For-iterated-equality n Modal A →
    Modal (H-level n A)
  Modal-H-level {A = A} ext n =
    For-iterated-equality n Modal A  ↝⟨ Modal-H-level′ ext n ⟩
    Modal (H-level′ n A)             ↝⟨ Modal-respects-≃ (inverse $ H-level↔H-level′ ext) ⟩□
    Modal (H-level n A)              □

  -- Some generalisations of Modal→Separated.

  Modalⁿ→Modal¹⁺ⁿ :
    ∀ n →
    For-iterated-equality n       Modal A →
    For-iterated-equality ( + n) Modal A
  Modalⁿ→Modal¹⁺ⁿ {A = A} n =
    For-iterated-equality n Modal A        →⟨ For-iterated-equality-cong₁ _ n Modal→Separated ⟩
    For-iterated-equality n Separated A    →⟨ For-iterated-equality-For-iterated-equality n  _ ⟩□
    For-iterated-equality ( + n) Modal A  □

  Modal→Modalⁿ :
    ∀ n →
    Modal A →
    For-iterated-equality n Modal A
  Modal→Modalⁿ zero = id
  Modal→Modalⁿ {A = A} (suc n) =
    Modal A                                →⟨ Modal→Modalⁿ n ⟩
    For-iterated-equality n Modal A        →⟨ Modalⁿ→Modal¹⁺ⁿ n ⟩□
    For-iterated-equality (suc n) Modal A  □

  ----------------------------------------------------------------------
  -- The function ◯-map

  -- The function ◯-map is abstract in order to make types printed by
  -- Agda potentially easier to read.

  abstract

    -- A map function for ◯.

    ◯-map : (A → B) → ◯ A → ◯ B
    ◯-map f = ◯-rec Modal-◯ (η ∘ f)

    -- A "computation rule" for ◯-map.

    ◯-map-η : ◯-map f (η x) ≡ η (f x)
    ◯-map-η = ◯-rec-η

  -- ◯-map id is pointwise equal to id.

  ◯-map-id : {x : ◯ A} → ◯-map id x ≡ id x
  ◯-map-id =
    ◯-elim
      {P = λ x → ◯-map id x ≡ x}
      (λ _ → Separated-◯ _ _)
      (λ x →
         ◯-map id (η x)  ≡⟨ ◯-map-η ⟩∎
         η x             ∎)
      _

  -- ◯-map commutes with composition (pointwise).

  ◯-map-∘ :
    {f : B → C} {g : A → B} →
    ◯-map (f ∘ g) x ≡ (◯-map f ∘ ◯-map g) x
  ◯-map-∘ {f = f} {g = g} =
    ◯-elim
      {P = λ x → ◯-map (f ∘ g) x ≡ ◯-map f (◯-map g x)}
      (λ _ → Separated-◯ _ _)
      (λ x →
         ◯-map (f ∘ g) (η x)      ≡⟨ ◯-map-η ⟩
         η (f (g x))              ≡⟨ sym ◯-map-η ⟩
         ◯-map f (η (g x))        ≡⟨ cong (◯-map f) $ sym ◯-map-η ⟩∎
         ◯-map f (◯-map g (η x))  ∎)
      _

  -- ◯-map (const x) is pointwise equal to const (η x).

  ◯-map-const : ◯-map (const x) y ≡ const (η x) y
  ◯-map-const {x = x} {y = y} =
    ◯-elim
      {P = λ y → ◯-map (const x) y ≡ η x}
      (λ _ → Separated-◯ _ _)
      (λ y →
         ◯-map (const x) (η y)  ≡⟨ ◯-map-η ⟩
         η x                    ∎)
      y

  -- ◯-map respects pointwise equality.

  ◯-map-cong : (∀ x → f x ≡ g x) → ◯-map f x ≡ ◯-map g x
  ◯-map-cong {f = f} {g = g} {x = x} p =
    ∘η≡∘η→≡
      {f = ◯-map f}
      {g = ◯-map g}
      (λ _ → Modal-◯)
      (λ x →
         ◯-map f (η x)  ≡⟨ ◯-map-η ⟩
         η (f x)        ≡⟨ cong η (p x) ⟩
         η (g x)        ≡⟨ sym ◯-map-η ⟩∎
         ◯-map g (η x)  ∎)
      x

  -- I did not take the remaining lemmas in this section from
  -- "Modalities in Homotopy Type Theory" or the corresponding Coq
  -- code.

  -- A fusion lemma for ◯-elim and ◯-map.

  ◯-elim-◯-map :
    {g : A → B} →
    ◯-elim {P = P} m f (◯-map g x) ≡
    ◯-elim
      {P = P ∘ ◯-map g}
      (m ∘ ◯-map g)
      (subst P (sym ◯-map-η) ∘ f ∘ g)
      x
  ◯-elim-◯-map {P = P} {m = m} {f = f} {x = x} {g = g} =
    ◯-elim
      {P = λ x →
             ◯-elim {P = P} m f (◯-map g x) ≡
             ◯-elim
               {P = P ∘ ◯-map g}
               (m ∘ ◯-map g)
               (subst P (sym ◯-map-η) ∘ f ∘ g)
               x}
      (λ x → Modal→Separated (m (◯-map g x)) _ _)
      (λ x →
         ◯-elim m f (◯-map g (η x))                                  ≡⟨ elim¹
                                                                          (λ {y} eq → ◯-elim m f y ≡ subst P eq (f (g x)))
                                                                          (
           ◯-elim m f (η (g x))                                            ≡⟨ ◯-elim-η ⟩
           f (g x)                                                         ≡⟨ sym $ subst-refl _ _ ⟩∎
           subst P (refl (η (g x))) (f (g x))                              ∎)
                                                                          _ ⟩
         subst P (sym ◯-map-η) (f (g x))                             ≡⟨ sym ◯-elim-η ⟩∎
         ◯-elim (m ∘ ◯-map g) (subst P (sym ◯-map-η) ∘ f ∘ g) (η x)  ∎)
      x

  -- A fusion lemma for ◯-rec and ◯-map.

  ◯-rec-◯-map : ◯-rec m f (◯-map g x) ≡ ◯-rec m (f ∘ g) x
  ◯-rec-◯-map {m = m} {f = f} {g = g} {x = x} =
    ◯-elim
      {P = λ x → ◯-rec m f (◯-map g x) ≡ ◯-rec m (f ∘ g) x}
      (λ _ → Modal→Separated m _ _)
      (λ x →
         ◯-rec m f (◯-map g (η x))  ≡⟨ cong (◯-rec m f) ◯-map-η ⟩
         ◯-rec m f (η (g x))        ≡⟨ ◯-rec-η ⟩
         f (g x)                    ≡⟨ sym ◯-rec-η ⟩∎
         ◯-rec m (f ∘ g) (η x)      ∎)
      x

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

  -- I did not take the results in this section from "Modalities in
  -- Homotopy Type Theory" or the corresponding Coq code (but perhaps
  -- something resembling at least some of these results can be found
  -- there).

  -- ◯ preserves logical equivalences.

  ◯-cong-⇔ : A ⇔ B → ◯ A ⇔ ◯ B
  ◯-cong-⇔ A⇔B = record
    { to   = ◯-map (_⇔_.to   A⇔B)
    ; from = ◯-map (_⇔_.from A⇔B)
    }

  -- ◯ preserves split surjections.

  ◯-cong-↠ : A ↠ B → ◯ A ↠ ◯ B
  ◯-cong-↠ A↠B = record
    { logical-equivalence = ◯-cong-⇔ (_↠_.logical-equivalence A↠B)
    ; right-inverse-of    = ◯-elim
        (λ _ → Separated-◯ _ _)
        (λ y →
           ◯-map (_↠_.to A↠B) (◯-map (_↠_.from A↠B) (η y))  ≡⟨ cong (◯-map (_↠_.to A↠B)) ◯-map-η ⟩
           ◯-map (_↠_.to A↠B) (η (_↠_.from A↠B y))          ≡⟨ ◯-map-η ⟩
           η (_↠_.to A↠B (_↠_.from A↠B y))                  ≡⟨ cong η $ _↠_.right-inverse-of A↠B _ ⟩∎
           η y                                              ∎)
    }

  -- ◯ preserves bijections.

  ◯-cong-↔ : A ↔ B → ◯ A ↔ ◯ B
  ◯-cong-↔ A↔B = record
    { surjection      = ◯-cong-↠ (_↔_.surjection A↔B)
    ; left-inverse-of = ◯-elim
        (λ _ → Separated-◯ _ _)
        (λ x →
           ◯-map (_↔_.from A↔B) (◯-map (_↔_.to A↔B) (η x))  ≡⟨ cong (◯-map (_↔_.from A↔B)) ◯-map-η ⟩
           ◯-map (_↔_.from A↔B) (η (_↔_.to A↔B x))          ≡⟨ ◯-map-η ⟩
           η (_↔_.from A↔B (_↔_.to A↔B x))                  ≡⟨ cong η $ _↔_.left-inverse-of A↔B _ ⟩∎
           η x                                              ∎)
    }

  -- ◯ preserves equivalences.

  ◯-cong-≃ : A ≃ B → ◯ A ≃ ◯ B
  ◯-cong-≃ = from-isomorphism ∘ ◯-cong-↔ ∘ from-isomorphism

  -- ◯ preserves equivalences with erased proofs.

  ◯-cong-≃ᴱ : A ≃ᴱ B → ◯ A ≃ᴱ ◯ B
  ◯-cong-≃ᴱ A≃ᴱB =
    EEq.[≃]→≃ᴱ (EEq.[proofs] (◯-cong-≃ (EEq.≃ᴱ→≃ A≃ᴱB)))

  mutual

    -- If A ↝[ c ∣ d ] B holds, then ◯ A ↝[ k ] ◯ B holds for all k for
    -- which Extensionality? k c d holds.

    ◯-cong-↝ :
      Extensionality? k c d →
      A ↝[ c ∣ d ] B →
      ◯ A ↝[ k ] ◯ B
    ◯-cong-↝ {k = implication} _   hyp = ◯-map (hyp _)
    ◯-cong-↝                   ext hyp = ◯-cong-↝-sym ext hyp

    -- A variant of ◯-cong-↝.

    ◯-cong-↝-sym :
      Extensionality? k c d →
      (∀ {k} → Extensionality? ⌊ k ⌋-sym c d → A ↝[ ⌊ k ⌋-sym ] B) →
      ◯ A ↝[ k ] ◯ B
    ◯-cong-↝-sym ext hyp = generalise-ext?′
      (◯-cong-⇔ (hyp _))
      (λ ext → _≃_.bijection $ ◯-cong-≃ (hyp ext))
      (λ ext → ◯-cong-≃ᴱ (hyp E.[ ext ]))
      ext

  mutual

    -- A variant of ◯-cong-↝-sym.

    ◯-cong-↝ᴱ :
      @ Extensionality? k c d →
      A ↝[ c ∣ d ]ᴱ B →
      ◯ A ↝[ k ] ◯ B
    ◯-cong-↝ᴱ {k = implication} _   hyp = ◯-map (hyp _)
    ◯-cong-↝ᴱ                   ext hyp = ◯-cong-↝-symᴱ ext hyp

    -- A variant of ◯-cong-↝-sym.

    ◯-cong-↝-symᴱ :
      @ Extensionality? k c d →
      (∀ {k} → @ Extensionality? ⌊ k ⌋-sym c d → A ↝[ ⌊ k ⌋-sym ] B) →
      ◯ A ↝[ k ] ◯ B
    ◯-cong-↝-symᴱ ext hyp = generalise-erased-ext?
      (◯-cong-⇔ (hyp _))
      (λ ext → _≃_.bijection $ ◯-cong-≃ (hyp ext))
      ext

  ----------------------------------------------------------------------
  -- Some equivalences and related results

  -- If A and B are equivalent, then Modal A and Modal B are
  -- equivalent (assuming function extensionality).

  Modal-cong :
    Extensionality? k a a →
    A ≃ B → Modal A ↝[ k ] Modal B
  Modal-cong {A = A} {B = B} ext A≃B =
    generalise-ext?-prop
      (record
         { to   = Modal-respects-≃ A≃B
         ; from = Modal-respects-≃ (inverse A≃B)
         })
      Modal-propositional
      Modal-propositional
      ext

  -- The type (x : ◯ A) → ◯ (P x) is inhabited if and only if
  -- (x : A) → ◯ (P (η x)) is.

  Π◯◯≃Π◯η :
    ((x : ◯ A) → ◯ (P x)) ↝[ a ∣ a ] ((x : A) → ◯ (P (η x)))
  Π◯◯≃Π◯η =
    generalise-ext?
      (record { to = _∘ η; from = ◯-elim (λ _ → Modal-◯) })
      (λ ext →
           (λ f → apply-ext ext λ x →
              ◯-elim (λ _ → Modal-◯) f (η x)  ≡⟨ ◯-elim-η ⟩∎
              f x                             ∎)
         , (λ f → apply-ext ext (◯-elim (λ _ → Separated-◯ _ _) λ x →
              ◯-elim (λ _ → Modal-◯) (f ∘ η) (η x)  ≡⟨ ◯-elim-η ⟩∎
              f (η x)                               ∎)))

  -- ◯ (↑ a ⊤) is equivalent to ⊤.

  ◯-⊤ : ◯ (↑ a ⊤) ≃ ⊤
  ◯-⊤ =
    ◯ (↑ a ⊤)  ↝⟨ inverse Eq.⟨ _ , Modal≃Is-equivalence-η _ Modal-⊤ ⟩ ⟩
    ↑ a ⊤      ↔⟨ Bijection.↑↔ ⟩□
    ⊤          □

  private module Abstract where abstract

    -- ◯ commutes with _×_.

    ◯× : ◯ (A × B) ≃ (◯ A × ◯ B)
    ◯× {A = A} {B = B} = Eq.↔→≃
      (◯-rec m′ (Σ-map η η))
      (uncurry λ x → ◯-rec Modal-◯ λ y → ◯-map (_, y) x)
      (λ (x , y) →
         ◯-rec m′ (Σ-map η η) (◯-rec Modal-◯ (λ y → ◯-map (_, y) x) y)  ≡⟨ ◯-elim
                                                                             {P = λ y →
                                                                                    ◯-rec m′ (Σ-map η η)
                                                                                      (◯-rec Modal-◯ (λ y → ◯-map (_, y) x) y) ≡
                                                                                    (x , y)}
                                                                             (λ _ → Modal→Separated m′ _ _)
                                                                             (λ y →
           ◯-rec m′ (Σ-map η η)
             (◯-rec Modal-◯ (λ y → ◯-map (_, y) x) (η y))                       ≡⟨ cong (◯-rec _ _)
                                                                                   ◯-rec-η ⟩

           ◯-rec m′ (Σ-map η η) (◯-map (_, y) x)                                ≡⟨ ◯-elim
                                                                                     (λ _ → Modal→Separated m′ _ _)
                                                                                     (λ x →
             ◯-rec m′ (Σ-map η η) (◯-map (_, y) (η x))                                  ≡⟨ cong (◯-rec _ _)
                                                                                           ◯-map-η ⟩

             ◯-rec m′ (Σ-map η η) (η (x , y))                                           ≡⟨ ◯-rec-η ⟩∎

             (η x , η y)                                                                ∎)
                                                                                     x ⟩∎
           (x , η y)                                                            ∎)
                                                                             _ ⟩∎
         (x , y)                                                        ∎)
      (◯-elim
         (λ _ → Separated-◯ _ _)
         (λ (x , y) →
            uncurry (λ x → ◯-rec Modal-◯ λ y → ◯-map (_, y) x)
              (◯-rec m′ (Σ-map η η) (η (x , y)))                ≡⟨ cong (uncurry λ x → ◯-rec Modal-◯ λ y → ◯-map (_, y) x)
                                                                   ◯-rec-η ⟩
            uncurry (λ x → ◯-rec Modal-◯ λ y → ◯-map (_, y) x)
              (η x , η y)                                       ≡⟨⟩

            ◯-rec Modal-◯ (λ y → ◯-map (_, y) (η x)) (η y)      ≡⟨ ◯-rec-η ⟩


            ◯-map (_, y) (η x)                                  ≡⟨ ◯-map-η ⟩∎

            η (x , y)                                           ∎))
      where
      m′ : Modal (◯ A × ◯ B)
      m′ = Modal-Σ Modal-◯ λ _ → Modal-◯

    -- Four "computation rules" for ◯×.

    ◯×-η : _≃_.to ◯× (η (x , y)) ≡ (η x , η y)
    ◯×-η = ◯-rec-η

    ◯×⁻¹-ηʳ : {y : B} → _≃_.from ◯× (x , η y) ≡ ◯-map (_, y) x
    ◯×⁻¹-ηʳ {x = x} {y = y} =
      ◯-rec Modal-◯ (λ y → ◯-map (_, y) x) (η y)  ≡⟨ ◯-rec-η ⟩∎
      ◯-map (_, y) x                              ∎

    ◯×⁻¹-η : {y : B} → _≃_.from ◯× (η x , η y) ≡ η (x , y)
    ◯×⁻¹-η {x = x} {y = y} =
      _≃_.from ◯× (η x , η y)  ≡⟨ ◯×⁻¹-ηʳ ⟩
      ◯-map (_, y) (η x)       ≡⟨ ◯-map-η ⟩∎
      η (x , y)                ∎

    ◯×⁻¹-ηˡ : {y : ◯ B} → _≃_.from ◯× (η x , y) ≡ ◯-map (x ,_) y
    ◯×⁻¹-ηˡ {x = x} {y = y} =
      ◯-elim
        {P = λ y → _≃_.from ◯× (η x , y) ≡ ◯-map (x ,_) y}
        (λ _ → Separated-◯ _ _)
        (λ y →
           _≃_.from ◯× (η x , η y)  ≡⟨ ◯×⁻¹-η ⟩
           η (x , y)                ≡⟨ sym ◯-map-η ⟩∎
           ◯-map (x ,_) (η y)       ∎)
        y

  open Abstract public

  -- I did not take the remaining results and definitions in this
  -- section from "Modalities in Homotopy Type Theory" or the
  -- corresponding Coq code (but that does not mean that one cannot
  -- find something similar in those places).

  -- ◯ commutes with Vec n (in a certain sense).

  ◯-Vec : ◯ (Vec n P) ≃ Vec n (◯ ∘ P)
  ◯-Vec {n = zero} =
    ◯ (↑ a ⊤)  ↝⟨ ◯-⊤ ⟩
    ⊤          ↔⟨ inverse Bijection.↑↔ ⟩□
    ↑ a ⊤      □
  ◯-Vec {n = suc n} {P = P} =
    ◯ (P fzero × Vec n (P ∘ fsuc))      ↝⟨ ◯× ⟩
    ◯ (P fzero) × ◯ (Vec n (P ∘ fsuc))  ↝⟨ (∃-cong λ _ → ◯-Vec) ⟩□
    ◯ (P fzero) × Vec n (◯ ∘ P ∘ fsuc)  □

  -- A "computation rule" for ◯-Vec.

  ◯-Vec-η :
    {xs : Vec n P} →
    _≃_.to ◯-Vec (η xs) ≡ Vec.map η xs
  ◯-Vec-η {n = zero}                = refl _
  ◯-Vec-η {n = suc _} {xs = x , xs} =
    Σ-map id (_≃_.to ◯-Vec) (_≃_.to ◯× (η (x , xs)))  ≡⟨ cong (Σ-map id (_≃_.to ◯-Vec)) ◯×-η ⟩
    Σ-map id (_≃_.to ◯-Vec) (η x , η xs)              ≡⟨ cong (_ ,_) ◯-Vec-η ⟩∎
    η x , Vec.map η xs                                ∎

  -- A lemma relating Vec.index and ◯-Vec.

  index-◯-Vec :
    {xs : Vec n (◯ ∘ P)} →
    ◯-map (λ xs → Vec.index xs i) (_≃_.from ◯-Vec xs) ≡
    Vec.index xs i
  index-◯-Vec {n = suc _} {i = fzero} {xs = x , xs} =
    ◯-elim
      {P = λ x → ◯-map proj₁ (_≃_.from ◯× (x , _≃_.from ◯-Vec xs)) ≡ x}
      (λ _ → Separated-◯ _ _)
      (λ x →
         ◯-map proj₁ (_≃_.from ◯× (η x , _≃_.from ◯-Vec xs))  ≡⟨ cong (◯-map _) ◯×⁻¹-ηˡ ⟩
         ◯-map proj₁ (◯-map (x ,_) (_≃_.from ◯-Vec xs))       ≡⟨ sym ◯-map-∘ ⟩
         ◯-map (const x) (_≃_.from ◯-Vec xs)                  ≡⟨ ◯-map-const ⟩∎
         η x                                                  ∎)
      x
  index-◯-Vec {n = suc _} {i = fsuc i} {xs = x , xs} =
    ◯-map (λ (_ , xs) → Vec.index xs i)
      (_≃_.from ◯× (x , _≃_.from ◯-Vec xs))                ≡⟨ ◯-map-∘ ⟩

    ◯-map (λ xs → Vec.index xs i)
      (◯-map proj₂ (_≃_.from ◯× (x , _≃_.from ◯-Vec xs)))  ≡⟨ cong (◯-map _) $
                                                              ◯-elim
                                                                {P = λ xs → ◯-map proj₂ (_≃_.from ◯× (x , xs)) ≡ xs}
                                                                (λ _ → Separated-◯ _ _)
                                                                (λ xs →
      ◯-map proj₂ (_≃_.from ◯× (x , η xs))                         ≡⟨ cong (◯-map _) ◯×⁻¹-ηʳ ⟩
      ◯-map proj₂ (◯-map (_, xs) x)                                ≡⟨ sym ◯-map-∘ ⟩
      ◯-map (const xs) x                                           ≡⟨ ◯-map-const ⟩∎
      η xs                                                         ∎)
                                                                _ ⟩

    ◯-map (λ xs → Vec.index xs i) (_≃_.from ◯-Vec xs)      ≡⟨ index-◯-Vec ⟩∎

    Vec.index xs i                                         ∎

  -- A lemma relating ◯-Vec and Vec.tabulate.

  ◯-Vec-tabulate-η :
    {f : (i : Fin n) → P i} →
    _≃_.from ◯-Vec (Vec.tabulate (η ∘ f)) ≡
    η (Vec.tabulate f)
  ◯-Vec-tabulate-η {n = zero}          = refl _
  ◯-Vec-tabulate-η {n = suc n} {f = f} =
    _≃_.from ◯×
      (η (f fzero) , _≃_.from ◯-Vec (Vec.tabulate (η ∘ f ∘ fsuc)))  ≡⟨ cong (_≃_.from ◯× ∘ (_ ,_)) ◯-Vec-tabulate-η ⟩

    _≃_.from ◯× (η (f fzero) , η (Vec.tabulate (f ∘ fsuc)))         ≡⟨ ◯×⁻¹-η ⟩∎

    η (f fzero , Vec.tabulate (f ∘ fsuc))                           ∎

  -- If A is modal, then ◯ (Σ A P) is equivalent to Σ A (◯ ∘ P).

  Modal→◯Σ≃Σ◯ :
    Modal A →
    ◯ (Σ A P) ≃ Σ A (◯ ∘ P)
  Modal→◯Σ≃Σ◯ {A = A} {P = P} m = Eq.↔→≃
    (◯-rec m′ (Σ-map id η))
    (λ (x , y) → ◯-map (x ,_) y)
    (uncurry λ x →
       ◯-elim (λ _ → Modal→Separated m′ _ _) λ y →
         ◯-rec m′ (Σ-map id η) (◯-map (x ,_) (η y))  ≡⟨ cong (◯-rec m′ (Σ-map id η)) ◯-map-η ⟩
         ◯-rec m′ (Σ-map id η) (η (x , y))           ≡⟨ ◯-rec-η ⟩∎
         (x , η y)                                   ∎)
    (◯-elim
       (λ _ → Separated-◯ _ _)
       (λ (x , y) →
          (let x′ , y′ = ◯-rec m′ (Σ-map id η) (η (x , y)) in
           ◯-map (x′ ,_) y′)                                   ≡⟨ cong (λ (p : Σ A (◯ ∘ P)) → let x′ , y′ = p in ◯-map (x′ ,_) y′)
                                                                  ◯-rec-η ⟩

          ◯-map (x ,_) (η y)                                   ≡⟨ ◯-map-η ⟩∎

          η (x , y)                                            ∎))
    where
    m′ = Modal-Σ m λ _ → Modal-◯

  ----------------------------------------------------------------------
  -- Choice

  -- I did not take the definitions in this section from "Modalities
  -- in Homotopy Type Theory" or the corresponding Coq code (but that
  -- does not mean that one cannot find something similar in those
  -- places).

  -- The inverse of a choice principle (that may or may not hold).

  ◯Π→Π◯ :
    {A : Type a} {P : A → Type a} →
    ◯ ((x : A) → P x) → ((x : A) → ◯ (P x))
  ◯Π→Π◯ = flip (◯-map ∘ flip _$_)

  -- A "computation rule" for ◯Π→Π◯.

  ◯Π→Π◯-η :
    Extensionality a a →
    ◯Π→Π◯ (η f) ≡ η ∘ f
  ◯Π→Π◯-η ext = apply-ext ext λ _ → ◯-map-η

  -- ◯Π→Π◯ commutes with ◯-map in a certain way.

  ◯Π→Π◯-◯-map :
    {f : ∀ {x} → P x → Q x} {g : ◯ ((x : A) → P x)} →
    ◯Π→Π◯ (◯-map (f ∘_) g) x ≡ ◯-map f (◯Π→Π◯ g x)
  ◯Π→Π◯-◯-map {x = x} {f = f} {g = g} =
    ◯-elim
      {P = λ g → ◯Π→Π◯ (◯-map (f ∘_) g) x ≡ ◯-map f (◯Π→Π◯ g x)}
      (λ _ → Separated-◯ _ _)
      (λ g →
         ◯Π→Π◯ (◯-map (f ∘_) (η g)) x  ≡⟨ cong (flip ◯Π→Π◯ _) ◯-map-η ⟩
         ◯Π→Π◯ (η (f ∘ g)) x           ≡⟨ ◯-map-η ⟩
         η (f (g x))                   ≡⟨ sym ◯-map-η ⟩
         ◯-map f (η (g x))             ≡⟨ cong (◯-map _) $ sym ◯-map-η ⟩∎
         ◯-map f (◯Π→Π◯ (η g) x)       ∎)
      g

  -- A definition of what it means for the modality to "have choice
  -- for A".
  --
  -- The definition is a little convoluted. In the presence of
  -- function extensionality it can be simplified, see
  -- Has-choice-for≃Is-equivalence-◯Π→Π◯. With the present formulation
  -- one can prove certain things without assuming function
  -- extensionality:
  -- * One can prove that modalities with choice satisfy certain
  --   properties (see Modality.Has-choice).
  -- * One can prove that very modal modalities have choice (see
  --   Modality.Very-modal.has-choice).

  Has-choice-for : Type a → Type (lsuc a)
  Has-choice-for A =
    {P : A → Type a} →
    ∃ λ (Π◯→◯Π : (∀ x → ◯ (P x)) → ◯ (∀ x → P x)) →
    ∃ λ (◯Π→Π◯-Π◯→◯Π : ∀ f x → ◯Π→Π◯ (Π◯→◯Π f) x ≡ f x) →
    Extensionality a a →
    ∃ λ (equiv : Is-equivalence (◯Π→Π◯ {P = P})) →
    let eq = Eq.⟨ _ , equiv ⟩ in
    ∃ λ (Π◯→◯Π≡ : Π◯→◯Π ≡ _≃_.from eq) →
    ∀ f x →
    ◯Π→Π◯-Π◯→◯Π f x ≡
    (◯Π→Π◯ (Π◯→◯Π f) x            ≡⟨ cong (λ g → ◯Π→Π◯ (g f) x) Π◯→◯Π≡ ⟩
     _≃_.to eq (_≃_.from eq f) x  ≡⟨ ext⁻¹ (_≃_.right-inverse-of eq f) x ⟩∎
     f x                          ∎)

  -- In the presence of function extensionality Has-choice-for A is
  -- equivalent to {P : A → Type a} → Is-equivalence (◯Π→Π◯ {P = P}).

  Has-choice-for≃Is-equivalence-◯Π→Π◯ :
    Extensionality (lsuc a) (lsuc a) →
    Has-choice-for A ≃
    ({P : A → Type a} → Is-equivalence (◯Π→Π◯ {P = P}))
  Has-choice-for≃Is-equivalence-◯Π→Π◯ ext =
    implicit-∀-cong ext λ {P} →

    (∃ λ (Π◯→◯Π : (∀ x → ◯ (P x)) → ◯ (∀ x → P x)) →
     ∃ λ (◯Π→Π◯-Π◯→◯Π : ∀ f x → ◯Π→Π◯ (Π◯→◯Π f) x ≡ f x) →
     Extensionality a a →
     ∃ λ (equiv : Is-equivalence (◯Π→Π◯ {P = P})) →
     let eq = Eq.⟨ _ , equiv ⟩ in
     ∃ λ (Π◯→◯Π≡ : Π◯→◯Π ≡ _≃_.from eq) →
     ∀ f x →
     ◯Π→Π◯-Π◯→◯Π f x ≡
     trans (cong (λ g → ◯Π→Π◯ (g f) x) Π◯→◯Π≡)
       (ext⁻¹ (_≃_.right-inverse-of eq f) x))                     ↝⟨ (∃-cong λ _ → ∃-cong λ _ →
                                                                      drop-⊤-left-Π (lower-extensionality lzero _ ext) $
                                                                      _⇔_.to contractible⇔↔⊤ $
                                                                      propositional⇒inhabited⇒contractible
                                                                        (Extensionality-propositional ext)
                                                                        ext′) ⟩
    (∃ λ (Π◯→◯Π : (∀ x → ◯ (P x)) → ◯ (∀ x → P x)) →
     ∃ λ (◯Π→Π◯-Π◯→◯Π : ∀ f x → ◯Π→Π◯ (Π◯→◯Π f) x ≡ f x) →
     ∃ λ (equiv : Is-equivalence (◯Π→Π◯ {P = P})) →
     let eq = Eq.⟨ _ , equiv ⟩ in
     ∃ λ (Π◯→◯Π≡ : Π◯→◯Π ≡ _≃_.from eq) →
     ∀ f x →
     ◯Π→Π◯-Π◯→◯Π f x ≡
     trans (cong (λ g → ◯Π→Π◯ (g f) x) Π◯→◯Π≡)
       (ext⁻¹ (_≃_.right-inverse-of eq f) x))                     ↔⟨ Σ-assoc F.∘
                                                                     (∃-cong λ _ → Σ-assoc) F.∘
                                                                     ∃-comm F.∘
                                                                     (∃-cong λ _ →
                                                                      inverse Σ-assoc F.∘
                                                                      ∃-comm F.∘
                                                                      (∃-cong λ _ → Σ-assoc)) ⟩
    (∃ λ ((equiv , Π◯→◯Π , Π◯→◯Π≡) :
          ∃ λ (equiv : Is-equivalence (◯Π→Π◯ {P = P})) →
          ∃ λ (Π◯→◯Π : (∀ x → ◯ (P x)) → ◯ (∀ x → P x)) →
          Π◯→◯Π ≡ _≃_.from Eq.⟨ _ , equiv ⟩) →
     ∃ λ (◯Π→Π◯-Π◯→◯Π : ∀ f x → ◯Π→Π◯ (Π◯→◯Π f) x ≡ f x) →
     ∀ f x →
     ◯Π→Π◯-Π◯→◯Π f x ≡
     trans (cong (λ g → ◯Π→Π◯ (g f) x) Π◯→◯Π≡)
       (ext⁻¹ (_≃_.right-inverse-of Eq.⟨ _ , equiv ⟩ f) x))       ↝⟨ (Σ-cong-contra
                                                                        (inverse $
                                                                         drop-⊤-right λ _ →
                                                                         _⇔_.to contractible⇔↔⊤ $
                                                                         singleton-contractible _) λ _ →
                                                                      F.id) ⟩
    (∃ λ (equiv : Is-equivalence (◯Π→Π◯ {P = P})) →
     let eq = Eq.⟨ _ , equiv ⟩ in
     ∃ λ (◯Π→Π◯-Π◯→◯Π : ∀ f x → ◯Π→Π◯ (_≃_.from eq f) x ≡ f x) →
     ∀ f x →
     ◯Π→Π◯-Π◯→◯Π f x ≡
     trans (cong (λ g → ◯Π→Π◯ (g f) x) (refl (_≃_.from eq)))
       (ext⁻¹ (_≃_.right-inverse-of eq f) x))                     ↝⟨ (∃-cong λ _ → ∃-cong λ _ →
                                                                      ∀-cong ext′ λ _ → ∀-cong ext′ λ _ →
                                                                      ≡⇒↝ _ $ cong (_ ≡_) $
                                                                      trans (cong (flip trans _) $
                                                                             cong-refl _) $
                                                                      trans-reflˡ _) ⟩
    (∃ λ (equiv : Is-equivalence (◯Π→Π◯ {P = P})) →
     let eq = Eq.⟨ _ , equiv ⟩ in
     ∃ λ (◯Π→Π◯-Π◯→◯Π : ∀ f x → ◯Π→Π◯ (_≃_.from eq f) x ≡ f x) →
     ∀ f x →
     ◯Π→Π◯-Π◯→◯Π f x ≡ ext⁻¹ (_≃_.right-inverse-of eq f) x)       ↝⟨ (∃-cong λ _ → ∃-cong λ _ →
                                                                      Eq.extensionality-isomorphism ext′ F.∘
                                                                      (∀-cong ext′ λ _ → Eq.extensionality-isomorphism ext′)) ⟩
    (∃ λ (equiv : Is-equivalence (◯Π→Π◯ {P = P})) →
     let eq = Eq.⟨ _ , equiv ⟩ in
     ∃ λ (◯Π→Π◯-Π◯→◯Π : ∀ f x → ◯Π→Π◯ (_≃_.from eq f) x ≡ f x) →
     ◯Π→Π◯-Π◯→◯Π ≡ ext⁻¹ ∘ _≃_.right-inverse-of eq)               ↔⟨ (drop-⊤-right λ _ →
                                                                      _⇔_.to contractible⇔↔⊤ $
                                                                      singleton-contractible _) ⟩□
    Is-equivalence (◯Π→Π◯ {P = P})                                □
    where
    ext′ : Extensionality a a
    ext′ = lower-extensionality _ _ ext

  -- A definition of what it means for the modality to "have choice",
  -- or to be a "modality with choice".

  Has-choice : Type (lsuc a)
  Has-choice = {A : Type a} → Has-choice-for A

  -- Has-choice-for P is a proposition (assuming function
  -- extensionality).

  Has-choice-for-propositional :
    Extensionality (lsuc a) (lsuc a) →
    Is-proposition (Has-choice-for A)
  Has-choice-for-propositional {A = A} ext =
                                                              $⟨ (implicit-Π-closure (lower-extensionality lzero _ ext)  λ _ →
                                                                  Is-equivalence-propositional (lower-extensionality _ _ ext)) ⟩
    Is-proposition ({P : A → Type a} → Is-equivalence ◯Π→Π◯)  →⟨ H-level-cong _  (inverse $ Has-choice-for≃Is-equivalence-◯Π→Π◯ ext) ⟩□
    Is-proposition (Has-choice-for A)                         □

  -- Has-choice is a proposition (assuming function extensionality).

  Has-choice-propositional :
    Extensionality (lsuc a) (lsuc a) →
    Is-proposition Has-choice
  Has-choice-propositional ext =
    implicit-Π-closure ext  λ _ →
    Has-choice-for-propositional ext

  -- Has-choice-for preserves equivalences (assuming function
  -- extensionality).

  Has-choice-for-cong-≃ :
    Extensionality (lsuc a) (lsuc a) →
    A ≃ B → Has-choice-for A ≃ Has-choice-for B
  Has-choice-for-cong-≃ {A = A} {B = B} ext A≃B =
    Has-choice-for A                                       ↝⟨ Has-choice-for≃Is-equivalence-◯Π→Π◯ ext ⟩

    ({P : A → Type a} → Is-equivalence (◯Π→Π◯ {P = P}))    ↝⟨ (implicit-Π-cong ext⁺₀ (Π-cong-contra ext₀⁺ (inverse A≃B) (λ _ → Eq.id)) λ P →

      Is-equivalence
        (◯Π→Π◯ ⦂ (◯ ((x : A) → P x) → (x : A) → ◯ (P x)))        ↝⟨ Is-equivalence≃Is-equivalence-∘ˡ
                                                                      (_≃_.is-equivalence $
                                                                       Π-cong-contra ext₀₀ (inverse A≃B) (λ _ → F.id))
                                                                      ext₀₀ F.∘
                                                                    Is-equivalence≃Is-equivalence-∘ʳ
                                                                      (_≃_.is-equivalence $
                                                                       ◯-cong-≃ $ Π-cong ext₀₀ (inverse A≃B) (λ _ → F.id))
                                                                      ext₀₀ ⟩
      Is-equivalence
        (Π-cong-contra-→ (_≃_.from A≃B) (λ _ → id) ∘
         ◯Π→Π◯ {P = P} ∘
         ◯-map (Π-cong _ (inverse A≃B) (λ _ → id)) ⦂
         (◯ ((x : B) → P (_≃_.from A≃B x)) →
          (x : B) → ◯ (P (_≃_.from A≃B x))))                     ↝⟨ Is-equivalence-cong ext₀₀ $
                                                                    ◯-elim
                                                                      (λ _ → Modal→Separated (Modal-Π ext₀₀ λ _ → Modal-◯) _ _)
                                                                      (lemma P) ⟩□
      Is-equivalence
        (◯Π→Π◯ ⦂
         (◯ ((x : B) → P (_≃_.from A≃B x)) →
          (x : B) → ◯ (P (_≃_.from A≃B x))))                     □) ⟩

    ({P : B → Type a} → Is-equivalence (◯Π→Π◯ {P = P}))    ↝⟨ inverse $ Has-choice-for≃Is-equivalence-◯Π→Π◯ ext ⟩□

    Has-choice-for B                                       □
    where
    ext⁺₀ = lower-extensionality lzero _ ext
    ext₀⁺ = lower-extensionality _ lzero ext
    ext₀₀ = lower-extensionality _ _ ext

    lemma = λ P f → apply-ext ext₀₀ λ x →
      ◯-map (_$ _≃_.from A≃B x) $
      ◯-map
        (λ f x →
           subst P (_≃_.left-inverse-of A≃B x)
             (f (_≃_.to A≃B x))) $
      η f                                                ≡⟨ sym ◯-map-∘ ⟩

      ◯-map
        (λ f →
           subst P
             (_≃_.left-inverse-of A≃B (_≃_.from A≃B x))
             (f (_≃_.to A≃B (_≃_.from A≃B x)))) $
      η f                                                ≡⟨ (cong (flip ◯-map _) $ apply-ext ext₀₀ λ f →

        subst P
          (_≃_.left-inverse-of A≃B (_≃_.from A≃B x))
          (f (_≃_.to A≃B (_≃_.from A≃B x)))                    ≡⟨ cong (flip (subst P) _) $ sym $
                                                                  _≃_.right-left-lemma A≃B _ ⟩
        subst P
          (cong (_≃_.from A≃B) $
           _≃_.right-inverse-of A≃B x)
          (f (_≃_.to A≃B (_≃_.from A≃B x)))                    ≡⟨ elim₁
                                                                    (λ {y} eq →
                                                                       subst P (cong (_≃_.from A≃B) eq) (f y) ≡ f x)
                                                                    (trans (cong (flip (subst P) _) $ cong-refl _) $
                                                                     subst-refl _ _)
                                                                    _ ⟩∎

        f x                                                    ∎) ⟩∎

      ◯-map (_$ x) (η f)                                 ∎

  -- The modality has choice for Fin n (lifted).

  Has-choice-for-Fin : Has-choice-for (↑ a (Fin n))
  Has-choice-for-Fin =
      Π◯→◯Π
    , ◯Π→Π◯-Π◯→◯Π
    , (λ ext →
           _≃_.is-equivalence
             (Eq.↔→≃ _ _
                (apply-ext ext ∘ ◯Π→Π◯-Π◯→◯Π)
                (λ _ → Π◯→◯Π-◯Π→Π◯ (lower-extensionality _ lzero ext)))
         , refl _
         , (λ f i →
              ◯Π→Π◯-Π◯→◯Π f i                                  ≡⟨ cong (_$ i) $ sym $ ext⁻¹-ext ext ⟩

              ext⁻¹ (apply-ext ext $ ◯Π→Π◯-Π◯→◯Π f) i          ≡⟨ trans (sym $ trans-reflˡ _) $
                                                                  cong (flip trans _) $ sym $ cong-refl _ ⟩∎
              trans (cong (λ g → ◯Π→Π◯ (g f) i) (refl Π◯→◯Π))
                (ext⁻¹ (apply-ext ext $ ◯Π→Π◯-Π◯→◯Π f) i)      ∎))
    where
    Π◯→◯Π : ((x : ↑ a (Fin n)) → ◯ (P x)) → ◯ ((x : ↑ a (Fin n)) → P x)
    Π◯→◯Π {n = n} {P = P} =
      ((x : ↑ a (Fin n)) → ◯ (P x))   →⟨ _∘ lift ⟩
      ((x : Fin n) → ◯ (P (lift x)))  →⟨ Vec.tabulate ⟩
      Vec n (◯ ∘ P ∘ lift)            ↔⟨ inverse ◯-Vec ⟩
      ◯ (Vec n (P ∘ lift))            →⟨ ◯-map Vec.index ⟩
      ◯ ((x : Fin n) → P (lift x))    →⟨ ◯-map (_∘ lower) ⟩□
      ◯ ((x : ↑ a (Fin n)) → P x)     □

    abstract

      ◯Π→Π◯-Π◯→◯Π :
        ∀ (f : (x : ↑ a (Fin n)) → ◯ (P x)) i →
        ◯Π→Π◯ (Π◯→◯Π f) i ≡ f i
      ◯Π→Π◯-Π◯→◯Π {n = n} {P = P} f (lift i) =
        ◯-map (_$ lift i) $
        ◯-map (_∘ lower) $
        ◯-map Vec.index $
        _≃_.from ◯-Vec $
        Vec.tabulate (f ∘ lift)                ≡⟨ sym (trans ◯-map-∘ ◯-map-∘) ⟩

        ◯-map (λ xs → Vec.index xs i) $
        _≃_.from ◯-Vec $
        Vec.tabulate (f ∘ lift)                ≡⟨ index-◯-Vec ⟩

        Vec.index (Vec.tabulate (f ∘ lift)) i  ≡⟨ Vec.index-tabulate n _ ⟩∎

        f (lift i)                             ∎

      Π◯→◯Π-◯Π→Π◯ :
        {f : ◯ ((x : ↑ a (Fin n)) → P x)} →
        Extensionality lzero a →
        Π◯→◯Π (◯Π→Π◯ f) ≡ f
      Π◯→◯Π-◯Π→Π◯ {n = n} {P = P} {f = f} ext =
        ◯-elim
          {P = λ f → Π◯→◯Π (◯Π→Π◯ f) ≡ f}
          (λ _ → Separated-◯ _ _)
          (λ f →
             ◯-map (_∘ lower) $
             ◯-map Vec.index $
             _≃_.from ◯-Vec $
             Vec.tabulate (λ i → ◯-map (_$ lift i) (η f))     ≡⟨ sym ◯-map-∘ ⟩

             ◯-map (λ xs → Vec.index xs ∘ lower) $
             _≃_.from ◯-Vec $
             Vec.tabulate (λ i → ◯-map (_$ lift i) (η f))     ≡⟨ (cong (◯-map _) $ cong (_≃_.from ◯-Vec) $ cong Vec.tabulate $ apply-ext ext λ _ →
                                                                  ◯-map-η) ⟩
             ◯-map (λ xs → Vec.index xs ∘ lower) $
             _≃_.from ◯-Vec $
             Vec.tabulate (η ∘ f ∘ lift)                      ≡⟨ cong (◯-map _)
                                                                 ◯-Vec-tabulate-η ⟩
             ◯-map (λ xs → Vec.index xs ∘ lower) $
             η (Vec.tabulate (f ∘ lift))                      ≡⟨ ◯-map-η ⟩

             η (Vec.index (Vec.tabulate (f ∘ lift)) ∘ lower)  ≡⟨ (cong (η ∘ (_∘ lower)) $
                                                                  apply-ext ext $
                                                                  Vec.index-tabulate n) ⟩∎
             η f                                              ∎)
          f

  ----------------------------------------------------------------------
  -- Some conversions

  -- Modalities are Σ-closed reflective subuniverses.

  Σ-closed : Σ-closed-reflective-subuniverse a
  Σ-closed = λ where
      .M.◯                    → ◯
      .M.η                    → η
      .M.Modal                → Modal
      .M.Modal-propositional  → Modal-propositional
      .M.Modal-◯              → Modal-◯
      .M.Modal-respects-≃     → Modal-respects-≃
      .M.extendable-along-η m → extendable-along-η (λ _ → m)
      .M.Σ-closed             → Modal-Σ
    where
    module M = Σ-closed-reflective-subuniverse

  -- Modalities are uniquely eliminating modalities (assuming function
  -- extensionality).

  uniquely-eliminating :
    Extensionality a a →
    Uniquely-eliminating-modality a
  uniquely-eliminating ext = λ where
      .M.◯                    → ◯
      .M.η                    → η
      .M.uniquely-eliminating → _≃_.is-equivalence (Π◯◯≃Π◯η ext)
    where
    module M = Uniquely-eliminating-modality

  ----------------------------------------------------------------------
  -- Stability

  -- I did not take the definitions or results in this section from
  -- "Modalities in Homotopy Type Theory" or the corresponding Coq
  -- code (but perhaps something resembling at least some of these
  -- results can be found there).

  -- A generalised form of stability.

  Stable-[_] : Kind → Type a → Type a
  Stable-[ k ] A = ◯ A ↝[ k ] A

  -- Modal types are k-stable for all k.

  Modal→Stable : Modal A → Stable-[ k ] A
  Modal→Stable {A = A} {k = k} =
    Modal A         →⟨ Modal→≃◯ ⟩
    (A ≃ ◯ A)       →⟨ inverse ⟩
    (◯ A ≃ A)       →⟨ from-equivalence ⟩□
    Stable-[ k ] A  □

  -- A "computation rule" for Modal→Stable.

  Modal→Stable-η : Modal→Stable m (η x) ≡ x
  Modal→Stable-η = η⁻¹-η

  -- A simplification lemma for Modal→Stable and
  -- Stable→left-inverse→Modal.

  Modal→Stable-Stable→left-inverse→Modal :
    Modal→Stable (Stable→left-inverse→Modal s p) x ≡ s x
  Modal→Stable-Stable→left-inverse→Modal {s = s} {p = p} {x = x} =
    ◯-elim
      {P = λ x → Modal→Stable m′ x ≡ s x}
      (λ x → Modal→Separated m′ _ _)
      (λ x →
         Modal→Stable m′ (η x)  ≡⟨ Modal→Stable-η ⟩
         x                      ≡⟨ sym $ p x ⟩∎
         s (η x)                ∎)
      x
    where
    m′ = Stable→left-inverse→Modal s p

  -- A simplification lemma for Modal→Stable and ◯-map.

  Modal→Stable-◯-map :
    Modal→Stable m₁ (◯-map f x) ≡ f (Modal→Stable m₂ x)
  Modal→Stable-◯-map {m₁ = m₁} {f = f} {x = x} {m₂ = m₂} =
    ◯-elim
      {P = λ x →
             Modal→Stable m₁ (◯-map f x) ≡
             f (Modal→Stable m₂ x)}
      (λ _ → Modal→Separated m₁ _ _)
      (λ x →
         Modal→Stable m₁ (◯-map f (η x))  ≡⟨ cong (Modal→Stable m₁) ◯-map-η ⟩
         Modal→Stable m₁ (η (f x))        ≡⟨ Modal→Stable-η ⟩
         f x                              ≡⟨ cong f $ sym Modal→Stable-η ⟩∎
         f (Modal→Stable m₂ (η x))        ∎)
      x

  -- Stable types are logical-equivalence-stable.

  Stable→Stable-⇔ : Stable A → Stable-[ logical-equivalence ] A
  Stable→Stable-⇔ s = record { to = s; from = η }

  -- Stability is closed under Π-types.

  Stable-Π :
    {A : Type a} {P : A → Type a} →
    (∀ x → Stable (P x)) →
    Stable ((x : A) → P x)
  Stable-Π {A = A} {P = P} hyp =
    ◯ ((x : A) → P x)    →⟨ ◯Π→Π◯ ⟩
    ((x : A) → ◯ (P x))  →⟨ ∀-cong _ hyp ⟩□
    ((x : A) → P x)      □

  -- A lemma relating Stable-Π and Modal-Π.

  Stable-Π-Modal-Π :
    {m : ∀ x → Modal (P x)}
    (ext : Extensionality a a) →
    Stable-Π (λ x → Modal→Stable (m x)) ≡
    Modal→Stable (Modal-Π ext m)
  Stable-Π-Modal-Π {m = m} ext =
    apply-ext ext λ f →
      (λ x → ◯-rec (m x) id (◯-map (_$ x) f))  ≡⟨ (apply-ext ext λ _ → ◯-rec-◯-map) ⟩
      (λ x → ◯-rec (m x) (_$ x) f)             ≡⟨ sym Modal→Stable-Stable→left-inverse→Modal ⟩∎
      Modal→Stable (Modal-Π ext m) f           ∎

  -- Stability is closed under implicit Π-types.

  Stable-implicit-Π :
    {A : Type a} {P : A → Type a} →
    (∀ x → Stable (P x)) →
    Stable ({x : A} → P x)
  Stable-implicit-Π {A = A} {P = P} hyp =
    ◯ ({x : A} → P x)  →⟨ ◯-map (λ f _ → f) ⟩
    ◯ ((x : A) → P x)  →⟨ Stable-Π hyp ⟩
    ((x : A) → P x)    →⟨ (λ f → f _) ⟩□
    ({x : A} → P x)    □

  abstract

    -- If A is modal, and P x is k-stable for all x, then Σ A P is
    -- k-stable.

    Stable-Σ :
      {P : A → Type a} →
      Modal A →
      (∀ x → Stable-[ k ] (P x)) →
      Stable-[ k ] (Σ A P)
    Stable-Σ {A = A} {P = P} m s =
      ◯ (Σ A P)    ↔⟨ Modal→◯Σ≃Σ◯ m ⟩
      Σ A (◯ ∘ P)  ↝⟨ ∃-cong s ⟩□
      Σ A P        □

    -- A lemma relating Stable-Σ and Modal-Σ.

    Stable-Σ-Modal-Σ :
      (m₂ : ∀ x → Modal (P x)) →
      Stable-Σ m₁ (λ x → Modal→Stable (m₂ x)) x ≡
      Modal→Stable (Modal-Σ m₁ m₂) x
    Stable-Σ-Modal-Σ {m₁ = m₁} {x = x} m₂ =
      ◯-elim
        {P = λ x →
               Stable-Σ m₁ (λ x → Modal→Stable (m₂ x)) x ≡
               Modal→Stable (Modal-Σ m₁ m₂) x}
        (λ _ → Modal→Separated (Modal-Σ m₁ m₂) _ _)
        (λ (x , y) →
           Σ-map id (Modal→Stable (m₂ _))
             (◯-rec _ (Σ-map id η) (η (x , y)))      ≡⟨ cong (Σ-map id (Modal→Stable (m₂ _))) ◯-rec-η ⟩

           (x , Modal→Stable (m₂ _) (η y))           ≡⟨ cong (_ ,_) Modal→Stable-η ⟩

           (x , y)                                   ≡⟨ sym Modal→Stable-η ⟩∎

           Modal→Stable (Modal-Σ m₁ m₂) (η (x , y))  ∎)
        x

  -- If A and B are k-stable, then A × B is k-stable.

  Stable-× : Stable-[ k ] A → Stable-[ k ] B → Stable-[ k ] (A × B)
  Stable-× {A = A} {B = B} sA sB =
    ◯ (A × B)  ↔⟨ ◯× ⟩
    ◯ A × ◯ B  ↝⟨ sA ×-cong sB ⟩□
    A × B      □

  -- If A and B are stable, then A ⇔ B is stable.

  Stable-⇔ : Stable A → Stable B → Stable (A ⇔ B)
  Stable-⇔ {A = A} {B = B} sA sB =
    ◯ (A ⇔ B)              ↔⟨ ◯-cong-↔ ⇔↔→×→ ⟩
    ◯ ((A → B) × (B → A))  ↝⟨ Stable-× (Stable-Π λ _ → sB) (Stable-Π λ _ → sA) ⟩
    (A → B) × (B → A)      ↔⟨ inverse ⇔↔→×→ ⟩□
    A ⇔ B                  □

  -- Stable respects logical equivalences.

  Stable-respects-⇔ :
    A ⇔ B → Stable A → Stable B
  Stable-respects-⇔ {A = A} {B = B} A⇔B s =
    ◯ B  →⟨ ◯-map $ _⇔_.from A⇔B ⟩
    ◯ A  →⟨ s ⟩
    A    →⟨ _⇔_.to A⇔B ⟩□
    B    □

  -- Stable-[ k ] respects equivalences.

  Stable-respects-≃ :
    A ≃ B → Stable-[ k ] A → Stable-[ k ] B
  Stable-respects-≃ {A = A} {B = B} A≃B s =
    ◯ B  ↔⟨ ◯-cong-≃ $ inverse A≃B ⟩
    ◯ A  ↝⟨ s ⟩
    A    ↔⟨ A≃B ⟩□
    B    □

  -- A variant of Stable-respects-≃.

  Stable-respects-↝ :
    Extensionality? k c d →
    A ↝[ c ∣ d ] B →
    Stable-[ k ] A → Stable-[ k ] B
  Stable-respects-↝ {A = A} {B = B} ext A↝B s =
    ◯ B  ↝⟨ ◯-cong-↝ ext $ inverse-ext? A↝B ⟩
    ◯ A  ↝⟨ s ⟩
    A    ↝⟨ A↝B ext ⟩□
    B    □

  -- If f has type A → B, where A is modal and B is separated, then
  -- Is-equivalence f is stable.

  Modal→Stable-Is-equivalence :
    {f : A → B} →
    Modal A → Separated B →
    Stable (Is-equivalence f)
  Modal→Stable-Is-equivalence {f = f} m s =
                                          $⟨ s′ ⟩
    Stable (∀ y → Contractible (f ⁻¹ y))  →⟨ Stable-respects-⇔ $ inverse $
                                             Is-equivalence≃Is-equivalence-CP _ ⟩□
    Stable (Is-equivalence f)             □
    where
    s′ =
      Stable-Π λ y →
      let m′ : Modal (f ⁻¹ y)
          m′ = Modal-Σ m (λ _ → s _ _) in
      Stable-Σ m′ λ _ →
      Stable-Π λ _ →
      Modal→Stable (Modal→Separated m′ _ _)

  -- If A is "modal n levels up", then H-level′ n A is stable.

  Stable-H-level′ :
    ∀ n →
    For-iterated-equality n Modal A →
    Stable (H-level′ n A)
  Stable-H-level′ {A = A} zero =
    Modal A                  →⟨ (λ m →
                                   Stable-Σ m λ _ →
                                   Stable-Π λ _ →
                                   Modal→Stable $ Modal→Separated m _ _) ⟩□
    Stable (Contractible A)  □
  Stable-H-level′ {A = A} (suc n) =
    For-iterated-equality (suc n) Modal A    →⟨ (λ m →
                                                   Stable-Π λ _ →
                                                   Stable-Π λ _ →
                                                   Stable-H-level′ n $
                                                   m _ _) ⟩□
    Stable ((x y : A) → H-level′ n (x ≡ y))  □

  -- If A is "modal n levels up", then H-level n A is stable.

  Stable-H-level :
    ∀ n →
    For-iterated-equality n Modal A →
    Stable (H-level n A)
  Stable-H-level {A = A} n m =
    ◯ (H-level n A)   →⟨ ◯-map $ H-level↔H-level′ _ ⟩
    ◯ (H-level′ n A)  →⟨ Stable-H-level′ n m ⟩
    H-level′ n A      →⟨ _⇔_.from $ H-level↔H-level′ _ ⟩□
    H-level n A       □

  ----------------------------------------------------------------------
  -- Some definitions related to Erased

  -- I did not take the definitions in this section from "Modalities
  -- in Homotopy Type Theory" or the corresponding Coq code.

  -- ◯ (Erased A) implies Erased (◯ A).

  ◯-Erased→Erased-◯ :
    {@ A : Type a} →
    @ ◯ (Erased A) → Erased (◯ A)
  ◯-Erased→Erased-◯ x = E.[ ◯-map E.erased x ]

  -- A definition of what it means for the modality to "commute with
  -- Erased".

  Commutes-with-Erased : Type (lsuc a)
  Commutes-with-Erased =
    {A : Type a} →
    Is-equivalence (λ (x : ◯ (Erased A)) → ◯-Erased→Erased-◯ x)

  -- Commutes-with-Erased is a proposition (assuming function
  -- extensionality).

  Commutes-with-Erased-propositional :
    Extensionality (lsuc a) a →
    Is-proposition Commutes-with-Erased
  Commutes-with-Erased-propositional ext =
    implicit-Π-closure ext  λ _ →
    Is-equivalence-propositional
      (lower-extensionality _ lzero ext)

  -- If A is stable, then Erased A is stable.

  Stable-Erased : {@ A : Type a} → @ Stable A → Stable (Erased A)
  Stable-Erased {A = A} s =
    ◯ (Erased A)  →⟨ (λ x → ◯-Erased→Erased-◯ x) ⟩
    Erased (◯ A)  →⟨ E.map s ⟩□
    Erased A      □

  -- If A is modal, then Contractibleᴱ A is stable.

  Stable-Contractibleᴱ :
    Modal A →
    Stable (Contractibleᴱ A)
  Stable-Contractibleᴱ m =
    Stable-Σ m λ _ →
    Stable-Erased (
    Stable-Π λ _ →
    Modal→Stable (Modal→Separated m _ _))

  -- If f has type A → B, A is modal, and equality is stable for B,
  -- then f ⁻¹ᴱ y is stable.

  Stable-⁻¹ᴱ :
    {A B : Type a} {f : A → B} {y : B} →
    Modal A →
    @ For-iterated-equality  Stable B →
    Stable (f ⁻¹ᴱ y)
  Stable-⁻¹ᴱ m s =
    Stable-Σ m λ _ →
    Stable-Erased (s _ _)

  ----------------------------------------------------------------------
  -- Some variants of the eliminators

  -- I did not take the definitions in this section from "Modalities
  -- in Homotopy Type Theory" or the corresponding Coq code (but
  -- perhaps something similar can be found there).

  abstract

    -- A variant of ◯-elim that uses Stable instead of Modal.

    ◯-elim′ :
      (∀ x → Stable (P x)) →
      ((x : A) → P (η x)) →
      ((x : ◯ A) → P x)
    ◯-elim′ {A = A} {P = P} s =
      ((x : A) → P (η x))      →⟨ η ∘_ ⟩
      ((x : A) → ◯ (P (η x)))  →⟨ _⇔_.from $ Π◯◯≃Π◯η _ ⟩
      ((x : ◯ A) → ◯ (P x))    →⟨ (λ f x → s x (f x)) ⟩□
      ((x : ◯ A) → P x)        □

    -- Three "computation rules" for ◯-elim′.

    ◯-elim′-η :
      {s : ∀ x → Stable (P x)} →
      ◯-elim′ s f (η x) ≡ s (η x) (η (f x))
    ◯-elim′-η {P = P} {f = f} {x = x} {s = s} =
      ◯-elim′ s f (η x)                                         ≡⟨⟩
      s (η x) (◯-elim (λ x → Modal-◯ {A = P x}) (η ∘ f) (η x))  ≡⟨ cong (s (η x)) ◯-elim-η ⟩∎
      s (η x) (η (f x))                                         ∎

    ◯-elim′-η′ :
      s (η x) (η (f x)) ≡ f x →
      ◯-elim′ s f (η x) ≡ f x
    ◯-elim′-η′ {s = s} {x = x} {f = f} hyp =
      ◯-elim′ s f (η x)  ≡⟨ ◯-elim′-η {s = s} ⟩
      s (η x) (η (f x))  ≡⟨ hyp ⟩∎
      f x                ∎

    ◯-elim′-Modal→Stable-η :
      ◯-elim′ (Modal→Stable ∘ m) f (η x) ≡ f x
    ◯-elim′-Modal→Stable-η {m = m} {f = f} {x = x} =
      ◯-elim′-η′ {s = Modal→Stable ∘ m}
        (Modal→Stable (m (η x)) (η (f x))  ≡⟨ Modal→Stable-η ⟩∎
         f x                               ∎)

    -- A variant of ◯-rec that uses Stable instead of Modal.

    ◯-rec′ : Stable B → (A → B) → (◯ A → B)
    ◯-rec′ s = ◯-elim′ (λ _ → s)

    -- Three "computation rules" for ◯-rec′.

    ◯-rec′-η : ◯-rec′ s f (η x) ≡ s (η (f x))
    ◯-rec′-η {s = s} = ◯-elim′-η {s = λ _ → s}

    ◯-rec′-η′ :
      s (η (f x)) ≡ f x →
      ◯-rec′ s f (η x) ≡ f x
    ◯-rec′-η′ {s = s} = ◯-elim′-η′ {s = λ _ → s}

    ◯-rec′-Modal→Stable-η :
      ◯-rec′ (Modal→Stable m) f (η x) ≡ f x
    ◯-rec′-Modal→Stable-η {m = m} =
      ◯-elim′-Modal→Stable-η {m = λ _ → m}

  -- If s : Stable B and a certain "computation rule" holds for ◯-rec′
  -- and s, then B is modal.

  ◯-rec′-η→Modal :
    (s : Stable B) →
    (∀ {A} {f : A → B} {x : A} → ◯-rec′ s f (η x) ≡ f x) →
    Modal B
  ◯-rec′-η→Modal s ◯-rec′-η′ =
    Stable→left-inverse→Modal
      s
      (λ x →
         s (η x)            ≡⟨ sym ◯-rec′-η ⟩
         ◯-rec′ s id (η x)  ≡⟨ ◯-rec′-η′ ⟩∎
         x                  ∎)

  abstract

    -- A binary variant of ◯-elim.

    ◯-elim₂ :
      {P : ◯ A → ◯ B → Type a} →
      (∀ x y → Modal (P x y)) →
      ((x : A) (y : B) → P (η x) (η y)) →
      ((x : ◯ A) (y : ◯ B) → P x y)
    ◯-elim₂ {P = P} m f x y =                      $⟨ ◯-elim
                                                        {P = uncurry P ∘ _≃_.to ◯×}
                                                        (uncurry m ∘ _≃_.to ◯×)
                                                        (λ (x , y) → subst (uncurry P) (sym ◯×-η) (f x y))
                                                        (_≃_.from ◯× (x , y)) ⟩
      uncurry P (_≃_.to ◯× (_≃_.from ◯× (x , y)))  →⟨ subst (uncurry P) (_≃_.right-inverse-of ◯× _) ⟩□
      P x y                                        □

    -- A "computation rule" for ◯-elim₂.

    ◯-elim₂-η :
      Extensionality a a →
      ◯-elim₂ m f (η x) (η y) ≡ f x y
    ◯-elim₂-η {m = m} {f = f} {x = x} {y = y} ext =
      let P = _ in

      subst (uncurry P) (_≃_.right-inverse-of ◯× (η x , η y))
        (◯-elim
           (uncurry m ∘ _≃_.to ◯×)
           (λ (x , y) → subst (uncurry P) (sym ◯×-η) (f x y))
           (_≃_.from ◯× (η x , η y)))                              ≡⟨ (cong (subst _ _) $
                                                                       cong (flip (◯-elim (uncurry m ∘ _≃_.to ◯×)) _) $
                                                                       apply-ext ext λ p →
                                                                       cong (flip (subst _) _) $ cong sym $ cong (_$ p) $ sym $
                                                                       _≃_.left-inverse-of (Eq.extensionality-isomorphism ext) _) ⟩
      subst (uncurry P) (_≃_.right-inverse-of ◯× (η x , η y))
        (◯-elim
           (uncurry m ∘ _≃_.to ◯×)
           (subst (uncurry P) (sym (ext⁻¹ ◯×-η′ _)) ∘ uncurry f)
           (_≃_.from ◯× (η x , η y)))                              ≡⟨ elim¹
                                                                        (λ {g} (eq : _≃_.to ◯× ∘ η ≡ g) →
                                                                           (f : ∀ p → uncurry P (g p)) →
                                                                           subst (uncurry P) (_≃_.right-inverse-of ◯× (g (x , y)))
                                                                             (◯-elim
                                                                                (uncurry m ∘ _≃_.to ◯×)
                                                                                (subst (uncurry P) (sym (ext⁻¹ {f = _≃_.to ◯× ∘ η} eq _)) ∘ f)
                                                                                (_≃_.from ◯× (g (x , y)))) ≡
                                                                           f (x , y))
                                                                        (λ f →
        subst (uncurry P)
          (_≃_.right-inverse-of ◯× (_≃_.to ◯× (η (x , y))))
          (◯-elim
             (uncurry m ∘ _≃_.to ◯×)
             (subst (uncurry P)
                (sym (ext⁻¹ {f = _≃_.to ◯× ∘ η} (refl _) _)) ∘
              f)
             (_≃_.from ◯× (_≃_.to ◯× (η (x , y)))))                        ≡⟨ (cong (subst _ _) $ cong (flip (◯-elim _) _) $
                                                                               apply-ext ext λ _ →
                                                                               trans (cong (flip (subst _) _) $
                                                                                      trans (cong sym $ ext⁻¹-refl _)
                                                                                      sym-refl) $
                                                                               subst-refl _ _) ⟩
        subst (uncurry P)
          (_≃_.right-inverse-of ◯× (_≃_.to ◯× (η (x , y))))
          (◯-elim
             (uncurry m ∘ _≃_.to ◯×)
             f
             (_≃_.from ◯× (_≃_.to ◯× (η (x , y)))))                        ≡⟨ cong (flip (subst _) _) $ sym $
                                                                              _≃_.left-right-lemma ◯× _ ⟩
        subst (uncurry P)
          (cong (_≃_.to ◯×) (_≃_.left-inverse-of ◯× (η (x , y))))
          (◯-elim
             (uncurry m ∘ _≃_.to ◯×)
             f
             (_≃_.from ◯× (_≃_.to ◯× (η (x , y)))))                        ≡⟨ elim₁
                                                                                (λ {p} (eq : p ≡ η (x , y)) →
                                                                                   subst (uncurry P)
                                                                                     (cong (_≃_.to ◯×) eq)
                                                                                     (◯-elim (uncurry m ∘ _≃_.to ◯×) f p) ≡
                                                                                   f (x , y))
                                                                                (
          subst (uncurry P)
            (cong (_≃_.to ◯×) (refl _))
            (◯-elim (uncurry m ∘ _≃_.to ◯×) f (η (x , y)))                       ≡⟨ trans (cong (flip (subst _) _) $
                                                                                           cong-refl _) $
                                                                                    subst-refl _ _ ⟩

          ◯-elim (uncurry m ∘ _≃_.to ◯×) f (η (x , y))                           ≡⟨ ◯-elim-η ⟩∎

          f (x , y)                                                              ∎)
                                                                                _ ⟩∎
        f (x , y)                                                          ∎)
                                                                        _ _ ⟩∎
      f x y                                                        ∎
      where
      ◯×-η′ : _≃_.to (◯× {A = A} {B = B}) ∘ η ≡ Σ-map η η
      ◯×-η′ = apply-ext ext λ _ → ◯×-η

    -- A binary variant of ◯-rec.

    ◯-rec₂ : Modal C → (A → B → C) → (◯ A → ◯ B → C)
    ◯-rec₂ m f x y = ◯-rec m (uncurry f) (_≃_.from ◯× (x , y))

    -- A "computation rule" for ◯-rec₂.

    ◯-rec₂-η : ◯-rec₂ m f (η x) (η y) ≡ f x y
    ◯-rec₂-η {m = m} {f = f} {x = x} {y = y} =
      ◯-rec m (uncurry f) (_≃_.from ◯× (η x , η y))  ≡⟨ cong (◯-rec _ _) ◯×⁻¹-η ⟩
      ◯-rec m (uncurry f) (η (x , y))                ≡⟨ ◯-rec-η ⟩∎
      f x y                                          ∎

  ----------------------------------------------------------------------
  -- Idempotent monadic modalities are monads

  -- At the time of writing I do not know if corresponding definitions
  -- appear in the source code corresponding to "Modalities in
  -- Homotopy Type Theory". The definitions are entirely
  -- straightforward, with the possible exception of the use of
  -- ◯-elim′ and Stable-Π—rather than ◯-elim, Modal-Π and function
  -- extensionality—in the proof of associativity.

  -- The modality is a raw monad.

  raw-monad : Raw-monad ◯
  Raw-monad.return raw-monad     = η
  Raw-monad._>>=_  raw-monad x f = ◯-rec Modal-◯ f x

  instance

    -- The modality is a monad.

    monad : Monad ◯
    Monad.raw-monad monad         = raw-monad
    Monad.left-identity monad x f =
      ◯-rec Modal-◯ f (η x)  ≡⟨ ◯-rec-η ⟩∎
      f x                    ∎
    Monad.right-identity monad = ◯-elim
      (λ _ → Separated-◯ _ _)
      (λ x →
         ◯-rec Modal-◯ η (η x)  ≡⟨ ◯-rec-η ⟩∎
         η x                    ∎)
    Monad.associativity monad = ◯-elim′
      (λ _ → Stable-Π λ _ → Stable-Π λ _ →
             Modal→Stable $ Separated-◯ _ _)
      (λ x f g →
         ◯-rec Modal-◯ (◯-rec Modal-◯ g ∘ f) (η x)  ≡⟨ ◯-rec-η ⟩
         ◯-rec Modal-◯ g (f x)                      ≡⟨ cong (◯-rec Modal-◯ g) $ sym ◯-rec-η ⟩∎
         ◯-rec Modal-◯ g (◯-rec Modal-◯ f (η x))    ∎)

  ----------------------------------------------------------------------
  -- A lemma related to h-levels

  -- If A is a proposition, then ◯ A is a proposition.
  --
  -- See also Contractible→Connected below.

  Is-proposition→Is-proposition-◯ :
    Is-proposition A → Is-proposition (◯ A)
  Is-proposition→Is-proposition-◯ {A = A} prop =
    ◯-elim₂
      (λ _ _ → Separated-◯ _ _)
      (λ x y →
         η x  ≡⟨ cong η $ prop x y ⟩∎
         η y  ∎)

  ----------------------------------------------------------------------
  -- Commuting with Σ

  -- I did not take the definitions and lemmas in this section from
  -- "Modalities in Homotopy Type Theory" or the corresponding Coq
  -- code.

  private abstract

    -- A lemma used in the implementation of ◯Ση≃Σ◯◯.

    Modal-Σ◯◯ : Modal (Σ (◯ A) (◯ ∘ P))
    Modal-Σ◯◯ = Modal-Σ Modal-◯ λ _ → Modal-◯

  -- ◯ commutes with Σ in a certain way (assuming function
  -- extensionality).
  --
  -- This lemma is due to Felix Cherubini.
  --
  -- See also Modality.Very-modal.◯Ση≃Σ◯◯.

  ◯Ση≃Σ◯◯ : ◯ (Σ A (P ∘ η)) ↝[ a ∣ a ] Σ (◯ A) (◯ ∘ P)
  ◯Ση≃Σ◯◯ {A = A} {P = P} =
    generalise-ext?
      (record { to = to; from = from })
      (λ ext → to-from ext , from-to ext)
    where
    abstract
      s′ : (x : ◯ A) → Stable ((y : P x) → ◯ (Σ A (P ∘ η)))
      s′ _ = Stable-Π λ _ → Modal→Stable Modal-◯

      m″ :
        Extensionality a a →
        (x : ◯ A) → Modal ((y : P x) → ◯ (Σ A (P ∘ η)))
      m″ ext _ = Modal-Π ext λ _ → Modal-◯

      s′-≡ : ∀ ext → s′ ≡ Modal→Stable ∘ m″ ext
      s′-≡ ext =
        apply-ext ext λ _ →
        Stable-Π (λ _ → Modal→Stable Modal-◯)     ≡⟨ Stable-Π-Modal-Π ext ⟩∎
        Modal→Stable (Modal-Π ext λ _ → Modal-◯)  ∎

    to : ◯ (Σ A (P ∘ η)) → Σ (◯ A) (◯ ∘ P)
    to = ◯-rec Modal-Σ◯◯ (Σ-map η η)

    from : Σ (◯ A) (◯ ∘ P) → ◯ (Σ A (P ∘ η))
    from =
      Σ (◯ A) (◯ ∘ P)  →⟨ (λ (x , y) → ◯-map (x ,_) y) ⟩
      ◯ (Σ (◯ A) P)    →⟨ ◯-rec Modal-◯ (uncurry $ ◯-elim′ s′ $ curry η) ⟩□
      ◯ (Σ A (P ∘ η))  □

    to-from :
      Extensionality a a →
      ∀ x → to (from x) ≡ x
    to-from ext = uncurry $
      ◯-elim
        (λ _ → Modal-Π ext λ _ →
               Modal→Separated Modal-Σ◯◯ _ _)
        (λ x →
           ◯-elim
             (λ _ → Modal→Separated Modal-Σ◯◯ _ _)
             (λ y →
                to
                  (◯-rec Modal-◯ (uncurry $ ◯-elim′ s′ $ curry η)
                     (◯-map (η x ,_) (η y)))                            ≡⟨ cong to $ cong (◯-rec _ _) ◯-map-η ⟩

                to
                  (◯-rec Modal-◯ (uncurry $ ◯-elim′ s′ $ curry η)
                     (η (η x , y)))                                     ≡⟨ cong to ◯-rec-η ⟩

                to (◯-elim′ s′ (curry η) (η x) y)                       ≡⟨ cong (λ s → to (◯-elim′ s (curry η) (η x) y)) $
                                                                           s′-≡ ext ⟩

                to (◯-elim′ (Modal→Stable ∘ m″ ext) (curry η) (η x) y)  ≡⟨ cong to $ cong (_$ y) ◯-elim′-Modal→Stable-η ⟩

                to (η (x , y))                                          ≡⟨⟩

                ◯-rec Modal-Σ◯◯ (Σ-map η η) (η (x , y))                 ≡⟨ ◯-rec-η ⟩∎

                (η x , η y)                                             ∎))

    from-to :
      Extensionality a a →
      ∀ x → from (to x) ≡ x
    from-to ext =
      ◯-elim
        (λ _ → Separated-◯ _ _)
        (λ (x , y) →
           let f = λ (x , y) → ◯-map (x ,_) y in

           ◯-rec Modal-◯ (uncurry $ ◯-elim′ s′ $ curry η)
             (f (◯-rec Modal-Σ◯◯ (Σ-map η η) (η (x , y))))               ≡⟨ cong (◯-rec _ _) $ cong f ◯-rec-η ⟩

           ◯-rec Modal-◯ (uncurry $ ◯-elim′ s′ $ curry η)
             (◯-map (η x ,_) (η y))                                      ≡⟨ cong (◯-rec _ _) ◯-map-η ⟩

           ◯-rec Modal-◯ (uncurry $ ◯-elim′ s′ $ curry η) (η (η x , y))  ≡⟨ ◯-rec-η ⟩

           ◯-elim′ s′ (curry η) (η x) y                                  ≡⟨ cong (λ s → ◯-elim′ s (curry η) (η x) y) $ s′-≡ ext ⟩

           ◯-elim′ (Modal→Stable ∘ m″ ext) (curry η) (η x) y             ≡⟨ cong (_$ y) ◯-elim′-Modal→Stable-η ⟩∎

           η (x , y)                                                     ∎)

  -- A definition of what it means for the modality to "commute with
  -- Σ".

  Commutes-with-Σ : Type (lsuc a)
  Commutes-with-Σ =
    {A : Type a} {P : ◯ A → Type a} →
    Is-equivalence (◯Ση≃Σ◯◯ {A = A} {P = P} _)

  -- If function extensionality holds, then the modality commutes with
  -- Σ.
  --
  -- See also Modality.Very-modal.commutes-with-Σ.

  commutes-with-Σ :
    Extensionality a a →
    Commutes-with-Σ
  commutes-with-Σ ext = _≃_.is-equivalence $ ◯Ση≃Σ◯◯ ext

  -- Commutes-with-Σ is a proposition (assuming function
  -- extensionality).

  Commutes-with-Σ-propositional :
    Extensionality (lsuc a) (lsuc a) →
    Is-proposition Commutes-with-Σ
  Commutes-with-Σ-propositional ext =
    implicit-Π-closure ext  λ _ →
    implicit-Π-closure (lower-extensionality lzero _ ext)  λ _ →
    Is-equivalence-propositional (lower-extensionality _ _ ext)

  ----------------------------------------------------------------------
  -- Some variants of Π◯◯≃Π◯η

  -- I did not take the lemmas in this section from "Modalities in
  -- Homotopy Type Theory" or the corresponding Coq code.

  -- Some variants of Π◯◯≃Π◯η, stated using stability.

  Π◯≃Πη :
    Extensionality? ⌊ k ⌋-sym a a →
    (∀ x → Stable-[ ⌊ k ⌋-sym ] (P x)) →
    ((x : ◯ A) → P x) ↝[ ⌊ k ⌋-sym ] ((x : A) → P (η x))
  Π◯≃Πη {A = A} {P = P} ext s =
    ((x : ◯ A) → P x)        ↝⟨ ∀-cong ext (inverse ∘ s) ⟩
    ((x : ◯ A) → ◯ (P x))    ↝⟨ Π◯◯≃Π◯η ext ⟩
    ((x : A) → ◯ (P (η x)))  ↝⟨ ∀-cong ext (s ∘ η) ⟩□
    ((x : A) → P (η x))      □

  Π◯↝Πη :
    (∀ {k} → Extensionality? k a a → ∀ x → Stable-[ k ] (P x)) →
    ((x : ◯ A) → P x) ↝[ a ∣ a ] ((x : A) → P (η x))
  Π◯↝Πη s = generalise-ext?′
    (Π◯≃Πη _ (s _))
    (λ ext → Π◯≃Πη ext (s ext))
    (λ ext → Π◯≃Πη E.[ ext ] (s E.[ ext ]))

  Π◯⇔Πη :
    (∀ x → Stable (P x)) →
    ((x : ◯ A) → P x) ⇔ ((x : A) → P (η x))
  Π◯⇔Πη s = Π◯≃Πη _ (Stable→Stable-⇔ ∘ s)

  -- Two simplification rules for Π◯≃Πη.

  Π◯≃Πη-η :
    ∀ ext s (f : ∀ x → P x) →
    _≃_.to (Π◯≃Πη ext s) f x ≡ f (η x)
  Π◯≃Πη-η {x = x} ext s f =
    _≃_.to (Π◯≃Πη ext s) f x                         ≡⟨⟩
    _≃_.to (s (η x)) (_≃_.from (s (η x)) (f (η x)))  ≡⟨ _≃_.right-inverse-of (s (η x)) _ ⟩∎
    f (η x)                                          ∎

  Π◯≃Πη⁻¹-η :
    ∀ ext (s : ∀ x → Stable-[ equivalence ] (P x)) →
    _≃_.from (Π◯≃Πη {P = P} ext s) f (η x) ≡ f x
  Π◯≃Πη⁻¹-η {P = P} {f = f} {x = x} ext s =
    _≃_.from (Π◯≃Πη ext s) f (η x)               ≡⟨⟩

    _≃_.to (s (η x))
      (◯-elim
         {P = ◯ ∘ P}
         (λ _ → Modal-◯)
         (λ x → _≃_.from (s (η x)) (f x))
         (η x))                                  ≡⟨ cong (_≃_.to (s (η x))) ◯-elim-η ⟩

    _≃_.to (s (η x)) (_≃_.from (s (η x)) (f x))  ≡⟨ _≃_.right-inverse-of (s (η x)) _ ⟩∎

    f x                                          ∎

  ----------------------------------------------------------------------
  -- Map-like lemmas for Modal and Separated

  -- If there is an embedding from B to A, and A is separated, then B
  -- is separated.
  --
  -- This follows from one part of Remark 2.16 (2) from "Localization
  -- in homotopy type theory" by Christensen, Opie, Rijke and
  -- Scoccola.
  --
  -- I based the proof on that of in_SepO_embedding, implemented by
  -- Mike Shulman in the file Separated.v in (one version of) the Coq
  -- HoTT library.

  Embedding→Separated→Separated :
    Embedding B A → Separated A → Separated B
  Embedding→Separated→Separated B↣A s x y =
                                                     $⟨ s _ _ ⟩
    Modal (Embedding.to B↣A x ≡ Embedding.to B↣A y)  →⟨ Modal-respects-≃ (inverse $ Embedding.equivalence B↣A) ⟩□
    Modal (x ≡ y)                                    □

  -- I did not take the remaining results in this section from
  -- "Modalities in Homotopy Type Theory" or the corresponding Coq
  -- code.

  -- Modal respects split surjections.

  Modal-respects-↠ : A ↠ B → Modal A → Modal B
  Modal-respects-↠ {A = A} {B = B} A↠B m =
    Stable→left-inverse→Modal
      (◯ B  →⟨ ◯-map (_↠_.from A↠B) ⟩
       ◯ A  →⟨ η⁻¹ m ⟩
       A    →⟨ _↠_.to A↠B ⟩□
       B    □)
      (λ x →
         _↠_.to A↠B (η⁻¹ m (◯-map (_↠_.from A↠B) (η x)))  ≡⟨ cong (_↠_.to A↠B ∘ η⁻¹ _) ◯-map-η ⟩
         _↠_.to A↠B (η⁻¹ m (η (_↠_.from A↠B x)))          ≡⟨ cong (_↠_.to A↠B) η⁻¹-η ⟩
         _↠_.to A↠B (_↠_.from A↠B x)                      ≡⟨ _↠_.right-inverse-of A↠B x ⟩∎
         x                                                ∎)

  -- A generalisation of Modal-respects-↠.
  --
  -- The case for 1 is one part of Remark 2.16 (2) from "Localization
  -- in homotopy type theory" by Christensen, Opie, Rijke and
  -- Scoccola.

  Modal-respects-↠ⁿ :
    ∀ n →
    A ↠ B →
    For-iterated-equality n Modal A →
    For-iterated-equality n Modal B
  Modal-respects-↠ⁿ n =
    For-iterated-equality-cong-→ n Modal-respects-↠

  ----------------------------------------------------------------------
  -- Lemmas related to Separated

  -- I did not take the lemmas in this section from "Modalities in
  -- Homotopy Type Theory" or the corresponding Coq code (but perhaps
  -- something similar can be found there).

  -- Propositions are separated.
  --
  -- This is Remark 2.16 (3) from "Localization in homotopy type
  -- theory" by Christensen, Opie, Rijke and Scoccola.

  Is-proposition→Separated : Is-proposition A → Separated A
  Is-proposition→Separated {A = A} prop =
    Embedding→Separated→Separated
      emb
      (Modal→Separated Modal-⊤)
    where
    emb : Embedding A (↑ a ⊤)
    emb = record
      { to           = _
      ; is-embedding = λ x y →
          _≃_.is-equivalence $
          Eq.↔→≃
            _
            (λ _ → prop x y)
            (λ _ → H-level.mono₁ 
                     (H-level.mono₁  (↑-closure  ⊤-contractible))
                     _ _)
            (λ _ → H-level.mono₁  prop _ _)
      }

  -- If A is separated, then W A P is separated (assuming function
  -- extensionality).

  Separated-W :
    {P : A → Type a} →
    Extensionality a a →
    Separated A →
    Separated (W A P)
  Separated-W {A = A} {P = P} ext s = λ x y →
    Stable→left-inverse→Modal
      (Stable-≡-W   x y)
      (Stable-≡-W-η x y)
    where
    head-lemma : sup x f ≡ sup y g → x ≡ y
    head-lemma = proj₁ ∘ Σ-≡,≡←≡ ∘ cong (_↔_.to W-unfolding)

    tail-lemma :
      (eq : sup x f ≡ sup y g) →
      subst (λ x → P x → W A P) (head-lemma eq) f ≡ g
    tail-lemma = proj₂ ∘ Σ-≡,≡←≡ ∘ cong (_↔_.to W-unfolding)

    heads : ◯ (_≡_ {A = W A P} (sup x f) (sup y g)) → x ≡ y
    heads {x = x} {f = f} {y = y} {g = g} =
      ◯ (sup x f ≡ sup y g)  →⟨ ◯-map head-lemma ⟩
      ◯ (x ≡ y)              →⟨ Modal→Stable (s _ _) ⟩□
      x ≡ y                  □

    heads-η : heads (η eq) ≡ head-lemma eq
    heads-η =
      trans (cong (Modal→Stable _) ◯-map-η) $
      Modal→Stable-η

    tails :
      (eq : ◯ (sup x f ≡ sup y g)) →
      ◯ (subst (λ x → P x → W A P) (heads eq) f z ≡
         g z)
    tails {f = f} {g = g} {z = z} =
      ◯-elim
        (λ _ → Modal-◯)
        (λ eq → η (cong (_$ z) (
           subst (λ x → P x → W A P) (heads (η eq)) f   ≡⟨ cong (λ eq → subst (λ x → P x → W A P) eq f) heads-η ⟩
           subst (λ x → P x → W A P) (head-lemma eq) f  ≡⟨ tail-lemma eq ⟩∎
           g                                            ∎)))

    tails-η :
      (eq : sup x f ≡ sup y g) →
      tails {z = z} (η eq) ≡
      η (cong (_$ z) $
         trans (cong (λ eq → subst (λ x → P x → W A P) eq f) heads-η) $
         tail-lemma eq)
    tails-η _ = ◯-elim-η

    Stable-≡-W : For-iterated-equality  Stable (W A P)
    Stable-≡-W (sup x f) (sup y g) eq =
      cong (uncurry sup) $
      Σ-≡,≡→≡
        (heads eq)
        (apply-ext ext λ z →
           subst (λ x → P x → W A P) (heads eq) f z  ≡⟨ Stable-≡-W _ (g z) (tails eq) ⟩∎
           g z                                       ∎)

    Stable-≡-W-η :
      (x y : W A P) (eq : x ≡ y) →
      Stable-≡-W x y (η eq) ≡ eq
    Stable-≡-W-η (sup x f) (sup y g) eq =
      cong (uncurry sup)
        (Σ-≡,≡→≡ (heads (η eq))
           (apply-ext ext λ z →
            Stable-≡-W _ (g z) (tails (η eq))))                        ≡⟨ (cong (λ f →
                                                                                   cong (uncurry sup)
                                                                                     (Σ-≡,≡→≡ (heads (η eq))
                                                                                        (apply-ext ext f))) $
                                                                           apply-ext ext λ _ →
                                                                           cong (Stable-≡-W _ (g _)) $
                                                                           tails-η eq) ⟩
      cong (uncurry sup)
        (Σ-≡,≡→≡ (heads (η eq))
           (apply-ext ext λ z →
            Stable-≡-W _ (g z)
              (η (cong (_$ z) $
                  trans (cong (λ eq → subst (λ x → P x → W A P) eq f)
                           heads-η) $
                  tail-lemma eq))))                                    ≡⟨ (cong (λ f →
                                                                                   cong (uncurry sup)
                                                                                     (Σ-≡,≡→≡ (heads (η eq))
                                                                                        (apply-ext ext f))) $
                                                                           apply-ext ext λ z →
                                                                           Stable-≡-W-η _ (g z) _) ⟩
      cong (uncurry sup)
        (Σ-≡,≡→≡ (heads (η eq))
           (apply-ext ext λ z →
            cong (_$ z) $
            trans (cong (λ eq → subst (λ x → P x → W A P) eq f)
                     heads-η) $
            tail-lemma eq))                                            ≡⟨ cong (cong (uncurry sup) ∘ Σ-≡,≡→≡ (heads (η eq))) $
                                                                          trans (ext-cong ext) $
                                                                          sym $ cong-id _ ⟩
      cong (uncurry sup)
        (Σ-≡,≡→≡ (heads (η eq))
           (trans (cong (λ eq → subst (λ x → P x → W A P) eq f)
                     heads-η) $
            tail-lemma eq))                                            ≡⟨ elim₁
                                                                            (λ {p} eq′ →
                                                                               cong (uncurry sup)
                                                                                 (Σ-≡,≡→≡ p
                                                                                    (trans (cong (λ eq → subst (λ x → P x → W A P) eq f) eq′) $
                                                                                     tail-lemma eq)) ≡
                                                                               cong (uncurry sup) (Σ-≡,≡→≡ (head-lemma eq) (tail-lemma eq)))
                                                                            (cong (cong (uncurry sup) ∘ Σ-≡,≡→≡ (head-lemma eq)) $
                                                                             trans (cong (flip trans _) $ cong-refl _) $
                                                                             trans-reflˡ _)
                                                                            _ ⟩

      cong (uncurry sup) (Σ-≡,≡→≡ (head-lemma eq) (tail-lemma eq))     ≡⟨ cong (cong (uncurry sup)) $
                                                                          _↔_.right-inverse-of Bijection.Σ-≡,≡↔≡ _ ⟩

      cong (uncurry sup) (cong (_↔_.to W-unfolding) eq)                ≡⟨⟩

      cong (_↔_.from W-unfolding) (cong (_↔_.to W-unfolding) eq)       ≡⟨ cong-∘ _ _ _ ⟩

      cong (_↔_.from W-unfolding ∘ _↔_.to W-unfolding) eq              ≡⟨ sym $
                                                                          trans-[trans]-sym _ _ ⟩
      trans
        (trans (cong (_↔_.from W-unfolding ∘ _↔_.to W-unfolding) eq)
           (_↔_.left-inverse-of W-unfolding (sup y g)))
        (sym (_↔_.left-inverse-of W-unfolding (sup y g)))              ≡⟨ cong (flip trans _) $
                                                                          naturality (_↔_.left-inverse-of W-unfolding) ⟩
      trans
        (trans (_↔_.left-inverse-of W-unfolding (sup x f))
           (cong id eq))
        (sym (_↔_.left-inverse-of W-unfolding (sup y g)))              ≡⟨⟩

      trans (trans (refl _) (cong id eq)) (sym (refl _))               ≡⟨ trans (cong₂ trans
                                                                                   (trans (trans-reflˡ _) $
                                                                                    sym $ cong-id _)
                                                                                   sym-refl) $
                                                                          trans-reflʳ _ ⟩∎
      eq                                                               ∎

  ----------------------------------------------------------------------
  -- Flattening lemmas

  -- Some flattening lemmas.
  --
  -- I did not take these lemmas from "Modalities in Homotopy Type
  -- Theory" or the corresponding Coq code.

  flatten-→ :
    (F : (Type a → Type a) → Type a) →
    (F ◯ → ◯ (F id)) →
    ◯ (F ◯) → ◯ (F id)
  flatten-→ _ f = ◯-rec Modal-◯ f

  flatten-⇔ :
    (F : (Type a → Type a) → Type a) →
    (∀ {G H} → (∀ {A} → G A → H A) → F G → F H) →
    (F ◯ → ◯ (F id)) →
    ◯ (F ◯) ⇔ ◯ (F id)
  flatten-⇔ F map f = record
    { to   = flatten-→ F f
    ; from = ◯-map (map η)
    }

  private

    module Flatten
      {F : (Type a → Type a) → Type a}
      (map : ∀ {G H} → (∀ {A} → G A → H A) → F G → F H)
      {f : F ◯ → ◯ (F id)}
      where

      open _⇔_ (flatten-⇔ F map f)

      to-from :
        (∀ x → f (map η x) ≡ η x) →
        ∀ x → to (from x) ≡ x
      to-from f-map =
         ◯-elim
           (λ _ → Separated-◯ _ _)
           (λ x →
              ◯-rec Modal-◯ f (◯-map (map η) (η x))  ≡⟨ cong (◯-rec Modal-◯ f) ◯-map-η ⟩
              ◯-rec Modal-◯ f (η (map η x))          ≡⟨ ◯-rec-η ⟩
              f (map η x)                            ≡⟨ f-map x ⟩∎
              η x                                    ∎)

      from-to :
        (∀ x → ◯-map (map η) (f x) ≡ η x) →
        ∀ x → from (to x) ≡ x
      from-to map-f =
        ◯-elim
          (λ _ → Separated-◯ _ _)
          (λ x →
             ◯-map (map η) (◯-rec Modal-◯ f (η x))  ≡⟨ cong (◯-map (map η)) ◯-rec-η ⟩
             ◯-map (map η) (f x)                    ≡⟨ map-f x ⟩∎
             η x                                    ∎)

  flatten-≃ :
    (F : (Type a → Type a) → Type a) →
    (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 = Eq.↔→≃
    (_⇔_.to equiv)
    (_⇔_.from equiv)
    (Flatten.to-from map f-map)
    (Flatten.from-to map map-f)
    where
    equiv = flatten-⇔ _ map f

  flatten-↝ :
    (F : (Type a → Type a) → Type a) →
    (map : ∀ {G H} → (∀ {A} → G A → H A) → F G → F H) →
    (f : F ◯ → ◯ (F id)) →
    (Extensionality a a →
     (∀ x → f (map η x) ≡ η x) ×
     (∀ x → ◯-map (map η) (f x) ≡ η x)) →
    ◯ (F ◯) ↝[ a ∣ a ] ◯ (F id)
  flatten-↝ _ map f hyp = generalise-ext?
    (flatten-⇔ _ map f)
    (λ ext →
         Flatten.to-from map (hyp ext .proj₁)
       , Flatten.from-to map (hyp ext .proj₂))

  -- ◯ A is equivalent to ◯ (◯ A).

  ◯≃◯◯ : ◯ A ≃ ◯ (◯ A)
  ◯≃◯◯ {A = A} = Eq.↔→≃
    η
    (◯-rec Modal-◯ id)
    (◯-elim
       (λ _ → Separated-◯ _ _)
       (λ x →
          η (◯-rec Modal-◯ id (η x))  ≡⟨ cong η ◯-rec-η ⟩∎
          η x                         ∎))
    (λ _ → ◯-rec-η)

  -- ◯ (Σ A (◯ ∘ P)) is equivalent to ◯ (Σ A P).

  ◯Σ◯≃◯Σ :
    {A : Type a} {P : A → Type a} →
    ◯ (Σ A (◯ ∘ P)) ≃ ◯ (Σ A