Martin Escardo

For a discussion of what is done here, see
https://mathstodon.xyz/@MartinEscardo/109395006766077334

\begin{code}

{-# OPTIONS --safe --without-K #-}

module Factorial.index where

import Factorial.Law
import Factorial.PlusOneLC
import Factorial.Swap

\end{code}