Source

Probability / Numbers.agda

Full commit
open import Algebra
module Numbers  where
open import Level
open import Relation.Binary
record Nums  : Setwhere
  field
    commRing : CommutativeRing zero zero
  module CR = CommutativeRing commRing hiding (zero) renaming (Carrier to Num)
  open CR
  field
    _≤_ : Rel Num _
    partialOrder : IsTotalOrder _≈_ _≤_
  module TO = IsTotalOrder partialOrder hiding (isEquivalence ; refl ; reflexive ; trans) 
  open TO
  0≤_ : Num  Set 
  0≤_ n = 0# ≤ n
  field
    0≤b→a≤a+b :  a  {b}  0≤ b  a ≤ (a + b)
    0≤1 : 01#

  open TO public
  open CR public