Chapter 180Optional

Dependent Probability and Fibred Measure

Prerequisites. Direct starred prerequisites: chapter 174. No later core chapter depends on this route.

Fix a two-point base $Z = {0, 1}$ and a family over it: $B (0) = {*}$ and $B (1) = {L, R}$ . Put a probability measure on each fibre: $μ_{0} (*) = 1$ and $μ_{1} (L) = μ_{1} (R) = 1 / 2$ . Substituting into the base is composing with a function into $Z$ : with $u : {a, b, c} \to Z$ given by $u (a) = 0$ , $u (b) = 1$ , $u (c) = 0$ , the family $u^{*} B$ has $(u^{*} B) (a) = {*}$ , $(u^{*} B) (b) = {L, R}$ , $(u^{*} B) (c) = {*}$ , and the reindexed measure $u^{*} μ$ assigns to each index the measure of its image. Substituting again along $v : {p, q} \to {a, b, c}$ with $v (p) = b$ and $v (q) = c$ gives $\begin{matrix} (u \circ v)^{*} μ : p \mapsto {L : \frac{1}{2}, R : \frac{1}{2}}, q \mapsto {* : 1}, \\ v^{*} (u^{*} μ) : p \mapsto {L : \frac{1}{2}, R : \frac{1}{2}}, q \mapsto {* : 1} . \end{matrix}$ The two printed maps are equal, entry by entry.

That they are equal is not a general fact about probability monads; it is a fact about this presentation of families. A family of spaces indexed by a base is usually presented by a display map $d : A \to Γ$ , and substitution along $θ : Δ \to Γ$ is a chosen pullback. Pullbacks are determined only up to isomorphism, so two ways of substituting twice agree up to a canonical isomorphism and not on the nose, and the isomorphisms must then be carried through every construction that follows — including the measures, which would agree only after transport. The equality displayed above would become an isomorphism, and the practical checker printing the two maps would have to compare them modulo a coercion.

The obstruction is therefore strictness, and the object that removes it is a presentation of families in which reindexing is defined by composition and is strictly functorial by construction. This chapter builds that presentation over quasi-Borel spaces, lifts measures and probability measures into it, proves the reindexing laws as commuting squares, and states the conditional expectation results whose hypotheses the fibred setting makes visible.

Convention 180.1 — Imported interface ¶

From chapter 174 this chapter uses quasi-Borel spaces (definition 174.6), their products and exponentials (proposition 174.8, proposition 174.10), measures on them (definition 174.12), and the probability monad with its laws (theorem 174.16, proposition 174.17); through that chapter it uses $PMK$ -map and $PMK$ -bind of convention 172.27. It uses no program logic, no inference transformation, and no result about SFPC.

Referenced from 2 locations

Dependent Probability and Fibred Measure

Reindexing, computed before it is abstracted

Definition 180.2 — Families of measures and their reindexing ¶

Let $Γ$ be a set. A family of measure spaces over $Γ$ is an assignment $γ \mapsto A_{γ}$ of a measurable space to each index, together with a measure $μ_{γ}$ on $A_{γ}$ . For $θ : Δ \to Γ$ , the reindexed family is $(θ^{*} A)_{δ} = A_{θ (δ)}$ with $(θ^{*} μ)_{δ} = μ_{θ (δ)}$ .

Referenced from 3 locations

Dependent Probability and Fibred Measure

Proposition 180.3 — Strict functoriality ¶

For $φ : Ξ \to Δ$ and $θ : Δ \to Γ$ , $\begin{matrix} φ^{*} (θ^{*} A) = (θ \circ φ)^{*} A, \\ φ^{*} (θ^{*} μ) = (θ \circ φ)^{*} μ, \\ {id}^{*} A = A, \\ {id}^{*} μ = μ, \end{matrix}$ as equalities of families, not merely as isomorphisms.

Referenced from 9 locations

Dependent Probability and Fibred Measure

Proof of Proposition 180.3 — Strict functoriality

Proof. Evaluate at an index: $(φ^{*} (θ^{*} A))_{ξ} = (θ^{*} A)_{φ (ξ)} = A_{θ (φ (ξ))} = ((θ \circ φ)^{*} A)_{ξ}$ , and the same computation with $μ$ in place of $A$ . The identity laws are immediate. ◻

Example 180.4 — The opening calculation, as an instance ¶

Take $Γ = Z$ , $A$ and $μ$ as in the chapter opening, and $u, v$ as displayed. Proposition 180.3 gives $(u \circ v)^{*} μ = v^{*} (u^{*} μ)$ directly, and evaluating at $p$ and $q$ : $\begin{matrix} ((u \circ v)^{*} μ)_{p} = μ_{u (v (p))} = μ_{u (b)} = μ_{1} = {L : \frac{1}{2}, R : \frac{1}{2}}, \\ ((u \circ v)^{*} μ)_{q} = μ_{u (c)} = μ_{0} = {* : 1} . \end{matrix}$ No transport and no coercion appears. The equality is the one the practical checker of exercise 180.8 compares, and the general statement it instantiates is proposition 180.3.

Referenced from 4 locations

Dependent Probability and Fibred Measure

Remark 180.5 — What the display-map presentation would give instead ¶

Presenting the same data by the display map $d : \underset{γ}{∐} A_{γ} \to Γ$ and defining $θ^{*}$ as a chosen pullback yields, for two composable substitutions, a canonical isomorphism $φ^{*} (θ^{*} A) ≅ (θ \circ φ)^{*} A$ rather than an equality, because a pullback is determined only up to isomorphism. Every later construction — the measure, the conditional expectation, the interpretation of a dependent type — then carries a coherence obligation. Definition 180.2 avoids the obligation by defining reindexing as composition; the work of the next section is to carry that definition into the quasi-Borel setting, where a family must also record which functions of a real parameter count as random.

Referenced from 2 locations

Dependent Probability and Fibred Measure

Quasi-Borel families

Definition 180.6 — Quasi-Borel family ¶

Let $Γ$ be a quasi-Borel space with random elements $M_{Γ}$ . A quasi-Borel family over $Γ$ , written $Γ ⊢ A$ , is a family $(A_{γ})_{γ \in Γ}$ of sets together with, for each $υ \in M_{Γ}$ , a set $R_{A}^{υ} \subseteq \prod_{r \in R} A_{υ (r)}$ of fibred random elements, subject to three axioms mirroring definition 174.6:

constants: for a constant $υ = λ r . γ$ , every constant function $λ r . a$ with $a \in A_{γ}$ lies in $R_{A}^{υ}$ ;
precomposition: if $α \in R_{A}^{υ}$ and $f : R \to R$ is measurable, then $α \circ f \in R_{A}^{υ \circ f}$ ;
recombination: if $R = ⨄_{i} S_{i}$ is a countable Borel partition, $α_{i} \in R_{A}^{υ_{i}}$ , and $υ$ is the corresponding gluing of the $υ_{i}$ , then the gluing of the $α_{i}$ lies in $R_{A}^{υ}$ .

A map of families $(θ ⊢ f) : (Γ ⊢ A) \to (Δ ⊢ B)$ consists of a function $θ : Γ \to Δ$ with $θ \circ υ \in M_{Δ}$ for every $υ \in M_{Γ}$ , and a family of functions $f_{γ} : A_{γ} \to B_{θ (γ)}$ such that $f \circ α \in R_{B}^{θ \circ υ}$ for every $α \in R_{A}^{υ}$ .

Referenced from 4 locations

Dependent Probability and Fibred Measure

Example 180.7 — Constant and preimage families ¶

A quasi-Borel space $X$ gives the constant family $A_{γ} = X$ with $R_{A}^{υ} = M_{X}$ ; the axioms are those of definition 174.6. A morphism $d : A \to Γ$ gives the preimage family $d^{- 1} [γ] = {a ∣ d (a) = γ}$ with $R_{d^{- 1} [-]}^{υ}$ the random elements $β \in M_{A}$ with $d \circ β = υ$ , read as functions into the fibres. The first is how a closed type enters a dependent context; the second is how an ordinary display map is presented as a family.

Referenced from 3 locations

Dependent Probability and Fibred Measure

Definition 180.8 — Reindexing and comprehension ¶

For $θ : Γ \to Δ$ a morphism of quasi-Borel spaces and $Δ ⊢ B$ , define $Γ ⊢ B [θ]$ by $B [θ]_{γ} = B_{θ (γ)}, R_{B [θ]}^{υ} = R_{B}^{θ \circ υ} .$ For $Γ ⊢ A$ , define the comprehension $Γ . A = \underset{γ \in Γ}{∐} A_{γ}$ with random elements $M_{Γ . A} = {λ r . ⟨ υ (r), α (r) ⟩ | υ \in M_{Γ}, α \in R_{A}^{υ}},$ and let ${disp}_{A} : Γ . A \to Γ$ be the first projection.

Referenced from 2 locations

Dependent Probability and Fibred Measure

Proposition 180.9 — The family fibration is split, and comprehension is a morphism ¶

$B [θ]$ is a quasi-Borel family; reindexing is strictly functorial, $B [θ] [φ] = B [θ \circ φ]$ and $B [id] = B$ ; $Γ . A$ is a quasi-Borel space; and ${disp}_{A}$ is a morphism.

Referenced from 5 locations

Dependent Probability and Fibred Measure

Proof of Proposition 180.9 — The family fibration is split, and comprehension is a morphism

Proof. $B [θ]$ is a family. Constants: a constant $υ = λ r . γ$ has $θ \circ υ$ constant at $θ (γ)$ , so the constant functions into $B_{θ (γ)} = B [θ]_{γ}$ lie in $R_{B}^{θ \circ υ} = R_{B [θ]}^{υ}$ . Precomposition: $R_{B [θ]}^{υ \circ f} = R_{B}^{θ \circ υ \circ f}$ , which contains $α \circ f$ for $α \in R_{B}^{θ \circ υ}$ . Recombination: the gluing of $θ \circ υ_{i}$ is $θ \circ (gluing of υ_{i})$ , so the axiom for $B$ applies verbatim.

Strictness. $B [θ] [φ]_{ξ} = B [θ]_{φ (ξ)} = B_{θ (φ (ξ))} = B [θ \circ φ]_{ξ}$ , and $R_{B [θ] [φ]}^{υ} = R_{B}^{θ \circ φ \circ υ} = R_{B [θ \circ φ]}^{υ}$ . Both components are equal, so the families are equal; the identity case is the same computation.

Comprehension. The three axioms for $M_{Γ . A}$ follow from the corresponding axioms for $M_{Γ}$ and for $R_{A}$ , taken in pairs: a constant pair is a pair of constants; precomposition acts on both components; and a countable Borel gluing of pairs is the pair of gluings, which is where axiom (iii) of definition 180.6 is used. Finally ${disp}_{A} \circ λ r . ⟨ υ (r), α (r) ⟩ = υ \in M_{Γ}$ , so the display map is a morphism. ◻

Remark 180.10 — What splitness buys, stated exactly ¶

Proposition 180.9 is the fibred form of proposition 180.3: substitution into a dependent type is composition in the index, so iterated substitution is associative on the nose. This is the property that Ahman–Kammar–Møgelberg’s Theorem 13 states, along with the fibred equivalence between this presentation and the codomain fibration over quasi-Borel spaces — the two present the same families, but only the first is split. The chapter uses splitness, not the equivalence.

Referenced from 2 locations

Dependent Probability and Fibred Measure

Fibred measures

Definition 180.11 — The fibred distribution and probability families ¶

For $Γ ⊢ A$ define $Γ ⊢ D A$ by $(D A)_{γ} = D (A_{γ})$ , the measures on the fibre in the sense of definition 174.12, with $R_{D A}^{υ} = {α | \exists β \in R_{A}^{υ} . α = q_{D} \circ β},$ where $q_{D}$ sends a fibred random element to the measure it presents. Define $Γ ⊢ P A$ in the same way with probability measures. The unit and Kleisli extension are those of theorem 174.16 applied fibrewise: $η_{γ} (a) = δ_{a}$ and $(μ ≫ = f)_{γ} = μ_{γ} ≫ = f_{γ}$ .

Referenced from 2 locations

Dependent Probability and Fibred Measure

Proposition 180.12 — Reindexing commutes with the fibred monads ¶

For $θ : Γ \to Δ$ and $Δ ⊢ B$ , $D (B [θ]) = (D B) [θ], P (B [θ]) = (P B) [θ],$ as equalities of families, and the unit and Kleisli extension are preserved: $η_{B [θ]} = η_{B} [θ]$ and $(μ ≫ = f) [θ] = μ [θ] ≫ = f [θ]$ .

Referenced from 5 locations

Dependent Probability and Fibred Measure

Proof of Proposition 180.12 — Reindexing commutes with the fibred monads

Proof. On fibres, $D (B [θ])_{γ} = D (B_{θ (γ)}) = (D B)_{θ (γ)} = (D B) [θ]_{γ}$ . On fibred random elements, $R_{D (B [θ])}^{υ} = {q_{D} \circ β ∣ β \in R_{B [θ]}^{υ}} = {q_{D} \circ β ∣ β \in R_{B}^{θ \circ υ}} = R_{D B}^{θ \circ υ} = R_{(D B) [θ]}^{υ}$ . Both components agree, so the families are equal. The unit and Kleisli extension are defined fibrewise, and reindexing only renames fibres, so the two displayed equations hold at every index; the square $\begin{array}{r} index γ ⟼ θ (γ) commutes with μ_{-} ⟼ μ_{-} ≫ = f_{-} \end{array}$ because both operations act on the index and on the fibre independently. ◻

Example 180.13 — The fixture, fibrewise and in the fibration ¶

Discrete spaces are quasi-Borel spaces with all functions random, so the opening data is a quasi-Borel family with a fibred probability measure $Z ⊢ μ : P B$ . Proposition 180.12 gives $P (B [u \circ v]) = (P B) [u \circ v] = ((P B) [u]) [v]$ by proposition 180.9, and evaluating the fibred measure at the two indices reproduces example 180.4. The general finite statement proved in proposition 180.3 is thus an instance of the fibred one, and the checker’s structural equality of printed maps is legitimate exactly because the two sides are equal rather than isomorphic.

Referenced from 2 locations

Dependent Probability and Fibred Measure

Convention 180.14 — Imported fibred structure ¶

Theorem 33 of Ahman, Kammar and Møgelberg is imported at exactly this signature: $D$ and $P$ define commutative fibred monads on the category of quasi-Borel families, and the fibres of the distribution monad satisfy Kock’s axioms for synthetic measure theory, that is, for every countable set $I$ there are canonical isomorphisms $Γ ⊢ D (\underset{i \in I}{∐} A_{i}) ≅ \prod_{i \in I} D (A_{i}) .$ Proposition 180.12 proves the reindexing half locally; commutativity in each fibre is proposition 174.17; what the import supplies is that these fit together as fibred monads and that the countable coproduct isomorphisms exist at the fibred signature. The synthetic axioms are therefore consequences of the construction rather than postulates: the coproduct isomorphism is countable additivity, and commutativity is Tonelli’s theorem, as remark 174.24 recorded.

Referenced from 3 locations

Dependent Probability and Fibred Measure

Conditional expectation in the fibration

The fibred setting makes an observation map into a term $Γ ⊢ H : Ω ⟶ Θ$ between two families, and a conditional expectation into a term of a function type. Two statements are imported at their exact signatures; both are recorded with every hypothesis they carry.

Convention 180.15 — Externalisation ¶

Their Proposition 40: let $Γ ⊢ Ω$ and $Γ ⊢ Θ$ be quasi-Borel families, $Γ ⊢ μ : P Ω$ a fibred probability measure, and $Γ ⊢ H : Ω ⟶ Θ$ a fibred observation map. For each index $γ$ , let $B_{Ω_{γ}}$ and $B_{Θ_{γ}}$ be the $σ$ -algebras of the free measurable spaces on the fibres and let $G_{γ} = H_{γ}^{- 1} B_{Θ_{γ}} \subseteq B_{Ω_{γ}}$ . Then for integrable fibred random variables $Γ ⊢ f : L^{1} (Ω, μ)$ and $Γ ⊢ g : L^{1} (Θ, μ_{H})$ , $(\forall γ . g_{γ} = E_{μ_{γ}} [f ∣ H]) ⟺ (\forall γ . g_{γ} \circ H_{γ} = E_{μ_{γ}} [f_{γ} ∣ G_{γ}]),$ so the fibred notion and the classical sub- $σ$ -algebra notion agree index by index. What the import supplies is the passage between the two notions; the classical properties — almost sure uniqueness, linearity — then transfer through it. Almost sure uniqueness at a fixed index is the following argument, recorded here so that the chapter does not depend on it from elsewhere: if $g$ and $g^{'}$ both satisfy $\int_{H^{- 1} (A)} f d μ = \int_{A} g d μ_{H}$ for every measurable $A$ , then $\int_{A} (g - g^{'}) d μ_{H} = 0$ for every $A$ ; taking $A = {g > g^{'}}$ and then $A = {g^{'} > g}$ makes both sets $μ_{H}$ -null.

Referenced from 4 locations

Dependent Probability and Fibred Measure

Convention 180.16 — Measurable conditional expectation ¶

Their Theorem 41: if the observation family $Θ$ is separable, then conditional expectation is a dependent function in the fibration, $\begin{aligned} Γ ⊢ E_{-} [- ∣ -] : & (μ : P Ω) ⟶ (H : Ω ⟶ Θ) ⟶ Separable (Θ, μ_{H}) \\ ⟶ (f : L^{1} (Ω, μ)) ⟶ Σ g : L^{1} (Θ, μ_{H}) . g = E_{μ} [f ∣ H], \end{aligned}$ and in particular, when $Θ$ is a standard Borel space, the separability argument may be omitted. The hypotheses are exactly: separability of the observation family with respect to the pushforward measure $μ_{H}$ , and integrability of $f$ with respect to $μ$ . Their proof constructs the conditional expectation first for square-integrable variables, using a measurable Schauder basis of $L^{2} (Θ, μ_{H})$ and the projection $\sum_{i < k} ⟨ f, φ_{i} \circ H ⟩ \cdot φ_{i}$ , and then takes limits of $E_{μ} [f^{\pm} \land n ∣ H]$ for integrable variables; every stage is a term in context, which is what makes the result a dependent function rather than a family of choices.

Referenced from 3 locations

Dependent Probability and Fibred Measure

Remark 180.17 — Separability is not decorative ¶

Without separability the conditional expectation still exists at each fixed index — it is the Radon–Nikodym derivative of $A \mapsto \int_{H^{- 1} (A)} f d μ$ with respect to $μ_{H}$ — but only as a choice at that index, determined up to a null set by the uniqueness argument of convention 180.15. Assembling those choices into a single term requires that the choices be made measurably in the index, and that is what the separability hypothesis and the measurable Schauder basis provide. This is the exact point at which the dependent setting demands more than the fibrewise classical theory.

Referenced from 2 locations

Dependent Probability and Fibred Measure

Remark 180.18 — Semantic families are not a surface language ¶

Everything above is semantic: quasi-Borel families, fibred measures, and terms in context are objects of a fibration, and the notation $Γ ⊢ t : A$ names an element, not a derivation in a typed probabilistic programming language. No preservation, progress, inference, normalization, or implementation-correctness claim is made here for any surface syntax; such a claim would require a language, an operational semantics, and an interpretation theorem, none of which this chapter constructs. The martingale definition that the source derives — $E_{f \sim μ} [f t ∣ H_{t}] = f t$ for the restriction maps $H_{t}$ — is likewise a semantic statement in the fibration, not a typing rule.

Referenced from 2 locations

Dependent Probability and Fibred Measure

Exercise 180.1 ¶

★☆☆ Verify proposition 180.3 on the opening data with a third substitution $w : {s} \to {p, q}$ , $w (s) = p$ , by computing both $((u \circ v) \circ w)^{*} μ$ and $w^{*} (v^{*} (u^{*} μ))$ .

Referenced from 2 locations

Dependent Probability and Fibred Measure

Exercise 180.2 ¶

★★☆ For the display map $d : {(0, *), (1, L), (1, R)} \to {0, 1}$ of the opening example, write out the preimage family of example 180.7 and check that its fibred random elements satisfy the three axioms of definition 180.6.

Referenced from 2 locations

Dependent Probability and Fibred Measure

Exercise 180.3 ¶

★★☆ Compute $Γ . A$ and ${disp}_{A}$ for the opening family, and exhibit a random element of $Γ . A$ whose two components are a constant and a nonconstant map.

Referenced from 2 locations

Dependent Probability and Fibred Measure

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 180.4, then exercise 180.5, then the practical project exercise 180.8.

Exercise 180.4 ¶

★☆☆ Prove proposition 180.3 for arbitrary finite index sets, displaying the evaluation at a generic index, and state where the proof would break if reindexing were defined by a chosen pullback.

Referenced from 3 locations

Dependent Probability and Fibred Measure

Exercise 180.5 ¶

★★☆ Write out the proof of proposition 180.12 for the two substitutions of the chapter opening, displaying the fibred random elements on both sides at the index $p$ .

Referenced from 3 locations

Dependent Probability and Fibred Measure

Exercise 180.6 ¶

★★☆ Give two families that are isomorphic but not equal, arising from two different choices of pullback along the same substitution, and exhibit the coercion that a non-split presentation would require in example 180.4.

Referenced from 2 locations

Dependent Probability and Fibred Measure

Exercise 180.7 ¶

★★☆ For the opening family with $Θ_{γ} = {*}$ and $H$ the unique map, compute the fibred conditional expectation of a bounded $f$ and check the equivalence of convention 180.15 at both indices.

Referenced from 2 locations

Dependent Probability and Fibred Measure

Exercise 180.8 ¶

★★★ Practical project.fibred-reindexing-checker Build a checker for finite fibred reindexing. Its inputs are a finite base set with a finite family of finite fibres, an exact rational probability measure on each fibre, and a chain of substitutions given as explicit finite maps. Its outputs are the two normalized finite maps obtained by reindexing once along the composite and twice along the factors, printed as sorted association lists from index to fibre measure with reduced rational masses.

The invariant to maintain is that every printed fibre measure sums to exactly $1$ , that reindexing never renames fibre elements, and that the two printed maps are compared by structural equality of the normalized representation, not by numerical tolerance.

The concrete result is the pair of printed maps for the chapter’s fixture: base $Z = {0, 1}$ with $B (0) = {*}$ , $B (1) = {L, R}$ , $μ_{0} (*) = 1$ , $μ_{1} (L) = μ_{1} (R) = 1 / 2$ ; the substitutions $u : {a, b, c} \to Z$ with $u (a) = 0, u (b) = 1, u (c) = 0$ and $v : {p, q} \to {a, b, c}$ with $v (p) = b, v (q) = c$ . The acceptance test is decidable and exact: both $(u \circ v)^{*} μ$ and $v^{*} (u^{*} μ)$ must print exactly $p \mapsto {L : 1 / 2, R : 1 / 2}$ ; $q \mapsto {* : 1}$ , and the checker must report structural equality; it must additionally reject an input whose fibre masses sum to $3 / 4$ , naming the defective index, and reject a substitution whose codomain does not match the base, naming the offending point. The written solution proves the general finite functoriality of proposition 180.3 before appealing to the quasi-Borel construction of proposition 180.9, and the checker establishes neither convention 180.14 nor convention 180.16.

Referenced from 4 locations