Martin Escardo \begin{code} {-# OPTIONS --safe --without-K #-} module CoNaturals.index where import CoNaturals.Type -- The type of conatural numbers. import CoNaturals.Type2 -- An equivalent copy. import CoNaturals.UniversalProperty import CoNaturals.Equivalence import CoNaturals.Type2Properties import CoNaturals.BothTypes import CoNaturals.Arithmetic import CoNaturals.Exercise -- With Chuangjie Xu. import CoNaturals.GenericConvergentSequence -- Avoid to import directly. import CoNaturals.GenericConvergentSequence2 -- Avoid to import directly. import CoNaturals.Sharp \end{code}