Martin Escardo

\begin{code}

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

module Fin.index where

import Fin.ArgMinMax
import Fin.ArithmeticViaEquivalence
import Fin.Bishop
import Fin.Choice
import Fin.Dedekind
import Fin.Embeddings
import Fin.Kuratowski
import Fin.Omega
import Fin.Order
import Fin.Pigeonhole
import Fin.Properties
import Fin.Topology
import Fin.Type
import Fin.UniverseInvariance
import Fin.Variation

\end{code}