Our Spartan (intensional) Martin-LΓΆf type theory has the empty type βˆ…,
the unit type πŸ™, two-point-type 𝟚, natural numbers β„•, product types Ξ ,
sum types Ξ£ (and hence binary product types _Γ—_), sum types _+_,
identity types _≑_, and universes 𝓀, π“₯, 𝓦, ....

\begin{code}

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

module SpartanMLTT where

open import Empty           public
open import One             public
open import Two             public
open import NaturalNumbers  public
open import Plus            public
open import Pi              public
open import Sigma           public
open import Universes       public
open import Id              public

open import GeneralNotation public

\end{code}