CONVENTIONS.txt

	       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.
   Try to use \cite for your citations so that they will all have a
   uniform appearance; \cite is currently aliased to natbib's \citep,
   but we may change it in the future.

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.