diff --git a/references.bib b/references.bib
index f104f1a31a..e3c872f78d 100644
--- a/references.bib
+++ b/references.bib
@@ -101,6 +101,14 @@ @misc{Awodey22
   keywords      = {Mathematics - Category Theory, Mathematics - Logic},
 }
 
+@misc{Babai00,
+  title         = {Finite Probablity Spaces},
+  author        = {Babai, L\'aszl\'o},
+  year          = 2000,
+  month         = apr,
+  url           = {https://people.cs.uchicago.edu/~laci/reu02/prob.pdf},
+}
+
 @article{BauerTaylor2009,
   title         = {The {{Dedekind}} Reals in Abstract {{Stone}} Duality},
   author        = {Bauer, Andrej and Taylor, Paul},
diff --git a/src/finite-probability-theory.lagda.md b/src/finite-probability-theory.lagda.md
new file mode 100644
index 0000000000..33a121fc7d
--- /dev/null
+++ b/src/finite-probability-theory.lagda.md
@@ -0,0 +1,11 @@
+# Finite probability theory
+
+```agda
+module finite-probability-theory where
+
+open import finite-probability-theory.expected-value-real-random-variables-finite-probability-spaces public
+open import finite-probability-theory.finite-probability-spaces public
+open import finite-probability-theory.positive-distributions-on-finite-types public
+open import finite-probability-theory.probability-distributions-on-finite-types public
+open import finite-probability-theory.real-random-variables-finite-probability-spaces public
+```
diff --git a/src/finite-probability-theory/expected-value-real-random-variables-finite-probability-spaces.lagda.md b/src/finite-probability-theory/expected-value-real-random-variables-finite-probability-spaces.lagda.md
new file mode 100644
index 0000000000..39c4bdd60d
--- /dev/null
+++ b/src/finite-probability-theory/expected-value-real-random-variables-finite-probability-spaces.lagda.md
@@ -0,0 +1,80 @@
+# Expected value of real random variables in finite probability spaces
+
+```agda
+module finite-probability-theory.expected-value-real-random-variables-finite-probability-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import finite-probability-theory.finite-probability-spaces
+open import finite-probability-theory.positive-distributions-on-finite-types
+open import finite-probability-theory.probability-distributions-on-finite-types
+open import finite-probability-theory.real-random-variables-finite-probability-spaces
+
+open import foundation.dependent-pair-types
+open import foundation.empty-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.inhabited-types
+open import foundation.propositions
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import group-theory.sums-of-finite-families-of-elements-abelian-groups
+
+open import real-numbers.addition-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.multiplication-real-numbers
+open import real-numbers.positive-real-numbers
+open import real-numbers.rational-real-numbers
+open import real-numbers.strict-inequality-real-numbers
+
+open import univalent-combinatorics.finite-types
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "expected value" Disambiguation="of a real random variable in a finite probability space" Agda=expected-value-real-random-variable-Finite-Probability-Space}}
+of a
+[real random variable](finite-probability-theory.real-random-variables-finite-probability-spaces.md)
+`X` in a
+[finite probability space](finite-probability-theory.finite-probability-spaces.md)
+`(Ω , Pr)` is the
+[sum](group-theory.sums-of-finite-families-of-elements-abelian-groups.md)
+
+$$
+  ∑_{x ∈ Ω} X(x)\operatorname{Pr}(x).
+$$
+
+Our definition follows Definition 2.2 of {{#cite Babai00}}.
+
+## Definitions
+
+### Expected value of a real random variable in a finite probability space
+
+```agda
+module _
+  {l : Level} (Ω : Finite-Probability-Space l)
+  (X : real-random-variable-Finite-Probability-Space Ω)
+  where
+
+  expected-value-real-random-variable-Finite-Probability-Space : ℝ lzero
+  expected-value-real-random-variable-Finite-Probability-Space =
+    sum-finite-Ab
+      ( abelian-group-add-ℝ-lzero)
+      ( finite-type-Finite-Probability-Space Ω)
+      ( λ x →
+        mul-ℝ
+          ( X x)
+          ( real-distribution-Finite-Probability-Space Ω x))
+```
+
+## References
+
+{{#bibliography}}
diff --git a/src/finite-probability-theory/finite-probability-spaces.lagda.md b/src/finite-probability-theory/finite-probability-spaces.lagda.md
new file mode 100644
index 0000000000..8ee8cb3520
--- /dev/null
+++ b/src/finite-probability-theory/finite-probability-spaces.lagda.md
@@ -0,0 +1,157 @@
+# Finite probability spaces
+
+```agda
+module finite-probability-theory.finite-probability-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import finite-probability-theory.positive-distributions-on-finite-types
+open import finite-probability-theory.probability-distributions-on-finite-types
+
+open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.empty-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.inhabited-types
+open import foundation.propositions
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import group-theory.sums-of-finite-families-of-elements-abelian-groups
+
+open import logic.propositional-double-negation-elimination
+
+open import real-numbers.addition-real-numbers
+open import real-numbers.apartness-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.positive-real-numbers
+open import real-numbers.rational-real-numbers
+open import real-numbers.strict-inequality-real-numbers
+
+open import univalent-combinatorics.finite-types
+open import univalent-combinatorics.inhabited-finite-types
+```
+
+</details>
+
+## Idea
+
+A {{#concept "finite probability space" Agda=Finite-Probability-Space}} is a
+[finite type](univalent-combinatorics.finite-types.md) equipped with a
+[probability distribution](finite-probability-theory.probability-distributions-on-finite-types.md).
+
+Any finite probability space is [inhabited](foundation.inhabited-types.md).
+
+Our definitions follows {{#cite Babai00}}, except, there it is assumed that the
+underlying type is [nonempty](foundation-core.empty-types.md), but this follows
+from the condition of having
+[total measure](finite-probability-theory.positive-distributions-on-finite-types.md)
+equal to 1.
+
+## Definitions
+
+### Finite probability spaces
+
+```agda
+Finite-Probability-Space : (l : Level) → UU (lsuc l)
+Finite-Probability-Space l =
+  Σ ( Finite-Type l)
+    ( probability-distribution-Finite-Type)
+
+module _
+  {l : Level} (Ω : Finite-Probability-Space l)
+  where
+
+  finite-type-Finite-Probability-Space : Finite-Type l
+  finite-type-Finite-Probability-Space = pr1 Ω
+
+  type-Finite-Probability-Space : UU l
+  type-Finite-Probability-Space =
+    type-Finite-Type finite-type-Finite-Probability-Space
+
+  is-finite-type-Finite-Probability-Space :
+    is-finite type-Finite-Probability-Space
+  is-finite-type-Finite-Probability-Space =
+    is-finite-type-Finite-Type finite-type-Finite-Probability-Space
+
+  distribution-Finite-Probability-Space :
+    positive-distribution-Finite-Type finite-type-Finite-Probability-Space
+  distribution-Finite-Probability-Space = pr1 (pr2 Ω)
+
+  real-distribution-Finite-Probability-Space :
+    type-Finite-Probability-Space → ℝ lzero
+  real-distribution-Finite-Probability-Space =
+    real-positive-distribution-Finite-Type
+      ( finite-type-Finite-Probability-Space)
+      ( distribution-Finite-Probability-Space)
+
+  eq-one-total-measure-distribution-Finite-Probability-Space :
+    ( total-measure-positive-distribution-Finite-Type
+      ( finite-type-Finite-Probability-Space)
+      ( distribution-Finite-Probability-Space)) ＝
+    one-ℝ
+  eq-one-total-measure-distribution-Finite-Probability-Space =
+    pr2 (pr2 Ω)
+```
+
+## Properties
+
+### A finite probability space is nonempty
+
+```agda
+module _
+  {l : Level} (Ω : Finite-Probability-Space l)
+  where
+
+  is-nonempty-type-Finite-Probability-Space :
+    is-nonempty (type-Finite-Probability-Space Ω)
+  is-nonempty-type-Finite-Probability-Space =
+    zero-is-not-one-ℝ ∘ absurd-is-empty-Finite-Probability-Space
+    where
+
+    absurd-is-empty-Finite-Probability-Space :
+      is-empty (type-Finite-Probability-Space Ω) →
+      zero-ℝ ＝ one-ℝ
+    absurd-is-empty-Finite-Probability-Space H =
+      ( inv
+        ( is-zero-total-measure-positive-distribution-is-empty-Finite-Type
+          ( finite-type-Finite-Probability-Space Ω)
+          ( distribution-Finite-Probability-Space Ω)
+          ( H))) ∙
+      ( eq-one-total-measure-distribution-Finite-Probability-Space Ω)
+```
+
+### A finite probability space is inhabited
+
+```agda
+module _
+  {l : Level} (Ω : Finite-Probability-Space l)
+  where
+
+  is-inhabited-type-Finite-Probability-Space :
+    is-inhabited (type-Finite-Probability-Space Ω)
+  is-inhabited-type-Finite-Probability-Space =
+    prop-double-negation-elim-is-inhabited-or-empty
+      ( is-inhabited-or-empty-is-finite
+        ( is-finite-type-Finite-Probability-Space Ω))
+      ( is-nonempty-type-Finite-Probability-Space Ω)
+
+  inhabited-type-Finite-Probability-Space : Inhabited-Type l
+  inhabited-type-Finite-Probability-Space =
+    ( type-Finite-Probability-Space Ω ,
+      is-inhabited-type-Finite-Probability-Space)
+
+  inhabited-finite-type-Finite-Probability-Space : Inhabited-Finite-Type l
+  inhabited-finite-type-Finite-Probability-Space =
+    ( finite-type-Finite-Probability-Space Ω ,
+      is-inhabited-type-Finite-Probability-Space)
+```
+
+## References
+
+{{#bibliography}}
diff --git a/src/finite-probability-theory/positive-distributions-on-finite-types.lagda.md b/src/finite-probability-theory/positive-distributions-on-finite-types.lagda.md
new file mode 100644
index 0000000000..88642b65f6
--- /dev/null
+++ b/src/finite-probability-theory/positive-distributions-on-finite-types.lagda.md
@@ -0,0 +1,95 @@
+# Positive distributions on finite types
+
+```agda
+module finite-probability-theory.positive-distributions-on-finite-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.empty-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import group-theory.sums-of-finite-families-of-elements-abelian-groups
+
+open import real-numbers.addition-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.positive-real-numbers
+open import real-numbers.rational-real-numbers
+
+open import univalent-combinatorics.finite-types
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "positive distribution" Disambiguation="on a finite type" Agda=positive-distribution-Finite-Type}}
+on a [finite type](univalent-combinatorics.finite-types.md) `Ω` is a function
+into the [positive real numbers](real-numbers.positive-real-numbers.md),
+`Pr : Ω → ℝ⁺`. We interpret the type `Ω` as the collection of _atomic events_,
+and `Pr(x)` as the (unnormalized) _probability_ that the atomic event `x` will
+occur. Note that for positive distributions no atomic event can be _impossible_
+since `Pr(x)` is always strictly greater than `0`. The **total measure** of a
+positive distribution `Pr` on a finite type `Ω` is the
+[sum](group-theory.sums-of-finite-families-of-elements-abelian-groups.md)
+
+$$
+  ∑_{x ∈ Ω}\operatorname{Pr}(x).
+$$
+
+## Definitions
+
+### Positive distributions on finite types
+
+```agda
+module _
+  {l : Level} (Ω : Finite-Type l)
+  where
+
+  positive-distribution-Finite-Type : UU (lsuc lzero ⊔ l)
+  positive-distribution-Finite-Type = type-Finite-Type Ω → ℝ⁺ lzero
+
+  real-positive-distribution-Finite-Type :
+    positive-distribution-Finite-Type → type-Finite-Type Ω → ℝ lzero
+  real-positive-distribution-Finite-Type Pr = real-ℝ⁺ ∘ Pr
+```
+
+### The total measure of a positive distribution on a finite type
+
+```agda
+module _
+  {l : Level} (Ω : Finite-Type l)
+  (Pr : positive-distribution-Finite-Type Ω)
+  where
+
+  total-measure-positive-distribution-Finite-Type : ℝ lzero
+  total-measure-positive-distribution-Finite-Type =
+    sum-finite-Ab
+      ( abelian-group-add-ℝ-lzero)
+      ( Ω)
+      ( real-positive-distribution-Finite-Type Ω Pr)
+```
+
+## Properties
+
+### The total measure of a positive distribution on an empty type is zero
+
+```agda
+module _
+  {l : Level} (Ω : Finite-Type l) (Pr : positive-distribution-Finite-Type Ω)
+  where
+
+  is-zero-total-measure-positive-distribution-is-empty-Finite-Type :
+    is-empty (type-Finite-Type Ω) →
+    total-measure-positive-distribution-Finite-Type Ω Pr ＝ zero-ℝ
+  is-zero-total-measure-positive-distribution-is-empty-Finite-Type H =
+    eq-zero-sum-finite-is-empty-Ab
+      ( abelian-group-add-ℝ-lzero)
+      ( Ω)
+      ( H)
+      ( real-positive-distribution-Finite-Type Ω Pr)
+```
diff --git a/src/finite-probability-theory/probability-distributions-on-finite-types.lagda.md b/src/finite-probability-theory/probability-distributions-on-finite-types.lagda.md
new file mode 100644
index 0000000000..c156d3165b
--- /dev/null
+++ b/src/finite-probability-theory/probability-distributions-on-finite-types.lagda.md
@@ -0,0 +1,81 @@
+# Probability distributions on finite types
+
+```agda
+module finite-probability-theory.probability-distributions-on-finite-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import finite-probability-theory.positive-distributions-on-finite-types
+
+open import foundation.empty-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.inhabited-types
+open import foundation.propositions
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import group-theory.sums-of-finite-families-of-elements-abelian-groups
+
+open import real-numbers.addition-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.positive-real-numbers
+open import real-numbers.rational-real-numbers
+
+open import univalent-combinatorics.finite-types
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "probability distribution" Disambiguation="on a finite type" Agda=probability-distribution-Finite-Type}}
+on a [finite type](univalent-combinatorics.finite-types.md) is a
+[positive distribution](finite-probability-theory.positive-distributions-on-finite-types.md)
+with total measure equal to 1.
+
+## Definition
+
+### The property of being a probability distribution on a finite type
+
+```agda
+module _
+  {l : Level} (Ω : Finite-Type l) (Pr : positive-distribution-Finite-Type Ω)
+  where
+
+  is-probability-distribution-prop-positive-distribution-Finite-Type :
+    Prop (lsuc lzero)
+  is-probability-distribution-prop-positive-distribution-Finite-Type =
+    Id-Prop
+      ( ℝ-Set lzero)
+      ( total-measure-positive-distribution-Finite-Type Ω Pr)
+      ( one-ℝ)
+
+  is-probability-distribution-positive-distribution-Finite-Type :
+    UU (lsuc lzero)
+  is-probability-distribution-positive-distribution-Finite-Type =
+    type-Prop is-probability-distribution-prop-positive-distribution-Finite-Type
+
+  is-prop-is-probability-distribution-Finite-Type :
+    is-prop is-probability-distribution-positive-distribution-Finite-Type
+  is-prop-is-probability-distribution-Finite-Type =
+    is-prop-type-Prop
+      is-probability-distribution-prop-positive-distribution-Finite-Type
+```
+
+### Probability distributions on finite types
+
+```agda
+module _
+  {l : Level} (Ω : Finite-Type l)
+  where
+
+  probability-distribution-Finite-Type : UU (lsuc lzero ⊔ l)
+  probability-distribution-Finite-Type =
+    type-subtype
+      ( is-probability-distribution-prop-positive-distribution-Finite-Type Ω)
+```
diff --git a/src/finite-probability-theory/real-random-variables-finite-probability-spaces.lagda.md b/src/finite-probability-theory/real-random-variables-finite-probability-spaces.lagda.md
new file mode 100644
index 0000000000..1ad7d9e065
--- /dev/null
+++ b/src/finite-probability-theory/real-random-variables-finite-probability-spaces.lagda.md
@@ -0,0 +1,101 @@
+# Real random variables in finite probability spaces
+
+```agda
+module finite-probability-theory.real-random-variables-finite-probability-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import finite-probability-theory.finite-probability-spaces
+open import finite-probability-theory.positive-distributions-on-finite-types
+open import finite-probability-theory.probability-distributions-on-finite-types
+
+open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.empty-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.inhabited-types
+open import foundation.propositions
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import group-theory.sums-of-finite-families-of-elements-abelian-groups
+
+open import real-numbers.addition-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.multiplication-real-numbers
+open import real-numbers.positive-real-numbers
+open import real-numbers.rational-real-numbers
+open import real-numbers.strict-inequality-real-numbers
+
+open import univalent-combinatorics.equality-finite-types
+open import univalent-combinatorics.finite-types
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "real random variable" Disambiguation="in a finite probability space" Agda=real-random-variable-Finite-Probability-Space}}
+in a
+[finite probability space](finite-probability-theory.finite-probability-spaces.md)
+is a function from the underlying
+[finite type](univalent-combinatorics.finite-types.md) to
+[`ℝ`](real-numbers.dedekind-real-numbers.md).
+
+Our definition follows Definition 2.1 of {{#cite Babai00}}.
+
+## Definitions
+
+### Real random variables in a finite probability space
+
+```agda
+module _
+  {l : Level} (Ω : Finite-Probability-Space l)
+  where
+
+  real-random-variable-Finite-Probability-Space : UU (lsuc lzero ⊔ l)
+  real-random-variable-Finite-Probability-Space =
+    type-Finite-Probability-Space Ω → ℝ lzero
+```
+
+### Constant random variables in a finite probability space
+
+```agda
+module _
+  {l : Level} (Ω : Finite-Probability-Space l)
+  where
+
+  const-real-random-variable-Finite-Probablity-Space :
+    (x : ℝ lzero) → real-random-variable-Finite-Probability-Space Ω
+  const-real-random-variable-Finite-Probablity-Space x _ = x
+```
+
+### Atomic real random variables in a finite probability space
+
+```agda
+module _
+  {l : Level} (Ω : Finite-Probability-Space l)
+  (e : type-Finite-Probability-Space Ω)
+  where
+
+  atomic-real-random-variable-Finite-Probability-Space :
+    real-random-variable-Finite-Probability-Space Ω
+  atomic-real-random-variable-Finite-Probability-Space e' =
+    rec-coproduct
+      ( λ _ → one-ℝ)
+      ( λ _ → zero-ℝ)
+      ( has-decidable-equality-is-finite
+        ( is-finite-type-Finite-Probability-Space Ω)
+        ( e)
+        ( e'))
+```
+
+## References
+
+{{#bibliography}}
diff --git a/src/real-numbers/apartness-real-numbers.lagda.md b/src/real-numbers/apartness-real-numbers.lagda.md
index 023123e63e..9255585865 100644
--- a/src/real-numbers/apartness-real-numbers.lagda.md
+++ b/src/real-numbers/apartness-real-numbers.lagda.md
@@ -8,6 +8,7 @@ module real-numbers.apartness-real-numbers where
 
 ```agda
 open import foundation.apartness-relations
+open import foundation.coproduct-types
 open import foundation.disjunction
 open import foundation.empty-types
 open import foundation.function-types
@@ -17,11 +18,13 @@ open import foundation.large-apartness-relations
 open import foundation.large-binary-relations
 open import foundation.negated-equality
 open import foundation.negation
+open import foundation.propositional-truncations
 open import foundation.propositions
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import real-numbers.dedekind-real-numbers
+open import real-numbers.rational-real-numbers
 open import real-numbers.strict-inequality-real-numbers
 ```
 
@@ -107,3 +110,17 @@ nonequal-apart-ℝ : {l : Level} (x y : ℝ l) → apart-ℝ x y → x ≠ y
 nonequal-apart-ℝ x y =
   nonequal-apart-Large-Apartness-Relation large-apartness-relation-ℝ
 ```
+
+### Zero is apart from one
+
+```agda
+apart-zero-one-ℝ : apart-ℝ zero-ℝ one-ℝ
+apart-zero-one-ℝ = unit-trunc-Prop (inl le-zero-one-ℝ)
+```
+
+### Zero is not equal to one
+
+```agda
+zero-is-not-one-ℝ : zero-ℝ ≠ one-ℝ
+zero-is-not-one-ℝ = nonequal-apart-ℝ zero-ℝ one-ℝ apart-zero-one-ℝ
+```
diff --git a/src/real-numbers/strict-inequality-real-numbers.lagda.md b/src/real-numbers/strict-inequality-real-numbers.lagda.md
index a68d6e8cbd..e4586773eb 100644
--- a/src/real-numbers/strict-inequality-real-numbers.lagda.md
+++ b/src/real-numbers/strict-inequality-real-numbers.lagda.md
@@ -841,6 +841,17 @@ module _
             le-real-is-in-upper-cut-ℚ r y y<r)
 ```
 
+### Zero is strictly less than one
+
+```agda
+le-zero-one-ℝ : le-ℝ zero-ℝ one-ℝ
+le-zero-one-ℝ =
+  preserves-le-real-ℚ
+    ( zero-ℚ)
+    ( one-ℚ)
+    ( le-zero-one-ℚ)
+```
+
 ## References
 
 {{#bibliography}}