Permalink
Switch branches/tags
Nothing to show
Find file
Fetching contributors…
Cannot retrieve contributors at this time
72 lines (61 sloc) 3.17 KB
Authorial conventions for the HoTT Book
1. To denote equality/identity/path types, you can write simply "="
infix. Of course, this works for chains of equalities "a=b=c=d"
and also vertically-stacked ones. An alternative notation is
"\id{x}{y}", or "\id[A]{x}{y}" if you want to notate the type to
which x and y belong; this notation might produce "x=y" or
"Id(x,y)" in the future. If you want to be sure of producing
"Id(x,y)", write instead "\idtype{x}{y}" or "\idtype[A]{x}{y}".
Note that single-character non-optional arguments do not need
braces, so you can write "\idtype xy", but you need to write
"\idtype{(x+1)^2}{x^2+2x+1}".
2. There are two macros that denote definitional/judgmental equality.
\jdeq or \judgeq should be used for an equality judgment being made
about two extant terms, while \defeq should be used when the
left-hand side is currently being defined to equal the right-hand
side. Both are used infix, and currently produce \equiv and
\coloneqq (that is, :=), respectively.
3. Here is a cheatsheet of some more macros. Arguments in [brackets]
are optional and can be omitted.
x = y identity type (fixed notation "x=y")
\id[A]{x}{y} identity type (agnostic notation)
\idtype[A]{x}{y} identity type (fixed notation "Id(x,y)")
x \jdeq y x is judged to be definitionally equal to y
x \defeq y x is currently being defined to equal y
\refl{x} reflexivity term at x
p \ct q concatenation of equalities p and q (diagrammatic order)
\opp{p} or \rev{p} the opposite equality of p
\trans{p}{x} covariant transport of x along p
\map{f}{p} map the path p under the function f
\mapdep{f}{p} likewise, for a dependently typed function f
\idfunc[A] the identity function of a type A
\eqv{A}{B} the type of equivalences from A to B
\type,\set,\prop universes of types, sets, and propositions
3. In the style of a textbook or lecture notes, generally try to keep
citations and references out of the main text. Rather, each
chapter should have an unnumbered "Notes" section at the end
containing references to the literature and relevant comments.
References should go in the references.bib file in BibTeX format.
Use \cite for your citations so that they will all have a uniform
appearance.
4. The following theorem-type environments are predefined:
thm Theorem
cor Corollary
lem Lemma
defn Definition
rmk Remark
eg Example
egs Examples
ex Exercise
When referring to a theorem defined elsewhere, use the macro
\autoref. This automatically produces words before numbers, such
as "Theorem 3.1", and automatically changes them if (for instance)
you change a theorem to a lemma.
Similarly, try to add \label{}s to all of your theorem-environments
so that other people can refer to them. If you find yourself needing
a lemma that you think should appear in someone else's chapter, you
can add a stub to their chapter with a \label. Only the following
characters should be used in labels: letters, digits, colon : and
dash -.
5. Each chapter is encouraged to also have an unnumbered section of
"Exercises" at the end.