{-# 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
private
module Dummy where
record Modality-record 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-η :
{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)
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 ∘ η)
Modal : Type a → Type a
Modal A = Is-equivalence (η {A = A})
Modal→≃◯ : Modal A → A ≃ ◯ A
Modal→≃◯ m = Eq.⟨ _ , m ⟩
Π◯◯≃Π◯η : ((x : ◯ A) → ◯ (P x)) ≃ ((x : A) → ◯ (P (η x)))
Π◯◯≃Π◯η = Eq.⟨ _ , uniquely-eliminating ⟩
Stable : Type a → Type a
Stable A = ◯ A → A
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 ∎
Modal-◯ : Modal (◯ A)
Modal-◯ {A = A} = Stable→left-inverse→Modal η⁻¹ η⁻¹-η
where
η⁻¹ : ◯ (◯ A) → ◯ A
η⁻¹ = _≃_.from Π◯◯≃Π◯η id
η⁻¹-η : η⁻¹ ∘ η ≡ id
η⁻¹-η =
_≃_.from Π◯◯≃Π◯η id ∘ η ≡⟨⟩
(_∘ η) (_≃_.from Π◯◯≃Π◯η id) ≡⟨ _≃_.right-inverse-of Π◯◯≃Π◯η _ ⟩∎
id ∎
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) ∎)
◯-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) □
◯-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 ∎
◯-rec : Modal B → (A → B) → (◯ A → B)
◯-rec m = ◯-elim (λ _ → m)
◯-rec-η : ∀ m → ◯-rec m f (η x) ≡ f x
◯-rec-η m = ◯-elim-η (λ _ → m)
◯-map : (A → B) → ◯ A → ◯ B
◯-map f = ◯-rec Modal-◯ (η ∘ f)
◯-map-η : ◯-map f (η x) ≡ η (f x)
◯-map-η = ◯-rec-η Modal-◯
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 ∎)
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
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)
◯-rec : Modal B → (A → B) → (◯ A → B)
◯-rec m f = extendable-along-η m 1 .proj₁ f .proj₁
◯-rec-η : ◯-rec m f (η x) ≡ f x
◯-rec-η = extendable-along-η _ 1 .proj₁ _ .proj₂ _
∘η≡∘η→≡ :
{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₁
∘η≡∘η→≡-η : ∘η≡∘η→≡ m p (η x) ≡ p x
∘η≡∘η→≡-η =
extendable-along-η _ 2 .proj₂ _ _ .proj₁ _ .proj₂ _
◯-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 ∎
◯-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 ∎
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 □
Stable : Type a → Type a
Stable A = ◯ A → A
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
Separated : Type a → Type a
Separated = For-iterated-equality 1 Modal
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 □)
(λ _ → ∘η≡∘η→≡-η)
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
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-η
_-Connected_ : (Type a → Type a) → Type a → Type a
◯ -Connected A = Contractible (◯ A)
_-Connected-→_ :
{A B : Type a} →
(Type a → Type a) → (A → B) → Type a
◯ -Connected-→ f = ∀ y → ◯ -Connected (f ⁻¹ y)
Connected-propositional :
Extensionality a a →
(◯ : Type a → Type a) →
Is-proposition (◯ -Connected A)
Connected-propositional ext _ = H-level-propositional ext 0
Connected-→-propositional :
Extensionality a a →
(◯ : Type a → Type a) →
Is-proposition (◯ -Connected-→ f)
Connected-→-propositional ext ◯ =
Π-closure ext 1 λ _ →
Connected-propositional ext ◯
_-Connectedᴱ_ : (Type a → Type a) → Type a → Type a
◯ -Connectedᴱ A = Contractibleᴱ (◯ A)
_-Connected-→ᴱ_ :
{A B : Type a} →
(Type a → Type a) → (A → B) → Type a
◯ -Connected-→ᴱ f = ∀ y → ◯ -Connectedᴱ (f ⁻¹ᴱ y)
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-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
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
Topological : Modality a → Type (lsuc a)
Topological M =
∃ λ ((_ , P , _) : Accessible M) →
∀ i → Is-proposition (P i)
Cotopological : (Type a → Type a) → Type (lsuc a)
Cotopological {a = a} ◯ =
Left-exact ◯ ×
({A : Type a} → Is-proposition A → ◯ -Connected A → Contractible A)
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
Empty-modal : Modality a → Type a
Empty-modal M = Modal ⊥
where
open Modality-record M
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
Very-modal : Modality a → Type (lsuc a)
Very-modal {a = a} M = {A : Type a} → ◯ (Modal A)
where
open Modality-record M
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-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
module Modality (M : Modality a) where
open Modality-record M public
abstract
◯-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₁
◯-elim-η : ◯-elim m f (η x) ≡ f x
◯-elim-η {m = m} {f = f} {x = x} =
extendable-along-η m 1 .proj₁ f .proj₂ x
◯-rec : Modal B → (A → B) → (◯ A → B)
◯-rec m = ◯-elim (λ _ → m)
◯-rec-η : ◯-rec m f (η x) ≡ f x
◯-rec-η = ◯-elim-η
∘η≡∘η→≡ :
{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₁
∘η≡∘η→≡-η : ∘η≡∘η→≡ m p (η x) ≡ p x
∘η≡∘η→≡-η {m = m} {p = p} =
extendable-along-η m 2 .proj₂ _ _ .proj₁ p .proj₂ _
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 □
Stable : Type a → Type a
Stable A = ◯ A → A
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→Is-proposition→Modal :
Stable A → Is-proposition A → Modal A
Stable→Is-proposition→Modal s prop =
Stable→left-inverse→Modal s (λ _ → prop _ _)
Separated : Type a → Type a
Separated = For-iterated-equality 1 Modal
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 □)
(λ _ → ∘η≡∘η→≡-η)
Separated-◯ : Separated (◯ A)
Separated-◯ = Modal→Separated Modal-◯
η-cong : ◯ (x ≡ y) → η x ≡ η y
η-cong = ◯-rec (Separated-◯ _ _) (cong η)
η-cong-η : η-cong (η p) ≡ cong η p
η-cong-η = ◯-rec-η
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
Modal→≃◯ : Modal A → A ≃ ◯ A
Modal→≃◯ m = Eq.⟨ _ , Modal≃Is-equivalence-η _ m ⟩
Modal→Is-embedding-η :
Modal A → Is-embedding (η ⦂ (A → ◯ A))
Modal→Is-embedding-η m =
Emb.Is-equivalence→Is-embedding
(Modal≃Is-equivalence-η _ m)
η⁻¹ : Modal A → ◯ A → A
η⁻¹ m = _≃_.from (Modal→≃◯ m)
η-η⁻¹ : η (η⁻¹ m x) ≡ x
η-η⁻¹ = _≃_.right-inverse-of (Modal→≃◯ _) _
η⁻¹-η : η⁻¹ m (η x) ≡ x
η⁻¹-η = _≃_.left-inverse-of (Modal→≃◯ _) _
[◯→Modal]→Modal : (◯ A → Modal A) → Modal A
[◯→Modal]→Modal m =
Is-equivalence-η→Modal $
HA.[inhabited→Is-equivalence]→Is-equivalence $
Modal≃Is-equivalence-η _ ∘ m
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
Modal-⊤ : Modal (↑ a ⊤)
Modal-⊤ = Stable→left-inverse→Modal _ refl
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-Σ : 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 ∎))
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)
Modal-Contractible :
Extensionality a a →
Modal A → Modal (Contractible A)
Modal-Contractible ext m =
Modal-Σ m λ _ →
Modal-Π ext λ _ →
Modal→Separated m _ _
Modal-⁻¹ :
{f : A → B} →
Modal A →
Separated B →
Modal (f ⁻¹ y)
Modal-⁻¹ m s = Modal-Σ m λ _ → s _ _
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 _ _) _ _
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
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)
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) □
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) □
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 □
abstract
◯-map : (A → B) → ◯ A → ◯ B
◯-map f = ◯-rec Modal-◯ (η ∘ f)
◯-map-η : ◯-map f (η x) ≡ η (f x)
◯-map-η = ◯-rec-η
◯-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-∘ :
{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 : ◯-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-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
◯-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
◯-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
◯-cong-⇔ : A ⇔ B → ◯ A ⇔ ◯ B
◯-cong-⇔ A⇔B = record
{ to = ◯-map (_⇔_.to A⇔B)
; from = ◯-map (_⇔_.from A⇔B)
}
◯-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 ∎)
}
◯-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 ∎)
}
◯-cong-≃ : A ≃ B → ◯ A ≃ ◯ B
◯-cong-≃ = from-isomorphism ∘ ◯-cong-↔ ∘ from-isomorphism
◯-cong-≃ᴱ : A ≃ᴱ B → ◯ A ≃ᴱ ◯ B
◯-cong-≃ᴱ A≃ᴱB =
EEq.[≃]→≃ᴱ (EEq.[proofs] (◯-cong-≃ (EEq.≃ᴱ→≃ A≃ᴱB)))
mutual
◯-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
◯-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
◯-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
◯-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
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
Π◯◯≃Π◯η :
((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 ⊤) ≃ ⊤
◯-⊤ =
◯ (↑ a ⊤) ↝⟨ inverse Eq.⟨ _ , Modal≃Is-equivalence-η _ Modal-⊤ ⟩ ⟩
↑ a ⊤ ↔⟨ Bijection.↑↔ ⟩□
⊤ □
private module Abstract where abstract
◯× : ◯ (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-◯
◯×-η : _≃_.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
◯-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) □
◯-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 ∎
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 ∎
◯-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)) ∎
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-◯
◯Π→Π◯ :
{A : Type a} {P : A → Type a} →
◯ ((x : A) → P x) → ((x : A) → ◯ (P x))
◯Π→Π◯ = flip (◯-map ∘ flip _$_)
◯Π→Π◯-η :
Extensionality a a →
◯Π→Π◯ (η f) ≡ η ∘ f
◯Π→Π◯-η ext = apply-ext ext λ _ → ◯-map-η
◯Π→Π◯-◯-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
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 ∎)
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
Has-choice : Type (lsuc a)
Has-choice = {A : Type a} → Has-choice-for A
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-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-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) ∎
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
Σ-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
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
Stable-[_] : Kind → Type a → Type a
Stable-[ k ] A = ◯ A ↝[ k ] A
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 □
Modal→Stable-η : Modal→Stable m (η x) ≡ x
Modal→Stable-η = η⁻¹-η
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
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→Stable-⇔ : Stable A → Stable-[ logical-equivalence ] A
Stable→Stable-⇔ s = record { to = s; from = η }
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) □
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 ∎
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
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 □
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
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 □
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-⇔ :
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-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 □
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 □
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′ _ _)
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)) □
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 □
◯-Erased→Erased-◯ :
{@0 A : Type a} →
@0 ◯ (Erased A) → Erased (◯ A)
◯-Erased→Erased-◯ x = E.[ ◯-map E.erased x ]
Commutes-with-Erased : Type (lsuc a)
Commutes-with-Erased =
{A : Type a} →
Is-equivalence (λ (x : ◯ (Erased A)) → ◯-Erased→Erased-◯ x)
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)
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 □
Stable-Contractibleᴱ :
Modal A →
Stable (Contractibleᴱ A)
Stable-Contractibleᴱ m =
Stable-Σ m λ _ →
Stable-Erased (
Stable-Π λ _ →
Modal→Stable (Modal→Separated m _ _))
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 _ _)
abstract
◯-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) □
◯-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 ∎)
◯-rec′ : Stable B → (A → B) → (◯ A → B)
◯-rec′ s = ◯-elim′ (λ _ → s)
◯-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}
◯-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
◯-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 □
◯-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 λ _ → ◯×-η
◯-rec₂ : Modal C → (A → B → C) → (◯ A → ◯ B → C)
◯-rec₂ m f x y = ◯-rec m (uncurry f) (_≃_.from ◯× (x , y))
◯-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 ∎
raw-monad : Raw-monad ◯
Raw-monad.return raw-monad = η
Raw-monad._>>=_ raw-monad x f = ◯-rec Modal-◯ f x
instance
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)) ∎)
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 ∎)
private abstract
Modal-Σ◯◯ : Modal (Σ (◯ A) (◯ ∘ P))
Modal-Σ◯◯ = Modal-Σ Modal-◯ λ _ → 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) ∎)
Commutes-with-Σ : Type (lsuc a)
Commutes-with-Σ =
{A : Type a} {P : ◯ A → Type a} →
Is-equivalence (◯Ση≃Σ◯◯ {A = A} {P = P} _)
commutes-with-Σ :
Extensionality a a →
Commutes-with-Σ
commutes-with-Σ ext = _≃_.is-equivalence $ ◯Ση≃Σ◯◯ ext
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)
Π◯≃Πη :
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)
Π◯≃Πη-η :
∀ 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 ∎
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) □
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 ∎)
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-↠
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 _ _)
}
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 ∎
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 ≃ ◯ (◯ A)
◯≃◯◯ {A = A} = Eq.↔→≃
η
(◯-rec Modal-◯ id)
(◯-elim
(λ _ → Separated-◯ _ _)
(λ x →
η (◯-rec Modal-◯ id (η x)) ≡⟨ cong η ◯-rec-η ⟩∎
η x ∎))
(λ _ → ◯-rec-η)
◯Σ◯≃◯Σ :
{A : Type a} {P : A → Type a} →
◯ (Σ A (◯ ∘ P)) ≃ ◯ (Σ A