    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- The type for booleans and some operations
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Data.Bool.Base where

    open import Data.Unit.Base using (⊤)
    open import Data.Empty using (⊥)
    open import Level using (Level)

    private
      variable
        a : Level
        A : Set a

    ------------------------------------------------------------------------
    -- The boolean type

    open import Agda.Builtin.Bool public

    ------------------------------------------------------------------------
    -- Relations

    infix 4 _≤_ _<_

    data _≤_ : Bool → Bool → Set where
      f≤t : false ≤ true
      b≤b : ∀ {b} → b ≤ b

    data _<_ : Bool → Bool → Set where
      f<t : false < true

    ------------------------------------------------------------------------
    -- Boolean operations

    infixr 6 _∧_
    infixr 5 _∨_ _xor_

    not : Bool → Bool
    not true  = false
    not false = true

    _∧_ : Bool → Bool → Bool
    true  ∧ b = b
    false ∧ b = false

    _∨_ : Bool → Bool → Bool
    true  ∨ b = true
    false ∨ b = b

    _xor_ : Bool → Bool → Bool
    true  xor b = not b
    false xor b = b

    ------------------------------------------------------------------------
    -- Conversion to Set

    -- A function mapping true to an inhabited type and false to an empty
    -- type.
    T : Bool → Set
    T true  = ⊤
    T false = ⊥

    ------------------------------------------------------------------------
    -- Other operations

    infix 0 if_then_else_

    if_then_else_ : Bool → A → A → A
    if true  then t else f = t
    if false then t else f = f