Martin Escardo, 26 January 2018 Moved from the file TotallySeparated 22 August 2024, and split into the following modules. \begin{code} {-# OPTIONS --safe --without-K #-} module Apartness.index where import Apartness.Definition import Apartness.Examples import Apartness.Morphisms import Apartness.NegationOfApartness import Apartness.Properties import Apartness.TightReflection \end{code}