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

module Relation.Binary.Bool where

open import Prelude

-- record TotalOrder {e} (E : Type e) : Type e where
--   field
--     _≤?_ : E → E → Bool

--   _≤_ : E → E → Type