open import Prim.Extension
open import Prim.Interval
open import Prim.Type
open import Prim.Kan

module Prim.Data.Bool where

Primitive: Booleans🔗

The booleans are the h-initial type with two inhabitants.

data Bool : Type where
  true false : Bool
{-# BUILTIN BOOL Bool #-}

{-# BUILTIN FALSE false #-}
{-# BUILTIN TRUE true #-}