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 #-}