lean2/hott/naming_conventions.md
Floris van Doorn 341a53b880 feat(pointed): make the naming in the pointed library more consistent.
Also start on a naming conventions file
2016-09-22 16:00:27 -04:00

14 lines
No EOL
802 B
Markdown

HoTT Naming Conventions
=======================
[generic naming conventions go here]
Pointed Types
-------------
We use a prefix `p` to specify that an operation/construction is pointed. For example `pequiv` is
pointed equivalences and `phomotopy` are pointed homotopies. Only if a construction only works for
pointed types and has no unpointed equivalent we omit the `p` (examples: `loop` `loopn`
`homotopy_group`). A lemma about pointed constructions repeats the `p` for every name, for example
`psusp_pequiv_psusp` or `pid_pcompose`. For notation we append `*` for the pointed version, like `Type*` (this is the universe of pointed types, not the universe considered as a pointed type), `S*` or `bool*`. For notations which only make sense pointed we don't add the star, like `Ω[n]` or `π[k]`.