Martin Escardo

https://doi.org/10.1017/S0960129520000225

Please follow the link after the import:

\begin{code}

{-# OPTIONS --without-K --exact-split --safe --no-sized-types --no-guardedness --auto-inline #-}

import InjectiveTypes.Article

\end{code}

*** Please do not move this file. It is linked from a published paper. ***