The booleans

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2026-05-02.
Last modified on 2026-05-02.

module foundation-core.booleans where
Imports 
open import foundation.dependent-pair-types
open import foundation.unit-type
open import foundation.universe-levels

open import foundation-core.constant-maps
open import foundation-core.empty-types
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.identity-types
open import foundation-core.negation
open import foundation-core.propositions
open import foundation-core.sections
open import foundation-core.sets

Idea

The type of booleans is a 2-element type with elements true false : bool, which is used for reasoning with decidable propositions.

Definition

The booleans

data bool : UU lzero where
  true false : bool

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

The induction principle of the booleans

module _
  {l : Level} (P : bool → UU l)
  where

  ind-bool : P true → P false → (b : bool) → P b
  ind-bool pt pf true = pt
  ind-bool pt pf false = pf

The recursion principle of the booleans

module _
  {l : Level} {P : UU l}
  where

  rec-bool : P → P → bool → P
  rec-bool = ind-bool (λ _ → P)

The if_then_else function

module _
  {l : Level} {A : UU l}
  where

  if_then_else_ : bool → A → A → A
  if b then x else y = rec-bool x y b

The standard propositions associated to the constructors of bool

prop-bool : bool → Prop lzero
prop-bool true = unit-Prop
prop-bool false = empty-Prop

type-prop-bool : bool → UU lzero
type-prop-bool = type-Prop ∘ prop-bool

Equality on the booleans

Eq-bool : bool → bool → UU lzero
Eq-bool true true = unit
Eq-bool true false = empty
Eq-bool false true = empty
Eq-bool false false = unit

refl-Eq-bool : (x : bool) → Eq-bool x x
refl-Eq-bool true = star
refl-Eq-bool false = star

Eq-eq-bool :
  {x y : bool} → x ＝ y → Eq-bool x y
Eq-eq-bool {x = x} refl = refl-Eq-bool x

eq-Eq-bool :
  {x y : bool} → Eq-bool x y → x ＝ y
eq-Eq-bool {true} {true} star = refl
eq-Eq-bool {false} {false} star = refl

neq-false-true-bool : ¬ (false ＝ true)
neq-false-true-bool ()

neq-true-false-bool : ¬ (true ＝ false)
neq-true-false-bool ()

Structure

The boolean operators

conjunction-bool : bool → bool → bool
conjunction-bool true true = true
conjunction-bool true false = false
conjunction-bool false true = false
conjunction-bool false false = false

disjunction-bool : bool → bool → bool
disjunction-bool true true = true
disjunction-bool true false = true
disjunction-bool false true = true
disjunction-bool false false = false

implication-bool : bool → bool → bool
implication-bool true true = true
implication-bool true false = false
implication-bool false true = true
implication-bool false false = true

Properties

The booleans are a set

abstract
  is-prop-Eq-bool : (x y : bool) → is-prop (Eq-bool x y)
  is-prop-Eq-bool true true = is-prop-unit
  is-prop-Eq-bool true false = is-prop-empty
  is-prop-Eq-bool false true = is-prop-empty
  is-prop-Eq-bool false false = is-prop-unit

abstract
  is-set-bool : is-set bool
  is-set-bool =
    is-set-prop-in-id
      ( Eq-bool)
      ( is-prop-Eq-bool)
      ( refl-Eq-bool)
      ( λ x y → eq-Eq-bool)

bool-Set : Set lzero
bool-Set = bool , is-set-bool

The “is true” predicate on booleans

is-true : bool → UU lzero
is-true = _＝ true

is-prop-is-true : (b : bool) → is-prop (is-true b)
is-prop-is-true b = is-set-bool b true

is-true-Prop : bool → Prop lzero
is-true-Prop b = is-true b , is-prop-is-true b

The “is false” predicate on booleans

is-false : bool → UU lzero
is-false = _＝ false

is-prop-is-false : (b : bool) → is-prop (is-false b)
is-prop-is-false b = is-set-bool b false

is-false-Prop : bool → Prop lzero
is-false-Prop b = is-false b , is-prop-is-false b

A boolean cannot be both true and false

not-is-false-is-true : (x : bool) → is-true x → ¬ (is-false x)
not-is-false-is-true true t ()
not-is-false-is-true false () f

not-is-true-is-false : (x : bool) → is-false x → ¬ (is-true x)
not-is-true-is-false true () f
not-is-true-is-false false t ()

The constant function const bool b is not an equivalence

abstract
  no-section-const-bool : (b : bool) → ¬ (section (const bool b))
  no-section-const-bool true (g , G) = neq-true-false-bool (G false)
  no-section-const-bool false (g , G) = neq-false-true-bool (G true)

abstract
  is-not-equiv-const-bool :
    (b : bool) → ¬ (is-equiv (const bool b))
  is-not-equiv-const-bool b e = no-section-const-bool b (section-is-equiv e)

Recent changes