------------------------------------------------------------------------
-- Code related to the paper "Compiling Programs with Erased
-- Univalence"
--
-- Nils Anders Danielsson
--
-- The paper is coauthored with Andreas Abel and Andrea Vezzosi.
------------------------------------------------------------------------
-- Note that this version of the code contains some changes that were
-- made after the paper was written. In particular, now the variant of
-- Agda that is activated using --erased-cubical supports higher
-- inductive types with non-erased higher constructors.
-- Most of the code referenced below can be found in modules that are
-- parametrised by a notion of equality. One can use them both with
-- Cubical Agda paths and with the Cubical Agda identity type family.
-- Note that the code does not follow the paper exactly. For instance,
-- some definitions use bijections (functions with quasi-inverses)
-- instead of equivalences. Some code that is not defined in Cubical
-- Agda is parametrised by assumptions of univalence and/or function
-- extensionality. Some other differences are mentioned below.
-- Note that there is a known problem with guarded corecursion in
-- Agda. Due to "quantifier inversion" (see "Termination Checking in
-- the Presence of Nested Inductive and Coinductive Types" by Thorsten
-- Altenkirch and myself) certain types may not have the expected
-- semantics when the option --guardedness is used. I expect that the
-- results would still hold if this bug were fixed, but because I do
-- not know what the rules of a fixed version of Agda would be I do
-- not know if any changes to the code would be required.
{-# OPTIONS --guardedness #-}
module README.Compiling-Programs-with-Erased-Univalence where
import Coherently-constant
import Colimit.Sequential
import Colimit.Sequential.Very-erased
import Equality.Path
import Equality.Path.Univalence
import Equivalence
import Equivalence.Erased
import Equivalence.Erased.Basics
import Equivalence.Erased.Contractible-preimages
import Equivalence.Half-adjoint
import Erased.Basics
import Erased.Cubical
import Erased.Level-1
import Erased.Stability
import H-level.Truncation.Propositional
import H-level.Truncation.Propositional.Erased
import H-level.Truncation.Propositional.Non-recursive
import H-level.Truncation.Propositional.Non-recursive.Erased
import H-level.Truncation.Propositional.One-step
import Preimage
import Univalence-axiom
import Lens.Non-dependent.Higher
import Lens.Non-dependent.Higher.Erased
import Lens.Non-dependent.Higher.Capriotti.Variant.Erased.Variant
import Lens.Non-dependent.Higher.Coinductive
import Lens.Non-dependent.Higher.Coinductive.Erased
import Lens.Non-dependent.Higher.Coinductive.Small
import Lens.Non-dependent.Higher.Coinductive.Small.Erased
import README.Fst-snd
------------------------------------------------------------------------
-- 2: Cubical Agda
-- The functions cong and ext.
cong = Equality.Path.cong
ext = Equality.Path.⟨ext⟩
-- The propositional truncation operator.
∥_∥ = H-level.Truncation.Propositional.∥_∥
-- The map function. This function is not defined in the same way as
-- in the paper, it is defined using a non-dependent eliminator.
map = H-level.Truncation.Propositional.∥∥-map
-- The propositional truncation operator with an erased truncation
-- constructor.
∥_∥ᴱ = H-level.Truncation.Propositional.Erased.∥_∥ᴱ
-- Half adjoint equivalences. Note that, unlike in the paper, _≃_ is
-- defined as a record type.
Is-equivalence = Equivalence.Half-adjoint.Is-equivalence
_≃_ = Equivalence._≃_
-- Univalence. (This type family is not defined in exactly the same
-- way as in the paper.)
Univalence = Univalence-axiom.Univalence
-- A proof of univalence. The proof uses glue.
--
-- The current module uses --erased-cubical, so this proof, which is
-- defined using --cubical, can only be used in erased contexts.
@0 univ : _
univ = Equality.Path.Univalence.univ
------------------------------------------------------------------------
-- 3: Postulating Erased Univalence
-- Erased.
Erased = Erased.Basics.Erased
-- []-cong for paths.
[]-cong = Erased.Cubical.[]-cong-Path
------------------------------------------------------------------------
-- 6.1: Equivalences with Erased Proofs
-- Equivalences with erased proofs. Note that, unlike in the paper,
-- _≃ᴱ_ is defined as a record type.
Is-equivalenceᴱ = Equivalence.Erased.Basics.Is-equivalenceᴱ
_≃ᴱ_ = Equivalence.Erased.Basics._≃ᴱ_
to = Equivalence.Erased.Basics._≃ᴱ_.to
from = Equivalence.Erased.Basics._≃ᴱ_.from
@0 to-from : _
to-from = Equivalence.Erased.Basics._≃ᴱ_.right-inverse-of
@0 from-to : _
from-to = Equivalence.Erased.Basics._≃ᴱ_.left-inverse-of
-- Erased≃ is stated a little differently.
Erased≃ = Erased.Level-1.Erased↔
-- Lemmas 41 and 42 are proved in modules parametrised by definitions
-- of []-cong, which is also assumed to satisfy certain properties
-- (that hold for the definition mentioned above). Some definitions
-- below are also defined in such modules.
Lemma-41 = Erased.Level-1.Erased-cong.Erased-cong-≃
Lemma-42 = Equivalence.Erased.[]-cong₁.Σ-cong-≃ᴱ-Erased
-- The functions substᴱ and subst.
substᴱ = Erased.Level-1.[]-cong₁.substᴱ
subst = Equality.Path.subst
-- Lemmas 45–47.
Lemma-45 = Equivalence.Erased.[]-cong.drop-⊤-left-Σ-≃ᴱ-Erased
Lemma-46 = Equivalence.Erased.Σ-cong-≃ᴱ
Lemma-47 = Equivalence.Erased.drop-⊤-left-Σ-≃ᴱ
------------------------------------------------------------------------
-- 6.2: A Non-recursive Definition of the Propositional Truncation
-- Operator
-- ∥_∥¹ and Colimit.
∥_∥¹ = H-level.Truncation.Propositional.One-step.∥_∥¹
Colimit = Colimit.Sequential.Colimit
-- Lemma 50.
Lemma-50 = Colimit.Sequential.universal-property
-- ∥_∥¹-out and ∥_∥ᴺ.
∥_∥¹-out = H-level.Truncation.Propositional.One-step.∥_∥¹-out-^
∥_∥ᴺ = H-level.Truncation.Propositional.Non-recursive.∥_∥
-- ∥_∥ᴺ and ∥_∥ are pointwise equivalent.
∥∥ᴺ≃∥∥ = H-level.Truncation.Propositional.Non-recursive.∥∥≃∥∥
-- Colimitᴱ.
Colimitᴱ = Colimit.Sequential.Very-erased.Colimitᴱ
-- Lemma 54.
Lemma-54 = Colimit.Sequential.Very-erased.universal-property
-- ∥_∥ᴺᴱ.
∥_∥ᴺᴱ = H-level.Truncation.Propositional.Non-recursive.Erased.∥_∥ᴱ
-- Lemma 56 (or rather its inverse).
Lemma-56 = H-level.Truncation.Propositional.Erased.∥∥ᴱ≃∥∥ᴱ
------------------------------------------------------------------------
-- 6.3: Higher Lenses with Erased Proofs
-- Lensᴱ, get and set.
Lensᴱ = Lens.Non-dependent.Higher.Lens
get = Lens.Non-dependent.Higher.Lens.get
set = Lens.Non-dependent.Higher.Lens.set
-- Lensᴱᴱ.
Lensᴱᴱ = Lens.Non-dependent.Higher.Erased.Lens
-- The function _⁻¹_.
_⁻¹_ = Preimage._⁻¹_
-- Lens^C (defined using a record type).
@0 Lens^C : _
Lens^C = Lens.Non-dependent.Higher.Coinductive.Small.Lens
-- Coherently-constant^C.
@0 Coherently-constant^C : _
Coherently-constant^C =
Lens.Non-dependent.Higher.Coinductive.Small.Coherently-constant
-- Lens^CE (with the field name get⁻¹-coherently-constant instead of
-- cc).
Lens^CE = Lens.Non-dependent.Higher.Coinductive.Small.Erased.Lens
------------------------------------------------------------------------
-- 6.4: The Definitions Are Equivalent
-- Lemma 65 (or rather its inverse), and a proof (in an erased
-- context) showing that Lemma 65 preserves getters and setters.
Lemma-65 =
Lens.Non-dependent.Higher.Coinductive.Small.Erased.Lens≃ᴱLensᴱ
@0 Lemma-65-preserves-getters-and-setters : _
Lemma-65-preserves-getters-and-setters =
Lens.Non-dependent.Higher.Coinductive.Small.Erased.Lens≃ᴱLensᴱ-preserves-getters-and-setters
-- Lens₁ᴱ and Lens₂ᴱ.
Lens₁ᴱ = Lens.Non-dependent.Higher.Capriotti.Variant.Erased.Variant.Lens
Lens₂ᴱ = Lens.Non-dependent.Higher.Coinductive.Erased.Lens
-- The function _⁻¹ᴱ_.
_⁻¹ᴱ_ = Equivalence.Erased.Contractible-preimages._⁻¹ᴱ_
-- Coherently-constant₁ᴱ, Coherently-constant, Coherently-constant₂ᴱ,
-- Coherently-constant₂^C and constant.
Coherently-constant₁ᴱ =
Lens.Non-dependent.Higher.Capriotti.Variant.Erased.Variant.Coherently-constant
Coherently-constant =
Coherently-constant.Coherently-constant
Coherently-constant₂ᴱ =
Lens.Non-dependent.Higher.Coinductive.Erased.Coherently-constant
@0 Coherently-constant₂^C : _
Coherently-constant₂^C =
Lens.Non-dependent.Higher.Coinductive.Coherently-constant
@0 constant : _
constant =
Lens.Non-dependent.Higher.Coinductive.constant
-- Lemmas 74–77.
Lemma-74 = Erased.Stability.Erased-other-singleton≃ᴱ⊤
Lemma-75 = Lens.Non-dependent.Higher.Coinductive.Erased.∥∥ᴱ→≃
Lemma-76 = Equivalence.Erased.other-singleton-with-Π-≃ᴱ-≃ᴱ-⊤
Lemma-77 = H-level.Truncation.Propositional.Erased.Σ-Π-∥∥ᴱ-Erased-≡-≃
------------------------------------------------------------------------
-- 6.5: Compilation of Lenses
-- A slightly more general variant of sndᴱ.
sndᴱ = Lens.Non-dependent.Higher.Erased.snd
-- Lemma 79.
Lemma-79 = H-level.Truncation.Propositional.Erased-∥∥×≃
-- A slightly more general variant of snd^C.
snd^C = README.Fst-snd.snd-with-space-leak
-- Lemma 81.
Lemma-81 =
Lens.Non-dependent.Higher.Coinductive.Small.Erased.with-other-setter
-- A slightly more general variant of the variant of snd^C with a
-- changed setter.
snd^C-with-changed-setter = README.Fst-snd.snd