Martin Escardo

\begin{code}

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

module BinarySystems.index where

import BinarySystems.InitialBinarySystem    -- More work than needed!
import BinarySystems.InitialBinarySystem2   -- No need to work with subtype of normal elements.
-- import BinarySystems.CubicalBinarySystem -- By Martin Escardo and Alex Rice;
                                            -- works with Agda 2.6.2 and needs the Cubical Library.
\end{code}