------------------------------------------------------------------------ -- Safe modules that use --erased-cubical ------------------------------------------------------------------------ {-# OPTIONS --safe --erased-cubical #-} module README.Safe.Cubical.Erased where -- Paths, extensionality and univalence. import Equality.Path -- Isomorphisms and equalities relating an arbitrary "equality with J" -- to path equality, along with proofs of extensionality and -- univalence for the "equality with J". import Equality.Path.Isomorphisms -- The cubical identity type. import Equality.Id -- Propositional equality, with some extra bells and whistles -- definable in Cubical Agda. import Equality.Propositional.Cubical -- Some tactics aimed at making equational reasoning proofs more -- readable for path equality. import Tactic.By.Path -- Some tactics aimed at making equational reasoning proofs more -- readable for the cubical identity type. import Tactic.By.Id -- Some theory of Erased, developed using Cubical Agda. import Erased.Cubical -- Some theory of equivalences with erased "proofs", defined in terms -- of partly erased contractible fibres, developed using Cubical Agda. import Equivalence.Erased.Contractible-preimages.Cubical -- Some theory of equivalences with erased "proofs", developed using -- Cubical Agda. import Equivalence.Erased.Cubical -- A sequential colimit for which everything except for the "base -- case" is erased. import Colimit.Sequential.Very-erased -- The sequential colimit HIT with an erased higher constructor. import Colimit.Sequential.Erased -- Sequential colimits. import Colimit.Sequential -- The one-step truncation HIT with an erased higher constructor. import H-level.Truncation.Propositional.One-step.Erased -- The one-step truncation. import H-level.Truncation.Propositional.One-step -- A non-recursive variant of H-level.Truncation.Propositional.Erased. import H-level.Truncation.Propositional.Non-recursive.Erased -- A variant of the propositional truncation operator with an erased -- truncation constructor. import H-level.Truncation.Propositional.Erased -- Propositional truncation. import H-level.Truncation.Propositional -- A definition of the propositional truncation operator that does not -- use recursive higher inductive types. import H-level.Truncation.Propositional.Non-recursive -- The "interval". import Interval -- Suspensions. import Suspension -- Spheres. import Sphere -- Pushouts, defined using a HIT. import Pushout -- Joins. import Join -- Localisation. import Localisation -- Nullification. import Nullification -- The nullification modality. import Nullification.Modality -- Truncation, defined as a HIT. import H-level.Truncation -- Homotopy groups of pointed types. import Pointed-type.Homotopy-group -- Connectedness for pointed types. import Pointed-type.Connected -- A variant of set quotients with erased higher constructors. import Quotient.Erased.Basics -- Quotients (set-quotients), defined using a higher inductive type. import Quotient -- Two variants of the set quotients from Quotient. import Quotient.Set-truncated-if-propositional import Quotient.Higher-constructors-if-propositional -- A variant of set quotients with erased higher constructors. import Quotient.Erased -- Listed finite subsets. import Finite-subset.Listed -- A membership relation for listed finite subsets (defined using -- erased univalence). import Finite-subset.Listed.Membership.Erased -- Kuratowski finite subsets. import Finite-subset.Kuratowski -- Listed finite subsets, defined using a HIT with erased higher -- constructors. import Finite-subset.Listed.Erased -- Cyclic groups. import Group.Cyclic -- Integers, defined using a quotient type. import Integer.Quotient -- The Eilenberg-MacLane space K(G, 1). import Eilenberg-MacLane-space -- Coherently constant functions. import Coherently-constant -- The "circle". import Circle -- The circle with an erased higher constructor. import Circle.Erased -- The torus, defined as a HIT. import Torus -- The figure of eight. import Figure-of-eight -- A variant of Nat.Wrapper.Cubical, defined using --erased-cubical. import Nat.Wrapper.Cubical.Erased -- A variant of the development in "Internalizing Representation -- Independence with Univalence" (by Angiuli, Cavallo, Mörtberg and -- Zeuner) with support for erasure. import Structure-identity-principle.Erased -- Truncated queues: any two queues representing the same sequence are -- equal, and things are set up so that at compile-time (but not at -- run-time) some queue operations compute in roughly the same way as -- the corresponding list operations. import Queue.Truncated -- Queue instances for the queues in Queue.Truncated. import Queue.Truncated.Instances -- Quotiented queues: any two queues representing the same sequence -- are equal. import Queue.Quotiented -- Queue instances for the queues in Queue.Quotiented. import Queue.Quotiented.Instances -- Abstract binding trees, based on Harper's "Practical Foundations -- for Programming Languages". import Abstract-binding-tree import README.Abstract-binding-tree