\begin{code} {-# OPTIONS --safe --without-K #-} module CoNaturals.BothTypes where open import CoNaturals.GenericConvergentSequence public hiding (is-finite') open import CoNaturals.GenericConvergentSequence2 public open import CoNaturals.Equivalence public open import CoNaturals.Type2Properties public \end{code}