The booleans

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Elisabeth Stenholm, Daniel Gratzer and Louis Wasserman.

Created on 2022-01-27.
Last modified on 2026-05-02.

module foundation.booleans where

open import foundation-core.booleans public
Imports 
open import foundation.apartness-relations
open import foundation.boolean-operations
open import foundation.decidable-equality
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.discrete-types
open import foundation.involutions
open import foundation.negated-equality
open import foundation.raising-universe-levels
open import foundation.tight-apartness-relations
open import foundation.unit-type
open import foundation.universe-levels

open import foundation-core.constant-maps
open import foundation-core.coproduct-types
open import foundation-core.decidable-propositions
open import foundation-core.double-negation-stable-equality
open import foundation-core.empty-types
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.homotopies
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

open import univalent-combinatorics.finite-types
open import univalent-combinatorics.standard-finite-types

Idea

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

Definition

Equality on the booleans is decidable

is-decidable-Eq-bool : {x y : bool} → is-decidable (Eq-bool x y)
is-decidable-Eq-bool {true} {true} = inl star
is-decidable-Eq-bool {true} {false} = inr id
is-decidable-Eq-bool {false} {true} = inr id
is-decidable-Eq-bool {false} {false} = inl star

The standard interpretation of booleans as decidable propositions

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

Properties

The booleans have decidable equality

has-decidable-equality-bool : has-decidable-equality bool
has-decidable-equality-bool true true = inl refl
has-decidable-equality-bool true false = inr neq-true-false-bool
has-decidable-equality-bool false true = inr neq-false-true-bool
has-decidable-equality-bool false false = inl refl

bool-Discrete-Type : Discrete-Type lzero
bool-Discrete-Type = bool , has-decidable-equality-bool

has-double-negation-stable-equality-bool :
  has-double-negation-stable-equality bool
has-double-negation-stable-equality-bool x y =
  double-negation-elim-is-decidable (has-decidable-equality-bool x y)

The booleans have a tight apartness relation

bool-Type-With-Tight-Apartness : Type-With-Tight-Apartness lzero lzero
bool-Type-With-Tight-Apartness =
  type-with-tight-apartness-Discrete-Type bool-Discrete-Type

The “is true” predicate on booleans is decidable

is-decidable-prop-is-true : (b : bool) → is-decidable-prop (is-true b)
is-decidable-prop-is-true b =
  ( is-prop-is-true b , has-decidable-equality-bool b true)

is-true-Decidable-Prop : bool → Decidable-Prop lzero
is-true-Decidable-Prop b = (is-true b , is-decidable-prop-is-true b)

The “is false” predicate on booleans is decidable

is-decidable-prop-is-false : (b : bool) → is-decidable-prop (is-false b)
is-decidable-prop-is-false b =
  ( is-prop-is-false b , has-decidable-equality-bool b false)

is-false-Decidable-Prop : bool → Decidable-Prop lzero
is-false-Decidable-Prop b = (is-false b , is-decidable-prop-is-false b)

A boolean cannot be both true and false

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

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

is-false-is-not-true : (x : bool) → ¬ (is-true x) → is-false x
is-false-is-not-true true np = ex-falso (np refl)
is-false-is-not-true false np = refl

is-true-is-not-false : (x : bool) → ¬ (is-false x) → is-true x
is-true-is-not-false true np = refl
is-true-is-not-false false np = ex-falso (np refl)

contrapositive-is-true-bool :
  {x y : bool} → (is-true x → is-true y) → is-false y → is-false x
contrapositive-is-true-bool {x} f refl =
  is-false-is-not-true x (neq-false-true-bool ∘ f)

contrapositive-is-false-bool :
  {x y : bool} → (is-false x → is-false y) → is-true y → is-true x
contrapositive-is-false-bool {x} f refl =
  is-true-is-not-false x (neq-true-false-bool ∘ f)

The type of booleans is equivalent to Fin 2

bool-Fin-2 : Fin 2 → bool
bool-Fin-2 (inl (inr star)) = true
bool-Fin-2 (inr star) = false

Fin-2-bool : bool → Fin 2
Fin-2-bool true = inl (inr star)
Fin-2-bool false = inr star

abstract
  is-retraction-Fin-2-bool : Fin-2-bool ∘ bool-Fin-2 ~ id
  is-retraction-Fin-2-bool (inl (inr star)) = refl
  is-retraction-Fin-2-bool (inr star) = refl

abstract
  is-section-Fin-2-bool : bool-Fin-2 ∘ Fin-2-bool ~ id
  is-section-Fin-2-bool true = refl
  is-section-Fin-2-bool false = refl

equiv-bool-Fin-2 : Fin 2 ≃ bool
pr1 equiv-bool-Fin-2 = bool-Fin-2
pr2 equiv-bool-Fin-2 =
  is-equiv-is-invertible
    ( Fin-2-bool)
    ( is-section-Fin-2-bool)
    ( is-retraction-Fin-2-bool)

The type of booleans is finite

is-finite-bool : is-finite bool
is-finite-bool = is-finite-equiv equiv-bool-Fin-2 (is-finite-Fin 2)

number-of-elements-bool : number-of-elements-is-finite is-finite-bool ＝ 2
number-of-elements-bool =
  inv
    ( compute-number-of-elements-is-finite
      ( 2 , equiv-bool-Fin-2)
      ( is-finite-bool))

bool-Finite-Type : Finite-Type lzero
pr1 bool-Finite-Type = bool
pr2 bool-Finite-Type = is-finite-bool

Recent changes