BeiZero

module Lecture-2 where

data ⊤ : Set where --\top
  tt : ⊤

data ⊥ : Set where --\bot

⊥-elim : {A : Set} → ⊥ → A
⊥-elim = λ ()

BeiZero

module Bool where

data 𝔹 : Set where --\bB
  true : 𝔹
  false : 𝔹

if_then_else_ : {A : Set} → 𝔹 → A → A → A --\to
if true then a else b = a
if false then a else b = b