\begin{code} {-# OPTIONS --safe --without-K #-} module TWA.index where import TWA.Thesis.index -- Todd Waugh Ambridge's Thesis, with two files by Andrew Sneap import TWA.BanachFixedPointTheorem -- By Todd Waugh Ambridge import TWA.Closeness -- Mostly by Todd Waugh Ambridge, originally by Martin Escardo import TWA.Escardo-Simpson-LICS2001 -- By Todd Waugh Ambridge import TWA.SIP-IntervalObject -- By Todd Waugh Ambridge \end{code}