hopf language

Author: 5HT

doc/anders.pdf

@@ -39,8 +39,8 @@ \section{Introduction}
 
 \textbf{Anders} is a Modal HoTT proof assistant based on: classical MLTT-80 \cite{MLTT80}
 with 0, 1, 2, W types; CCHM \cite{CCHM} in CHM \cite{CHM} flavour as cubical type system with
-hcomp/transp Kan operations; HTS \cite{HTS} strict equality on pretypes in Voevodsky style;
-de Rham \cite{deRham} stack modality primitives for infinitesimal differential geometry purposes.
+hcomp/transp operations; HTS \cite{HTS} strict equality on pretypes;
+infinitisemal \cite{deRham} modality primitives for differential geometry purposes.
 We tend not to touch general recursive higher inductive schemes,
 instead we will try to express as much HIT as possible through Suspensions, Truncations,
 Quotients primitives built into type checker core.