Source

Probability / OrderedBooleanAlgebra.agda

open import Level
open import Algebra
module OrderedBooleanAlgebra (algebra : BooleanAlgebra zero zero) where
  open import Relation.Binary
  open BooleanAlgebra algebra public renaming (
       Carrier to Event ;
       ⊤ to Ω ;
       ⊥ to ∅ ;
       _∧_ to _∩_ ; 
       _∨_ to _∪_)
  import Algebra.Props.BooleanAlgebra as B
  open B algebra 
  open Poset poset public hiding (_≈_ ; isEquivalence ; refl ; reflexive ; trans) renaming (_≤_ to _⊆_)