Martin Escardo, from about 2010 to today.

A motivation for what is done here can be found in three blog
posts by Chris Groassack from July 2024:
https://grossack.site/tags/life-in-the-topological-topos/

\begin{code}

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

module TypeTopology.index where

import TypeTopology.ADecidableQuantificationOverTheNaturals
import TypeTopology.AbsolutenessOfCompactness -- by Andrew Swan
import TypeTopology.AbsolutenessOfCompactnessExample -- by Andrew Swan
import TypeTopology.Cantor
import TypeTopology.CantorMinusPoint
import TypeTopology.CantorSearch
import TypeTopology.CompactTypes
import TypeTopology.ConvergentSequenceHasInf
import TypeTopology.DecidabilityOfNonContinuity
import TypeTopology.Density
import TypeTopology.DisconnectedTypes
import TypeTopology.ExtendedSumCompact
import TypeTopology.FailureOfTotalSeparatedness
import TypeTopology.GenericConvergentSequenceCompactness
import TypeTopology.InfProperty
import TypeTopology.LexicographicCompactness
import TypeTopology.PropInfTychonoff
import TypeTopology.PropTychonoff
import TypeTopology.RicesTheoremForTheUniverse
import TypeTopology.SequentiallyHausdorff
import TypeTopology.SigmaDiscreteAndTotallySeparated
import TypeTopology.SimpleTypes
import TypeTopology.SquashedCantor
import TypeTopology.SquashedSum
import TypeTopology.TheTopologyOfTheUniverse
import TypeTopology.TotallySeparated
import TypeTopology.UniformSearch -- by Ayberk Tosun
import TypeTopology.WeaklyCompactTypes

\end{code}