------------------------------------------------------------------------
-- 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 1 .proj₁ f .proj₁

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

  ◯-rec-η : ◯-rec m f (η x)  f x
  ◯-rec-η = extendable-along-η _ 1 .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 2 .proj₂ _ _ .proj₁ p .proj₁

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

  ∘η≡∘η→≡-η : ∘η≡∘η→≡ m p (η x)  p x
  ∘η≡∘η→≡-η =
    extendable-along-η _ 2 .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 1 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 0

-- ◯ -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 1 λ _ 
  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  1 λ _ 
  implicit-Π-closure ext′ 1 λ _ 
  implicit-Π-closure ext′ 1 λ _ 
  Π-closure ext′ 1 λ _ 
  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 1 (Left-exact-propositional ext) $
  implicit-Π-closure ext  1 λ _ 
  Π-closure          ext′ 1 λ _ 
  Π-closure          ext′ 1 λ _ 
  H-level-propositional ext′ 0
  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 1 λ _ 
  implicit-Π-closure (lower-extensionality lzero _ ext) 1 λ _ 
  Π-closure (lower-extensionality _ _ ext) 1 λ _ 
  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 1 .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 1 .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 2 .proj₂ _ _ .proj₁ p .proj₁

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

    ∘η≡∘η→≡-η : ∘η≡∘η→≡ m p (η x)  p x
    ∘η≡∘η→≡-η {m = m} {p = p} =
      extendable-along-η m 2 .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 1 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 1 λ _ 
         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 (1 + 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 1 _ ⟩□
    For-iterated-equality (1 + 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-↝ᴱ :
      @0 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ᴱ :
      @0 Extensionality? k c d 
      (∀ {k}  @0 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) 1 λ _ 
                                                                  Is-equivalence-propositional (lower-extensionality _ _ ext)) 
    Is-proposition ({P : A  Type a}  Is-equivalence ◯Π→Π◯)  →⟨ H-level-cong _ 1 (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 1 λ _ 
    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-◯ :
    {@0 A : Type a} 
    @0  (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 1 λ _ 
    Is-equivalence-propositional
      (lower-extensionality _ lzero ext)

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

  Stable-Erased : {@0 A : Type a}  @0 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 
    @0 For-iterated-equality 1 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 1 λ _ 
    implicit-Π-closure (lower-extensionality lzero _ ext) 1 λ _ 
    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₁ 1
                     (H-level.mono₁ 0 (↑-closure 0 ⊤-contractible))
                     _ _)
             _  H-level.mono₁ 1 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 1 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