The model of the tick calculus can be extended with basic type constructors like natural numbers,
\(\Pi \) - and \(\Sigma \) -types as well as identity types. Here we just recall what it means for a
CwF to have extensional identity types, referring the reader to Hofmann [1]} for details on other
constructors.
