```------------------------------------------------------------------------
------------------------------------------------------------------------

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

-- 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ᴱ; _⁻¹ᴱ_)
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 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).
--

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

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

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

-- _-Connected-→ᴱ_ is a variant of _-Connected→_ that uses
--

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

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

{f : A → B} →
Extensionality a a →
Separated A →
Separated B →
Modal (HA.Proofs f g)
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) λ _ →

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

----------------------------------------------------------------------

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

instance

-- The modality is a monad.

◯-rec Modal-◯ f (η x)  ≡⟨ ◯-rec-η ⟩∎
f x                    ∎
(λ _ → Separated-◯ _ _)
(λ x →
◯-rec Modal-◯ η (η x)  ≡⟨ ◯-rec-η ⟩∎
η x                    ∎)
(λ _ → 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.
--

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

◯Ση≃Σ◯◯ : ◯ (Σ 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
-- Σ.
--

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                  □

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) \$
Σ-≡,≡→≡
(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)
(apply-ext ext λ z →
Stable-≡-W _ (g z) (tails (η eq))))                        ≡⟨ (cong (λ f →
cong (uncurry sup)
(apply-ext ext f))) \$
apply-ext ext λ _ →
cong (Stable-≡-W _ (g _)) \$
tails-η eq) ⟩
cong (uncurry sup)
(apply-ext ext λ z →
Stable-≡-W _ (g z)
(η (cong (_\$ z) \$
trans (cong (λ eq → subst (λ x → P x → W A P) eq f)
tail-lemma eq))))                                    ≡⟨ (cong (λ f →
cong (uncurry sup)
(apply-ext ext f))) \$
apply-ext ext λ z →
Stable-≡-W-η _ (g z) _) ⟩
cong (uncurry sup)
(apply-ext ext λ z →
cong (_\$ z) \$
trans (cong (λ eq → subst (λ x → P x → W A P) eq f)
tail-lemma eq))                                            ≡⟨ cong (cong (uncurry sup) ∘ Σ-≡,≡→≡ (heads (η eq))) \$
trans (ext-cong ext) \$
sym \$ cong-id _ ⟩
cong (uncurry sup)
(trans (cong (λ eq → subst (λ x → P x → W A P) eq f)
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 ```