Source

Probability / EventAlgebra.agda

Full commit
open import Level
open import Algebra
module EventAlgebra (algebra : BooleanAlgebra zero zero) where
  open import Relation.Binary
  module BA = BooleanAlgebra algebra  renaming (
       Carrier to Event ;
       ⊤ to Ω ;
       ⊥ to ∅ ;
       _∧_ to _∩_ ; 
       _∨_ to _∪_ ; 
       ¬_ to ∁_)
  open BA public
  import Algebra.Props.BooleanAlgebra as B
  import Algebra.FunctionProperties as FP
  open import Algebra.Structures
  open FP _≈_
  abstract
    _∖_ : Op₂ Event
    a ∖ b = a ∩ ∁ b
    
--    _⊆_ : Rel Event zero
--    e₁ ⊆ e₂ = {!!}

  _disj_ : Rel Event zero
  e₁ disj e₂ = e₁ ∩ e₂ ≈ ∅

  ∪-monoid : Monoid zero zero
  ∪-monoid = record { -- TODO заиспользовать имеющийся моноид
      Carrier = Event; _≈_ = _≈_; _∙_ = _∪_; ε = ∅; 
      isMonoid = IsCommutativeSemiring.+-isMonoid (B.∨-∧-isCommutativeSemiring algebra) }