{-# OPTIONS --rewriting #-}

open import Agda.Primitive using (Level;lsuc;_⊔_;lzero)
open import Lib
open import Interval
open import Proposition
open import Cofibs
open import Kan

module Bool where

  data Bool {l : Level} : Set l where
    true : Bool
    false : Bool

  decBool : {l : Level} (x y : Bool{l}) → (x == y) ∨ ((x == y) → ⊥{l})
  decBool true true = inl id
  decBool true false = inr (\ ())
  decBool false true = inr (\ ())
  decBool false false = inl id