{-# OPTIONS --without-K --safe #-}

module DepthComonads.Bool where

open import DepthComonads.Level
open import Agda.Builtin.Bool using (Bool; true; false) public

bool : ∀ {ℓ} {P : Bool → Type ℓ} (f : P false) (t : P true) → (x : Bool) → P x
bool f t = λ { false → f ; true → t }
{-# INLINE bool #-}

bool′ : A → A → Bool → A
bool′ = bool
{-# INLINE bool′ #-}

not : Bool → Bool
not = bool′ true false

infixl  _or_
_or_ : Bool → Bool → Bool
x or y = bool′ y true x

infixl  _and_
_and_ : Bool → Bool → Bool
x and y = bool′ false y x

infixr  if_then_else_
if_then_else_ : ∀ {a} {A : Type a} → Bool → A → A → A
if p then x else y = bool y x p
{-# INLINE if_then_else_ #-}

open import DepthComonads.Unit
open import DepthComonads.Empty

T : Bool → Type
T = bool′ ⊥ ⊤

open import DepthComonads.Path

true≢false : true ≢ false
true≢false p = subst T p tt

false≢true : false ≢ true
false≢true p = true≢false (sym p)