open import 1Lab.Prelude hiding (map) open import 1Lab.Reflection.Induction
Investigating the fact that Agda’s erasure modality is an open modality. Terminology is borrowed and some proofs are extracted from the paper Modalities in homotopy type theory by Rijke, Shulman and Spitters. The erasure modality was previously investigated in Logical properties of a modality for erasure by Danielsson.
module ErasureOpen where private variable ℓ ℓ' : Level A B : Type ℓ
The Erased monadic modality, internalising
@0:
record Erased (@0 A : Type ℓ) : Type ℓ where
constructor [_]
field
@0 erased : A
open Erased
η : {@0 A : Type ℓ} → A → Erased A
η x = [ x ]
μ : {@0 A : Type ℓ} → Erased (Erased A) → Erased A
μ [ [ x ] ] = [ x ]
…is equivalent to the open modality ○
induced by the following subsingleton:
data Compiling : Type where @0 compiling : Compiling Compiling-is-prop : is-prop Compiling Compiling-is-prop compiling compiling = refl ○_ : Type ℓ → Type ℓ ○ A = Compiling → A ○'_ : ○ Type ℓ → Type ℓ ○' A = (c : Compiling) → A c infix 30 ○_ ○'_ ○→Erased : ○ A → Erased A ○→Erased a .erased = a compiling -- Agda considers clauses that match on erased constructors as erased. Erased→○ : Erased A → ○ A Erased→○ a compiling = a .erased ○≃Erased : ○ A ≃ Erased A ○≃Erased = Iso→Equiv (○→Erased , iso Erased→○ (λ _ → refl) (λ _ → funext λ where compiling → refl)) η○ : A → ○ A η○ a _ = a
Since Agda allows erased matches for the empty type, the empty type
is modal; in other words, we are not not Compiling.
¬¬compiling : ¬ ¬ Compiling ¬¬compiling ¬c with ○→Erased ¬c ... | ()
The corresponding closed modality ● is
given by the join with Compiling, which is equivalent to
the following higher inductive type.
data ●_ (A : Type ℓ) : Type ℓ where
-- At runtime, we only have A.
η● : A → ● A
-- At compile time, we also have an erased "cone" that glues all of A together,
-- so that ● A is contractible.
@0 tip : ● A
@0 cone : (a : A) → η● a ≡ tip
infix 30 ●_
unquoteDecl ●-elim = make-elim ●-elim (quote ●_)
@0 ●-contr : is-contr (● A)
●-contr {A = A} = contr tip λ a → sym (ps a) where
ps : (a : ● A) → a ≡ tip
ps = ●-elim cone refl λ a i j → cone a (i ∨ j)
The rest of this file investigates some properties of open and closed
modalities that are not specific to the Compiling
proposition we use here.
module Modality
{○_ : ∀ {ℓ} → Type ℓ → Type ℓ}
(η○ : ∀ {ℓ} {A : Type ℓ} → A → ○ A)
(○-elim : ∀ {ℓ ℓ'} {A : Type ℓ} {P : ○ A → Type ℓ'}
→ ((a : A) → ○ P (η○ a)) → (a : ○ A) → ○ P a)
(○-elim-β : ∀ {ℓ ℓ'} {A : Type ℓ} {P : ○ A → Type ℓ'} {pη : (a : A) → ○ P (η○ a)}
→ (a : A) → ○-elim {P = P} pη (η○ a) ≡ pη a)
(○-≡-modal : ∀ {ℓ} {A : Type ℓ} {x y : ○ A} → is-equiv (η○ {A = x ≡ y}))
where
modal : Type ℓ → Type ℓ
modal A = is-equiv (η○ {A = A})
modal-map : (A → B) → Type _
modal-map {B = B} f = (b : B) → modal (fibre f b)
connected : Type ℓ → Type ℓ
connected A = is-contr (○ A)
connected-map : (A → B) → Type _
connected-map {B = B} f = (b : B) → connected (fibre f b)
modal+connected→contr : modal A → connected A → is-contr A
modal+connected→contr A-mod A-conn = Equiv→is-hlevel 0 (η○ , A-mod) A-conn
modal+connected→equiv : {f : A → B} → modal-map f → connected-map f → is-equiv f
modal+connected→equiv f-mod f-conn .is-eqv b = modal+connected→contr (f-mod b) (f-conn b)
elim-modal
: ∀ {ℓ ℓ'} {A : Type ℓ} {P : ○ A → Type ℓ'}
→ (∀ a → modal (P a))
→ ((a : A) → P (η○ a)) → (a : ○ A) → P a
elim-modal P-modal pη a = equiv→inverse (P-modal a) (○-elim (λ a → η○ (pη a)) a)
elim-modal-β
: ∀ {ℓ ℓ'} {A : Type ℓ} {P : ○ A → Type ℓ'} P-modal {pη : (a : A) → P (η○ a)}
→ (a : A) → elim-modal {P = P} P-modal pη (η○ a) ≡ pη a
elim-modal-β P-modal {pη} a =
ap (equiv→inverse (P-modal (η○ a))) (○-elim-β a)
∙ equiv→unit (P-modal (η○ a)) (pη a)
map : (A → B) → ○ A → ○ B
map f = ○-elim (η○ ∘ f)
map-≃ : A ≃ B → (○ A) ≃ (○ B)
map-≃ e = map (e .fst) , is-iso→is-equiv λ where
.is-iso.inv → map (Equiv.from e)
.is-iso.rinv → elim-modal (λ _ → ○-≡-modal) λ b →
ap (map (e .fst)) (○-elim-β b) ∙ ○-elim-β (Equiv.from e b) ∙ ap η○ (Equiv.ε e b)
.is-iso.linv → elim-modal (λ _ → ○-≡-modal) λ a →
ap (map (Equiv.from e)) (○-elim-β a) ∙ ○-elim-β (e .fst a) ∙ ap η○ (Equiv.η e a)
retract-○→modal : (η⁻¹ : ○ A → A) → is-left-inverse η⁻¹ η○ → modal A
retract-○→modal η⁻¹ ret = is-iso→is-equiv $
iso η⁻¹ (elim-modal (λ _ → ○-≡-modal) λ a → ap η○ (ret a)) ret
retract→modal
: (f : A → B) (g : B → A)
→ is-left-inverse f g → modal A → modal B
retract→modal {B = B} f g ret A-modal = retract-○→modal η⁻¹ linv where
η⁻¹ : ○ B → B
η⁻¹ = f ∘ elim-modal (λ _ → A-modal) g
linv : is-left-inverse η⁻¹ η○
linv b = ap f (elim-modal-β (λ _ → A-modal) b) ∙ ret b
modal-≃ : B ≃ A → modal A → modal B
modal-≃ e = retract→modal (Equiv.from e) (Equiv.to e) (Equiv.η e)
connected-≃ : B ≃ A → connected A → connected B
connected-≃ e A-conn = Equiv→is-hlevel 0 (map-≃ e) A-conn
≡-modal : modal A → ∀ {x y : A} → modal (x ≡ y)
≡-modal A-modal = modal-≃ (ap-equiv (η○ , A-modal)) ○-≡-modal
PathP-modal : {A : I → Type ℓ} → modal (A i0) → ∀ {x y} → modal (PathP A x y)
PathP-modal {A = A} A-modal {x} {y} = subst modal (sym (PathP≡Path⁻ A x y)) (≡-modal A-modal)
reflection-modal : modal (○ A)
reflection-modal = is-iso→is-equiv λ where
.is-iso.inv → ○-elim id
.is-iso.rinv → elim-modal (λ _ → ○-≡-modal) λ a → ap η○ (○-elim-β a)
.is-iso.linv → ○-elim-β
Π-modal : {B : A → Type ℓ} → (∀ a → modal (B a)) → modal ((a : A) → B a)
Π-modal B-modal = retract-○→modal
(λ f a → elim-modal (λ _ → B-modal _) (_$ a) f)
(λ f → funext λ a → elim-modal-β (λ _ → B-modal _) f)
Σ-modal : {B : A → Type ℓ} → modal A → (∀ a → modal (B a)) → modal (Σ A B)
Σ-modal {B = B} A-modal B-modal = retract-○→modal
(Equiv.from Σ-Π-distrib
( elim-modal (λ _ → A-modal) fst
, elim-modal (λ _ → B-modal _) λ (a , b) →
subst B (sym (elim-modal-β (λ _ → A-modal) (a , b))) b))
λ (a , b) →
elim-modal-β (λ _ → A-modal) (a , b)
,ₚ elim-modal-β (λ _ → B-modal _) (a , b) ◁ to-pathp⁻ refl
η-connected : connected-map (η○ {A = A})
η-connected a = contr
(○-elim {P = fibre η○} (λ a → η○ (a , refl)) a)
(elim-modal (λ _ → ○-≡-modal) λ (a' , p) →
J (λ a p → ○-elim (λ x → η○ (x , refl)) a ≡ η○ (a' , p)) (○-elim-β a') p)
○Σ○≃○Σ : {B : A → Type ℓ} → (○ (Σ A λ a → ○ B a)) ≃ (○ (Σ A B))
○Σ○≃○Σ .fst = ○-elim λ (a , b) → map (a ,_) b
○Σ○≃○Σ .snd = is-iso→is-equiv λ where
.is-iso.inv → map (Σ-map₂ η○)
.is-iso.rinv → elim-modal (λ _ → ○-≡-modal) λ (a , b) →
ap (○-elim _) (○-elim-β (a , b)) ∙ ○-elim-β (a , η○ b) ∙ ○-elim-β b
.is-iso.linv → elim-modal (λ _ → ○-≡-modal) λ (a , b) →
ap (map _) (○-elim-β (a , b)) ∙ elim-modal
{P = λ b → ○-elim _ (○-elim _ b) ≡ η○ (a , b)} (λ _ → ○-≡-modal)
(λ b → ap (○-elim _) (○-elim-β b) ∙ ○-elim-β (a , b)) b
Σ-connected : {B : A → Type ℓ} → connected A → (∀ a → connected (B a)) → connected (Σ A B)
Σ-connected A-conn B-conn = Equiv→is-hlevel 0 (○Σ○≃○Σ e⁻¹)
(connected-≃ (Σ-contract B-conn) A-conn)
-- Additional properties of *lex* modalities
module _ (○-lex : ∀ {ℓ} {A : Type ℓ} {a b : A} → (○ (a ≡ b)) ≃ (η○ a ≡ η○ b)) where
≡-connected : connected A → {x y : A} → connected (x ≡ y)
≡-connected A-conn = Equiv→is-hlevel 0 ○-lex (Path-is-hlevel 0 A-conn)
PathP-connected : {A : I → Type ℓ} → connected (A i0) → ∀ {x y} → connected (PathP A x y)
PathP-connected {A = A} A-conn {x} {y} =
subst connected (sym (PathP≡Path⁻ A x y)) (≡-connected A-conn)
○ and ● are higher modalities, so we can
instantiate this module for both of them.
○-elim-○
: ∀ {ℓ ℓ'} {A : Type ℓ} {P : ○ A → Type ℓ'}
→ ((a : A) → ○ P (η○ a)) → (a : ○ A) → ○ P a
○-elim-○ {P = P} pη a c =
subst P (funext λ _ → ap a (Compiling-is-prop _ _)) (pη (a c) c)
○-≡-modal : {x y : ○ A} → is-equiv (η○ {A = x ≡ y})
○-≡-modal = is-iso→is-equiv λ where
.is-iso.inv p i compiling → p compiling i compiling
.is-iso.rinv p i compiling j compiling → p compiling j compiling
.is-iso.linv p i j compiling → p j compiling
●-elim-●
: ∀ {ℓ ℓ'} {A : Type ℓ} {P : ● A → Type ℓ'}
→ ((a : A) → ● P (η● a)) → (a : ● A) → ● P a
●-elim-● pη = ●-elim pη tip λ _ → is-contr→pathp (λ _ → ●-contr) _ _
●-≡-modal : {x y : ● A} → is-equiv (η● {A = x ≡ y})
●-≡-modal = is-iso→is-equiv λ where
.is-iso.inv → ●-elim id (is-contr→is-prop ●-contr _ _)
λ p → is-contr→is-set ●-contr _ _ _ _
.is-iso.rinv → ●-elim (λ _ → refl) (sym (●-contr .paths _))
λ p → is-set→squarep (λ _ _ → is-contr→is-set ●-contr) _ _ _ _
.is-iso.linv _ → refl
module ○ = Modality η○ ○-elim-○ (λ _ → funext λ _ → transport-refl _) ○-≡-modal
module ● = Modality η● ●-elim-● (λ _ → refl) ●-≡-modal
Open and closed modalities are lex.
○-lex : {a b : A} → ○ (a ≡ b) ≃ (η○ a ≡ η○ b)
○-lex = funext≃
module ●-ids {A : Type ℓ} {a : A} where
code : ● A → Type ℓ
code = ●-elim (λ b → ● (a ≡ b)) (Lift _ ⊤) (λ b → ua (is-contr→≃ ●-contr (hlevel 0)))
code-refl : code (η● a)
code-refl = η● refl
decode : ∀ b → code b → η● a ≡ b
decode = ●.elim-modal (λ _ → ●.Π-modal λ _ → ●-≡-modal)
λ a → ●.elim-modal (λ _ → ●-≡-modal) (ap η●)
decode-over : ∀ b (c : code b) → PathP (λ i → code (decode b c i)) code-refl c
decode-over = ●.elim-modal (λ _ → ●.Π-modal λ _ → ●.PathP-modal ●.reflection-modal)
λ a → ●.elim-modal (λ _ → ●.PathP-modal ●.reflection-modal)
λ p i → η● λ j → p (i ∧ j)
ids : is-based-identity-system (η● a) code code-refl
ids .to-path {b} = decode b
ids .to-path-over {b} = decode-over b
●-lex : {a b : A} → ● (a ≡ b) ≃ (η● a ≡ η● b)
●-lex = based-identity-system-gives-path ●-ids.ids
Some equivalences specific to open and closed modalities:
●-modal A ≃ ○ (is-contr A) ≃ is-contr (○ A) = ○-connected A
@0 ●-modal→contr : ●.modal A → is-contr A ●-modal→contr A-modal = Equiv→is-hlevel 0 (η● , A-modal) ●-contr contr→●-modal : @0 is-contr A → ●.modal A contr→●-modal A-contr = ●.retract-○→modal (●-elim id (A-contr .centre) λ a → sym (A-contr .paths a)) λ _ → refl contr→○-connected : @0 is-contr A → ○.connected A contr→○-connected A-contr = contr (Erased→○ [ A-contr .centre ]) λ a → funext λ where compiling → A-contr .paths _ @0 ○-connected→contr : ○.connected A → is-contr A ○-connected→contr A-conn = contr (A-conn .centre compiling) λ a → A-conn .paths (η○ a) $ₚ compiling ○-connected→●-modal : ○.connected A → ●.modal A ○-connected→●-modal A-conn = contr→●-modal (○-connected→contr A-conn)
We prove an Artin gluing theorem: every type
A is equivalent to a certain pullback of ○ A
and ● A over ● ○ A, which we call
Fracture A. Handwaving, this corresponds to decomposing a
type into its “compile time” part and its “runtime” part.
○→●○ : ○ A → ● ○ A
○→●○ = η●
●→●○ : ● A → ● ○ A
●→●○ = ●.map η○
Fracture : Type ℓ → Type ℓ
Fracture A = Σ (○ A × ● A) λ (o , c) → ○→●○ o ≡ ●→●○ c
module _ {A : Type ℓ} where
fracture : A → Fracture A
fracture a = (η○ a , η● a) , refl
The idea is to prove that the fibres of the fracture map
are both ●-modal and ●-connected, and hence
contractible.
For the modal part, we observe that an element of the fibre of
fracture at a triple (o : ○ A, c : ● A, p) can
be rearranged into an element of the fibre of η○ at
o (which is ○-connected, hence
●-modal) together with a dependent path whose type is
●-modal by standard results about higher modalities.
fracture-modal : ●.modal-map fracture
fracture-modal ((o , c) , p) = ●.modal-≃ e $
●.Σ-modal (○-connected→●-modal (○.η-connected _)) λ _ →
●.PathP-modal $ ●.Σ-modal ●.reflection-modal λ _ → ●-≡-modal
where
e : fibre fracture ((o , c) , p)
≃ Σ (fibre η○ o) λ (a , q) →
PathP (λ i → Σ (● A) λ c → ○→●○ (q i) ≡ ●→●○ c) (η● a , refl) (c , p)
e = Σ-ap-snd (λ _ → ap-equiv (Σ-assoc e⁻¹) ∙e Iso→Equiv Σ-pathp-iso e⁻¹) ∙e Σ-assoc
Almost symmetrically, for the connected part, we rearrange the fibre
into an element of the fibre of η● at c (which
is ●-connected) together with a dependent path in the
fibres of ○→●○. Since the latter is defined as
η● its fibres are ●-connected as well, hence
the path type is ●-connected because ● is
lex.
fracture-connected : ●.connected-map fracture
fracture-connected ((o , c) , p) = ●.connected-≃ e $
●.Σ-connected (●.η-connected _) λ _ →
●.PathP-connected ●-lex (●.η-connected _)
where
e : fibre fracture ((o , c) , p)
≃ Σ (fibre η● c) λ (a , q) →
PathP (λ i → Σ (○ A) λ o → ○→●○ o ≡ ●→●○ (q i)) (η○ a , refl) (o , p)
e = Σ-ap-snd (λ _ → ap-equiv (Σ-ap-fst ×-swap ∙e Σ-assoc e⁻¹) ∙e Iso→Equiv Σ-pathp-iso e⁻¹) ∙e Σ-assoc
fracture-is-equiv : is-equiv fracture
fracture-is-equiv = ●.modal+connected→equiv fracture-modal fracture-connected
Artin-gluing : A ≃ Fracture A
Artin-gluing = fracture , fracture-is-equiv