{-# OPTIONS --safe --cubical-compatible --erased-matches #-}
open import Equality
import Modality.Basics
module Modality.Erased-matches
{c⁺}
(eq : ∀ {a p} → Equality-with-J a p c⁺)
(open Modality.Basics eq)
{a}
(M : Modality a)
where
open Derived-definitions-and-properties eq
open Modality M hiding (◯Wη→W◯; ◯Wη→W◯-η; Stable-W)
import Modality.Has-choice
open import Prelude
open import Accessibility eq as A using (Acc; _<W_)
import Accessibility.Erased-matches eq as AE
open import Equivalence eq as Eq using (_≃_)
open import Erased.Box-cong-axiomatisation eq
using ([]-cong-axiomatisation)
import Erased.Level-1 eq as E
open import Extensionality eq
open import Function-universe eq hiding (id; _∘_)
private variable
ℓ : Level
A : Type ℓ
P : A → Type ℓ
k x : A
Accessibility-modal-for-erasure-stable :
{@0 A : Type a} {@0 _<_ : A → A → Type a} →
E.Stable (Accessibility-modal-for _<_)
Accessibility-modal-for-erasure-stable E.[ acc₁ , acc₂ ] =
(λ acc → AE.Acc-erasure-stable E.[ acc₁ acc ])
, (λ acc → AE.Acc-erasure-stable E.[ acc₂ acc ])
Accessibility-modal-erasure-stable :
E.Stable Accessibility-modal
Accessibility-modal-erasure-stable E.[ acc ] =
Accessibility-modal-for-erasure-stable E.[ acc ]
private
◯Wη→W◯-Acc :
@0 Extensionality a a →
(x : ◯ (W A (P ∘ η))) →
@0 Acc _[ _<W_ ]◯_ x →
W (◯ A) P
◯Wη→W◯-Acc {P} ext w (A.acc a) =
sup x′ λ y → ◯Wη→W◯-Acc ext (f′ y) (a (f′ y) (f′<w y))
where
p′ = ◯Wη→Σ◯Π◯Wη {P = P} w
x′ = p′ .proj₁
f′ = p′ .proj₂
@0 f′<w : ∀ y → f′ y [ _<W_ ]◯ w
f′<w =
◯-elim′
{P = λ w →
let (x′ , f′) = ◯Wη→Σ◯Π◯Wη {P = P} w in
∀ y → f′ y [ _<W_ ]◯ w}
(λ _ → Stable-Π λ _ → Modal→Stable Modal-◯)
(λ @0 where
w@(sup x f) y →
let x′ , f′ = ◯Wη→Σ◯Π◯Wη (η w)
@0 lemma : (x′ , f′) ≡ (η x , η ∘ f)
lemma = ◯Wη→Σ◯Π◯Wη-η ext
in
η ( f (subst (P ∘ proj₁) lemma y)
, w
, (f′ y ≡⟨ elim₁
(λ {(x′ , f′)} eq →
(y : P x′) → f′ y ≡ η (f (subst (P ∘ proj₁) eq y)))
(λ _ → cong (η ∘ f) $ sym $ subst-refl _ _)
lemma y ⟩∎
η (f (subst (P ∘ proj₁) lemma y)) ∎)
, (η w ∎)
, (_ , refl _)
))
w
◯Wη→W◯-Acc-η :
(@0 ext : Extensionality a a) →
Extensionality a a →
[]-cong-axiomatisation a →
(x : W A (P ∘ η))
(@0 acc : Acc _[ _<W_ ]◯_ (η x)) →
◯Wη→W◯-Acc {P = P} ext (η x) acc ≡ W-map η id x
◯Wη→W◯-Acc-η {A} {P} ext ext′ ax (sup x f) (A.acc acc) =
cong (uncurry sup) $
Σ-≡,≡→≡
(cong proj₁ lemma)
(apply-ext ext′ λ y →
let @0 acc₁ : ∀ y → Acc _[ _<W_ ]◯_ (p′ .proj₂ y)
acc₁ = _
in
subst (λ y → P y → W (◯ A) P)
(cong proj₁ lemma)
(λ y → ◯Wη→W◯-Acc ext (p′ .proj₂ y) (acc₁ y))
y
≡⟨ elim₁
(λ {(x′ , f′)} lemma →
(y : P (η x))
(@0 acc₁ : (y : P x′) → Acc _[ _<W_ ]◯_ (f′ y)) →
subst (λ y → P y → W (◯ A) P)
(cong proj₁ lemma)
(λ y → ◯Wη→W◯-Acc ext (f′ y) (acc₁ y))
y ≡
◯Wη→W◯-Acc ext (η (f y)) (acc₂ y))
(λ y (@0 acc₁) →
subst (λ y → P y → W (◯ A) P)
(cong proj₁ (refl _))
(λ y → ◯Wη→W◯-Acc ext (η (f y)) (acc₁ y))
y ≡⟨ cong (_$ y) $ cong (flip (subst (λ y → P y → W (◯ A) P)) _) $
cong-refl _ ⟩
subst (λ y → P y → W (◯ A) P)
(refl _)
(λ y → ◯Wη→W◯-Acc ext (η (f y)) (acc₁ y))
y ≡⟨ cong (_$ y) $ subst-refl _ _ ⟩
◯Wη→W◯-Acc ext (η (f y)) (acc₁ y) ≡⟨ cong (λ acc → ◯Wη→W◯-Acc ext (η (f y)) (E.erased acc)) $
[]-cong-axiomatisation.[]-cong ax E.[ A.Acc-propositional ext _ _ ] ⟩∎
◯Wη→W◯-Acc ext (η (f y)) (acc₂ y) ∎)
lemma y acc₁ ⟩
◯Wη→W◯-Acc ext (η (f y)) (acc₂ y) ≡⟨ ◯Wη→W◯-Acc-η ext ext′ ax (f y) (acc₂ y) ⟩∎
W-map η id (f y) ∎)
where
p′ = ◯Wη→Σ◯Π◯Wη {P = P} (η (sup x f))
lemma : p′ ≡ (η x , η ∘ f)
lemma = ◯Wη→Σ◯Π◯Wη-η ext′
@0 acc₂ : ∀ y → Acc _[ _<W_ ]◯_ (η (f y))
acc₂ y =
acc (η (f y)) (η (_ , _ , refl _ , refl _ , _ , refl _))
◯Wη→W◯ :
{P : ◯ A → Type a} →
@0 Accessibility-modal-for (_<W_ {A = A} {P = P ∘ η}) →
@0 Extensionality a a →
◯ (W A (P ∘ η)) → W (◯ A) P
◯Wη→W◯ {A} {P} acc ext =
◯ (W A (P ∘ η)) →⟨ ◯-map (λ x → x , A.Well-founded-W x) ⟩
◯ (∃ λ (x : W A (P ∘ η)) → Acc _<W_ x) →⟨ ◯-map (Σ-map id (acc′ .proj₁)) ⟩
◯ (∃ λ (x : W A (P ∘ η)) → Acc _[ _<W_ ]◯_ (η x)) →⟨ ◯Ση≃Σ◯◯ _ ⟩
(∃ λ (x : ◯ (W A (P ∘ η))) → ◯ (Acc _[ _<W_ ]◯_ x)) →⟨ Σ-map id (acc′ .proj₂) ⟩
(∃ λ (x : ◯ (W A (P ∘ η))) → Acc _[ _<W_ ]◯_ x) →⟨ (λ (x , a) → ◯Wη→W◯-Acc ext x a) ⟩□
W (◯ A) P □
where
acc′ = Accessibility-modal-for-erasure-stable E.[ acc ]
◯Wη→W◯-η :
{x : W A (P ∘ η)}
(@0 acc : Accessibility-modal-for _<W_)
(@0 ext : Extensionality a a) →
Extensionality a a →
[]-cong-axiomatisation a →
◯Wη→W◯ {P = P} acc ext (η x) ≡ W-map η id x
◯Wη→W◯-η {A} {P} {x} acc ext ext′ ax =
(λ (x , a) → ◯Wη→W◯-Acc ext x (acc′ .proj₂ a))
(◯Ση≃Σ◯◯ _
(◯-map (Σ-map id (acc′ .proj₁))
(◯-map (λ x → x , A.Well-founded-W x) (η x)))) ≡⟨ cong (λ (x , a) → ◯Wη→W◯-Acc ext x (acc′ .proj₂ a)) $
trans (cong (◯Ση≃Σ◯◯ _) $
trans (cong (◯-map _) ◯-map-η)
◯-map-η)
◯-rec-η ⟩
(λ (x , a) → ◯Wη→W◯-Acc ext x (acc′ .proj₂ a))
(η x , η (acc′ .proj₁ (A.Well-founded-W x))) ≡⟨⟩
◯Wη→W◯-Acc ext (η x)
(acc′ .proj₂ (η (acc′ .proj₁ (A.Well-founded-W x)))) ≡⟨ ◯Wη→W◯-Acc-η ext ext′ ax _ _ ⟩∎
W-map η id x ∎
where
acc′ = Accessibility-modal-for-erasure-stable E.[ acc ]
Stable-W :
@0 Accessibility-modal-for (_<W_ {A = A} {P = P}) →
@0 Extensionality a a →
Modal A →
Stable (W A P)
Stable-W {A} {P} acc ext m =
◯ (W A P) →⟨ ◯-map $ W-map id (subst P Modal→Stable-η) ⟩
◯ (W A (P ∘ Modal→Stable m ∘ η)) →⟨ ◯Wη→W◯ acc′ ext ⟩
W (◯ A) (P ∘ Modal→Stable m) →⟨ W-map (Modal→Stable m) id ⟩□
W A P □
where
@0 acc′ :
Accessibility-modal-for
(_<W_ {A = A} {P = P ∘ Modal→Stable m ∘ η})
acc′ =
subst
(λ f → Accessibility-modal-for (_<W_ {A = A} {P = P ∘ f}))
(apply-ext ext λ _ → sym Modal→Stable-η)
acc
module Has-choice
(Valid-domain : Type a → Type a)
(has-choice :
{A : Type a} →
Valid-domain A → Modality.Has-choice-for M A)
where
private
open module H = Modality.Has-choice eq M Valid-domain has-choice
hiding (module Valid-domain-Π◯;
module Valid-domain-Π;
module Valid-domain)
module Valid-domain-Π◯
(P : ◯ A → Type a)
(v : ∀ x → Valid-domain (P x))
where
private
open module V₁ {x} = Valid-domain₁ (v x)
open H.Valid-domain-Π◯ _ v hiding (◯Wη≃W◯)
◯Wη≃W◯ :
@0 Accessibility-modal-for (_<W_ {A = A} {P = P ∘ η}) →
@0 Extensionality a a →
◯ (W A (P ∘ η)) ↝[ a ∣ a ] W (◯ A) P
◯Wη≃W◯ acc ext =
generalise-ext?
(record { to = ◯Wη→W◯ acc ext; from = W◯→◯Wη })
(λ ext′ → to-from ext′ , from-to ext′)
where
module _ (ext′ : Extensionality a a) where
ax = E.Extensionality→[]-cong-axiomatisation ext′
from-to : ∀ x → W◯→◯Wη (◯Wη→W◯ acc ext x) ≡ x
from-to =
◯-elim
(λ _ → Separated-◯ _ _)
(λ x →
W◯→◯Wη (◯Wη→W◯ acc ext (η x)) ≡⟨ cong W◯→◯Wη $
◯Wη→W◯-η acc ext ext′ ax ⟩
W◯→◯Wη (W-map η id x) ≡⟨ W◯→◯Wη-W-map-η-id ext′ ⟩∎
η x ∎)
to-from : ∀ x → ◯Wη→W◯ acc ext (W◯→◯Wη x) ≡ x
to-from (sup x f) =
◯-elim
{P = λ x →
∀ f →
(∀ y → ◯Wη→W◯ acc ext (W◯→◯Wη (f y)) ≡ f y) →
◯Wη→W◯ acc ext (W◯→◯Wη (sup x f)) ≡
sup x f}
(λ _ → Modal-Π ext′ λ _ →
Modal-Π ext′ λ _ →
Separated-W ext′ Separated-◯ _ _)
(λ x f hyp →
◯Wη→W◯ acc ext (W◯→◯Wη (sup (η x) f)) ≡⟨ cong (◯Wη→W◯ acc ext) $ W◯→◯Wη-sup-η ext′ f ⟩
◯Wη→W◯ acc ext (◯-map (sup x) (Π◯→◯Π (W◯→◯Wη ∘ f))) ≡⟨ ◯-elim
{P = λ f′ →
◯Wη→W◯ acc ext (◯-map (sup x) f′) ≡
sup (η x) (◯Wη→W◯ acc ext ∘ ◯Π→Π◯ f′)}
(λ _ → Separated-W ext′ Separated-◯ _ _)
(λ f′ →
◯Wη→W◯ acc ext (◯-map (sup x) (η f′)) ≡⟨ cong (◯Wη→W◯ acc ext)
◯-map-η ⟩
◯Wη→W◯ acc ext (η (sup x f′)) ≡⟨ ◯Wη→W◯-η acc ext ext′ ax ⟩
W-map η id (sup x f′) ≡⟨⟩
sup (η x) (W-map η id ∘ f′) ≡⟨ (cong (sup _) $ sym $ apply-ext ext′ λ _ →
◯Wη→W◯-η acc ext ext′ ax) ⟩
sup (η x) (◯Wη→W◯ acc ext ∘ η ∘ f′) ≡⟨ cong (sup _ ∘ (◯Wη→W◯ acc ext ∘_)) $ sym $
◯Π→Π◯-η ext′ ⟩∎
sup (η x) (◯Wη→W◯ acc ext ∘ ◯Π→Π◯ (η f′)) ∎)
_ ⟩
sup (η x) (◯Wη→W◯ acc ext ∘ ◯Π→Π◯ (Π◯→◯Π (W◯→◯Wη ∘ f))) ≡⟨ cong (sup _ ∘ (◯Wη→W◯ acc ext ∘_)) $
_≃_.left-inverse-of (Π◯≃◯Π ext′) _ ⟩
sup (η x) (◯Wη→W◯ acc ext ∘ W◯→◯Wη ∘ f) ≡⟨ cong (sup (η x)) $ apply-ext ext′
hyp ⟩∎
sup (η x) f ∎)
x f (λ y → to-from (f y))
module Valid-domain-Π
{A : Type a} {P : A → Type a}
(v : ∀ x → Valid-domain (P x))
where
Stable-[]-W :
@0 Accessibility-modal-for (_<W_ {A = A} {P = P}) →
@0 Extensionality a a →
Extensionality? ⌊ k ⌋-sym a a →
Modal A →
Stable-[ ⌊ k ⌋-sym ] (W A P)
Stable-[]-W acc ext ext′ m =
◯ (W A P) ↝⟨ (◯-cong-↝-sym ext′ λ ext → W-cong₂ ext λ _ → ≡⇒↝ _ $ cong P $ sym
Modal→Stable-η) ⟩
◯ (W A (P ∘ Modal→Stable m ∘ η)) ↝⟨ Valid-domain-Π◯.◯Wη≃W◯ _ (λ _ → v _) acc′ ext ext′ ⟩
W (◯ A) (P ∘ Modal→Stable m) ↝⟨ (inverse $ W-cong ext′ (Modal→≃◯ m) λ _ → ≡⇒↝ _ $ cong P $ sym
Modal→Stable-η) ⟩□
W A P □
where
@0 acc′ :
Accessibility-modal-for
(_<W_ {A = A} {P = P ∘ Modal→Stable m ∘ η})
acc′ =
subst
(λ f → Accessibility-modal-for (_<W_ {A = A} {P = P ∘ f}))
(apply-ext ext λ _ → sym Modal→Stable-η)
acc
Modal-W :
@0 Accessibility-modal-for (_<W_ {A = A} {P = P}) →
Extensionality a a →
Modal A →
Modal (W A P)
Modal-W acc ext m =
Is-equivalence-η→Modal $
_≃_.is-equivalence $
Eq.with-other-function
(inverse $ Stable-[]-W acc ext ext m)
η
lemma
where
P≃ : P x ≃ P (Modal→Stable m (η x))
P≃ = ≡⇒↝ _ $ cong P $ sym Modal→Stable-η
P→ : P x → P (Modal→Stable m (η x))
P→ = _≃_.to P≃
P← : P (Modal→Stable m (η x)) → P x
P← = _≃_.from P≃
open module V₁ {x} = Valid-domain₁ (v x)
open H.Valid-domain-Π◯ (P ∘ Modal→Stable m) (λ _ → v _)
lemma : ∀ x → ◯-map (W-map id P→) (W◯→◯Wη (W-map η P← x)) ≡ η x
lemma (sup x f) =
◯-map (W-map id P→) (W◯→◯Wη $ W-map η P← (sup x f)) ≡⟨⟩
◯-map (W-map id P→) (W◯→◯Wη $ sup (η x) (W-map η P← ∘ f ∘ P←)) ≡⟨ cong (◯-map _) $
W◯→◯Wη-sup-η ext (W-map η P← ∘ f ∘ P←) ⟩
◯-map (W-map id P→)
(◯-map (sup x) (Π◯→◯Π (W◯→◯Wη ∘ W-map η P← ∘ f ∘ P←))) ≡⟨ sym ◯-map-∘ ⟩
◯-map (sup x ∘ (_∘ P→) ∘ (W-map id P→ ∘_))
(Π◯→◯Π (W◯→◯Wη ∘ W-map η P← ∘ f ∘ P←)) ≡⟨ ◯-map-∘ ⟩
◯-map (sup x ∘ (_∘ P→))
(◯-map (W-map id P→ ∘_) (Π◯→◯Π (W◯→◯Wη ∘ W-map η P← ∘ f ∘ P←))) ≡⟨ cong (◯-map _) $ sym $
Π◯→◯Π-◯-map ext ⟩
◯-map (sup x ∘ (_∘ P→))
(Π◯→◯Π (◯-map (W-map id P→) ∘ W◯→◯Wη ∘ W-map η P← ∘ f ∘ P←)) ≡⟨ (cong (◯-map (sup x ∘ (_∘ P→))) $ cong Π◯→◯Π $
apply-ext ext λ y →
lemma (f (P← y))) ⟩
◯-map (sup x ∘ (_∘ P→)) (Π◯→◯Π (η ∘ f ∘ P←)) ≡⟨ cong (◯-map (sup x ∘ (_∘ P→))) $ cong Π◯→◯Π $ sym $
◯Π→Π◯-η ext ⟩
◯-map (sup x ∘ (_∘ P→)) (Π◯→◯Π (◯Π→Π◯ (η (f ∘ P←)))) ≡⟨ cong (◯-map (sup x ∘ (_∘ P→))) $
_≃_.right-inverse-of (Π◯≃◯Π ext) _ ⟩
◯-map (sup x ∘ (_∘ P→)) (η (f ∘ P←)) ≡⟨ ◯-map-η ⟩
η (sup x (f ∘ P← ∘ P→)) ≡⟨ (cong (η ∘ sup x) $ cong (f ∘_) $ apply-ext ext λ _ →
_≃_.left-inverse-of P≃ _) ⟩∎
η (sup x f) ∎
module Valid-domain (v : {A : Type a} → Valid-domain A) where
private
open module V₁ {A P} = Valid-domain-Π◯ {A = A} P (λ _ → v) public
open module V₂ {A P} = Valid-domain-Π {A = A} {P = P} (λ _ → v)
public