Before submitting changes, make sure they do not contradict the requirements described in this document.
If your change conflicts with a requirement with the word "MUST", it will be rejected.
If your change conflicts with a requirement with the word "SHOULD", it may be accepted if the requirement cannot be met for a valid reason.
Self-check changes against requirements before submitting them, this will save a lot of time and effort for the maintainer to check them and increase the likelihood and speed of change acceptance.
The meanings of the terms "MUST" (also "SHOULD", "MAY", etc.) in this document are in accordance with RFC 2119.
-
1.1 Prelude modules SHOULD be imported as follows:
Foundations.Base
when working on otherFoundations.*
Foundations.Prelude
when working onMeta.*
internalsMeta.Prelude
when working on other modulesPrelude
,Algebra.Prelude
,Categories.Prelude
when using cubical-mini as an external dependency
-
1.2 Inductive
Data.*
types MUST have:- recursor (
rec
) - dependent eliminator (
elim
) - universal property for mapping out (
universal
)
- recursor (
-
1.3 All
Data.*
types MUST have:- path space characterization (
module Path
) +Extensionality
instance - discreteness instance (if applicable)
- strongest finiteness instance (if applicable)
- path space characterization (
-
1.4 Definitions SHOULD be maximally universe polymorphic.
-
1.5 Imports MUST NOT be
public
except for modules intended for collection and re-export. -
1.6 Primitives and built-ins MUST NOT be imported anywhere except in
Foundations.*
,Data.*.Base
,IO.*
. -
1.7
Base
submodule MUST import only theFoundations.*
modules and those essential for the definition. -
1.8 Definitions SHOULD be grouped in folders and modules by math area and its' customs, and not by implementation details.
HITs
module would be an example of how NOT to group things as HITs per se aren't studied in this library, they are used as a tool to describe other mathematical concepts.
-
2.1 The project SHOULD be tested with
make test
before submitting changes. -
2.2 If macros are used, the
private variable
SHOULD NOT be used to quantify universe levels, but SHOULD be used otherwise. -
2.3 Option
--safe
SHOULD be used. -
2.4 Options
--no-exact-split
,--lossy-unification
MAY be used. -
2.5 Record terms SHOULD be created using copattern-matching for efficiency.
-
2.6 If function argument can always be inferred, it MUST be made implicit.
-
2.7 If function argument is rarely inferred, it SHOULD be made explicit.
-
3.1.1 Lines SHOULD be less than 100 characters in length.
-
3.1.2 The reference to the paper on which the code is based SHOULD be at the top of the file.
-
3.1.3 Local definitions MUST be in
where
,let-in
orprivate
.So that it is easy to see which are the main results of a file and which are just helper definitions.
-
3.1.6 Imports SHOULD be grouped in the following order:
Foundations
,Meta
,Structures
,Correspondences
,Data
,Functions
.
And in lexicographical order inside groups.
-
3.2.1 Type names SHOULD start with a capital letter, except for types representing properties, they MUST start with
is
(e.g.is-prop
). -
3.2.2 Other identifier names SHOULD be in kebab case.
-
3.2.3 Definition names MUST NOT refer to variable names.
For example, prefer
+-comm
to something likem+n≡n+m
. -
3.2.4 Identifier names MUST NOT contain
=
, use=
instead.Otherwise it garbles column alignment.
-
3.2.5 Predicate names MUST be written as suffixes, e.g.:
Nat-is-set
,is-prop-is-prop
,is-of-hlevel-is-prop
.
-
3.2.6 Fields of a record indicating the truth of a predicate MUST be prefixed with
has-
. -
3.2.7 All long names SHOULD be abbreviated, as in the table:
Long name Abbreviation identity on the left id-l
identity on the right id-r
commutative comm
associative assoc
idempotent idem
absorptive absorp
distribute left dist-l
distribute right dist-r
composition comp
function fun
category Cat
homomorphism hom
-
3.2.8 Level names MUST be descriptive or
ℓ ℓ′ ℓ″ ... ℓᵃ ℓᵇ ℓᶜ ... ℓa ℓb ℓc ...
-
3.2.9
≡
SHOULD refer to congruences or some other strict similarity relations.When defining a new target language, locally rename
=
to≡
for definitional equalities of the target language if you need so. Builtin Agda equality is called_=ⁱ_
. -
3.2.10
→
SHOULD be used overto
. -
3.2.11
equiv
or≃
SHOULD refer to equivalences of types or structures.Operators can use subscript
ₑ
. -
3.2.12
iso
or≅
SHOULD refer to isomorphisms of types or structures.Here an isomorphism is a function with a quasi-inverse, i.e. a quasi-equivalence in the sense of the HoTT Book. Operators can use subscript
ᵢ
. -
3.2.13
Path
or=
SHOULD refer to paths in names, notEq
,Id
, or other "equality" or "identity"-related names.Operators can use subscript
ₚ
. -
3.2.14 Sub- and superscripts MUST be used in the following order:
- Alpha subscript,
- Numerical subscript,
- Alpha superscript,
- Numerical superscript.
-
3.2.15 Numerical superscripts SHOULD be used for arity specification.
-
3.2.16 Numerical subscripts SHOULD be used to indicate hlevel.
-
3.2.17 Results about
Pathᴾ
(path overs) SHOULD end with superscriptᴾ
. -
3.2.18 Results about displayed stuff SHOULD end with superscript
ᴰ
. -
3.2.19 Partial function names (returning
Maybe
) SHOULD use superscriptᵐ
.