include hlevels

HoTT · Dec 18, 2012 · 302a6a8 · 302a6a8
1 parent 8ceb06a
commit 302a6a8
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/CONVENTIONS.txt b/CONVENTIONS.txt
@@ -27,9 +27,9 @@
    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
+   p \ct q		concatenation of equalities p and q (diagrammatic order)
    \opp{p} or \rev{p}	the opposite equality of p
-   \trans{p}{x}		transport of x along 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 

diff --git a/main.tex b/main.tex
@@ -32,6 +32,8 @@
 
 \include{induction}
 
+\include{hlevels}
+
 \include{hits}
 
 \include{homotopy}