Two-point type.

\begin{code}

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

module Two where

open import Universes

data 𝟚 : 𝓤₀ ̇  where
  : 𝟚
  : 𝟚

𝟚-induction : {A : 𝟚  𝓤 ̇ }  A   A   (x : 𝟚)  A x
𝟚-induction r s  = r
𝟚-induction r s  = s

𝟚-cases : {A : 𝓤 ̇ }  A  A  𝟚  A
𝟚-cases = 𝟚-induction

\end{code}