------------------------------------------------------------------------ -- 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. -- An attempt has been made to track uses of univalence by passing -- around explicit proofs of the univalence axiom (except in certain -- README modules). However, some library code that is used does not -- adhere to this convention (note that univalence is provable in -- Cubical Agda), so perhaps some use of univalence is not tracked in -- this way. On the other hand some library code that is not defined -- in Cubical Agda passes around explicit proofs of 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 and some other lemmas use arguments of type Block s (for -- some string s). This type is equivalent to the unit type. These -- arguments are used to block definitions from being unfolded by the -- type-checker. 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