Fibrations: Dependent views and type-varying data

A14Prose proofWhen the type of data depends on where you stand.

For a large class of cases—though not for all—in which we employ the word "meaning," it can be defined thus: the meaning of a word is its use in the language.
— Ludwig Wittgenstein, Philosophical Investigations §43 (1953)

This chapter formalizes context-dependent predicates as fibrations, defining Anchor A14: a fibration p : E -> B equipped with pullback functors that re-index types along context refinements, subject to identity and composition laws. Where the sheaf condition of Chapter 11 handles gluing of claims within a fixed type, A14 addresses the prior question of how the type itself varies across contexts. The relationship between fibrations and dependent type theory is made explicit, and T8 (Uncertainty/Value) is resolved by recognizing predicates like "best" and "affordable" as families indexed over context parameters. The worked examples and failure modes treated here elaborate the formal infrastructure underlying the narrative in Vol I, Chapter 6 ("Evidence without Custody").

The Problem with "Best"

A user asks: "Find me the best dress." The system returns candidates. A second user, with a different budget, different occasion, different aesthetic, receives the same ranking. The system has committed an error, but not a factual one—it has committed a type error.

"Best" has no meaning until you specify the context. Best for what budget? Best for what occasion? Best according to whose aesthetic? The system treated "best" as a flat predicate when it is actually fibered: its type depends on where you stand.

Consider three examples:

Best restaurant depends on (diet, cuisine preference, budget). A vegan seeking fine dining under $50 and a carnivore seeking casual under $20 are asking different questions. The system that returns the same ranking has confused them.

Affordable wedding dress vs affordable cocktail dress. The budget thresholds differ by occasion. A $3,000 dress is affordable for a wedding, unaffordable for a cocktail party. "Affordable" is not one predicate; it is a family of predicates indexed by occasion.

Compatible software package depends on (OS version, existing dependencies). A package compatible with Ubuntu 22.04 and Python 3.11 may be incompatible with CentOS 7 and Python 3.6. "Compatible" lives in a fiber over the system configuration.

These are not edge cases. Many system predicates are fibered over context. Treating them as flat is a category error: the predicate has no well-defined meaning without either parameters or an explicit default context.

What Is a Fiber?

Imagine a base space B where each point is a context: a combination of parameters. Formally, think of B as a poset (or category) of contexts ordered by refinement: b′ → b means "b′ is more specific than b." Over each point b ∈ B, there is a "fiber" E_b containing the types, predicates, and scoring functions that make sense in that context.

Example

Base B = (budget, occasion) with budget ∈ low/medium/high and occasion ∈ casual/formal/wedding.

Fiber over (low, casual) contains predicates like affordable_casual, suitable_for_brunch.
Fiber over (high, wedding) contains predicates like within_budget_for_wedding, formal_enough.

The predicates are literally different objects in different fibers. You cannot compare "affordable" in one fiber to "affordable" in another without first specifying how they relate.

This is not relativism—the fibers are structured, with maps between them, and that structure is called a fibration.

Remark(Intuition: The Shadow on the Floor)

A complex 3D object—say, a sculpture—casts a shadow on the floor. The shadow is 2D: simpler, flatter, missing information.

The shadow is the base: a simplified projection of reality.
The sculpture is the total space: the rich, complete object.
The projection is the map from total to base: how the sculpture produces its shadow.

Here's the problem: many different sculptures can cast the same shadow. A sphere and a cylinder viewed from above both cast circular shadows. If you only see the shadow, you cannot know which object produced it.

Lifting is the attempt to reconstruct the sculpture from its shadow. When lifting is well-defined, you can move from the simple representation back to the rich one. When it's ambiguous, you're stuck guessing.

This is why AI systems hallucinate. A language model sees tokens—shadows of meaning. Many different intentions, contexts, and truths can produce the same token sequence. The model "lifts" from tokens to meaning, but the lifting is ambiguous. It guesses, and sometimes guesses wrong.

A fibration structures this relationship. It says: here is the base (contexts), here is the total space (context-dependent predicates), and here is how to lift correctly when lifting is possible. The mathematics doesn't eliminate ambiguity—it makes the ambiguity explicit and tractable.

Don't confuse restriction and pullback:

Restriction (Chapter 10, presheaf): Take a claim and see what survives in a refined context. The type stays the same; you are narrowing scope.
Pullback (Chapter 12, fibration): Take the type itself and re-index it to a refined context. The type changes.

Restriction is about claims within a fixed type. Pullback is about re-indexing types across contexts. The distinction matters because restricting claims (A13's world) and reindexing types (A14's world) are different operations.

The Reindexing Property

A14

A Grothendieck fibration(Grothendieck 1971, Exposé VI)(Jacobs 1999, ch. 1) is a functor $p : \mathbf{E} \to \mathbf{B}$ such that for every object $e \in \mathbf{E}$ with $p(e) = b$ and every morphism $f : b' \to b$ in $\mathbf{B}$ , there exists a cartesian lift $\bar{f} : e' \to e$ in $\mathbf{E}$ with $p(\bar{f}) = f$ .

Cartesian means $\bar{f}$ is universal among lifts: for any $g : e'' \to e$ in $\mathbf{E}$ with $p(g) = f \circ h$ for some $h : p(e'') \to b'$ , there exists a unique $k : e'' \to e'$ with $\bar{f} \circ k = g$ and $p(k) = h$ .

The fibration determines pullback (reindexing) functors: for each $f : b' \to b$ , a functor $f^* : \mathbf{E}_b \to \mathbf{E}_{b'}$ (where $\mathbf{E}_b := p^{-1}(b)$ is the fiber over $b$ ) satisfying:

$\mathrm{id}^* \cong \mathrm{id}$ (pulling back along identity does nothing)
$(g \circ f)^* \cong f^* \circ g^*$ (pulling back along a composition is composing pullbacks, up to coherent isomorphism)

These isomorphisms satisfy the cleavage coherence conditions(Jacobs 1999, §1.2): the associator and unitor natural isomorphisms compose consistently (Mac Lane's pentagon and triangle).

If you have a predicate or scoring function valid in context B, and you refine the context (B′ is more specific than B), you can pull back the predicate to the refined context. The predicate does not disappear just because you zoomed in.

Engineering reading: A fibered predicate is a versioned function bundle keyed by context. The bundle contains score_fn, ordering (or decision rule), and invariants. Reindexing is the rule for specializing it as context gains parameters.

Store it as a first-class object: PredicateBundle(ctx_schema, score_fn, decision_rule, invariants, provenance, version). Pullback is a deterministic compiler from ctx_schema to a refinement.

Without structured pullback, predicates would be stranded in their original contexts. Refining context would break everything. Pullback says: refinement is well-behaved and compositional.

Example

In a build system, let B = (OS, compiler_version).

Predicate "compiles_successfully" lives over (Linux, gcc-12)
At this coarse context, it means "CI green on any Linux / gcc-12 configuration"
Refinement: (Ubuntu_22.04, gcc-12.2.1) → (Linux, gcc-12)
After pullback, it means "CI green on Ubuntu 22.04 / gcc-12.2.1 specifically"

The predicate survives refinement because the pullback functor carries it along. The meaning specializes as the context gains parameters.

Dependent Types

The fibration picture is exactly what dependent type theory formalizes(Martin-Löf 1984)(Jacobs 1999, ch. 4–5).

Γ ⊢ A type: In context Γ, the type A is well-formed(Smith 1990, ch. 1).

This is the fibration:

Γ is a point in the base (a context)
A is an object in the fiber over Γ
"Γ ⊢ A type" means A ∈ E_Γ

For systems, the consequence is direct:

"affordable" is not a type. "affordable in context (budget=X, occasion=Y)" is a type.
Dependent types make the context explicit in the type system.
Systems that lack dependent types must simulate this with ad-hoc parameter passing.

The ad-hoc approach works until you need to compose, compare, or version these predicates across contexts. Then it breaks.

Example

Non-dependent (flat) signature:

affordable : Dress → Bool

This is wrong. What budget? The predicate is underspecified.

Dependent (fibered) signature:

affordable : (ctx : Context) → Dress → Bool_ctx

The second signature makes the dependency explicit. The first hides it and hopes.

Worked Example: "Affordable Wedding Dress"

Setup:

Base B = (budget, occasion)
"Affordable" is a family of scoring functions indexed by B; define affordable_γ(x) := price(x) ≤ budget_γ
$\text{affordable}_{(5000, \text{wedding})}(x)$ means price(x) ≤ 5000
$\text{affordable}_{(200, \text{casual})}(x)$ means price(x) ≤ 200

Query: "Find affordable wedding dresses."

System behavior (fibered):

Extract user context: (budget=5000, occasion=wedding)
Identify fiber: predicates valid in that context
Evaluate $\text{affordable}_{(5000, \text{wedding})}(\text{dress})$ for each dress
Return results scoped to context

What goes wrong without fibrations:

System has a flat "affordable" predicate calibrated to average budget
User with $5000 wedding budget gets items marked "not affordable" (above average threshold)
System has committed a type error: it evaluated a fibered predicate as if it were flat

Refinement scenario:

User refines context: (budget=5000, occasion=wedding, style=boho)
Pullback: $\text{affordable}_{(5000, \text{wedding})}$ pulls back to $\text{affordable}_{(5000, \text{wedding}, \text{boho})}$
Additional predicates become available: fits_boho_aesthetic

The pullback functor carries the predicate along as context refines.

Relationship to Sheaves

A13 (sheaf condition) tells you how to glue claims that have the same type. A14 (fibration) tells you how types vary across contexts. Together: you can glue fibered predicates if their pullbacks to a common refinement agree.

A sheaf F on site (C, J) assigns values to each context U
A dependent sheaf (or stack(Johnstone 2002, Part C)) assigns types to each context U, and values are sections of those types
The fibration is the type-assignment; the sheaf condition applies fiberwise

If "affordable" is fibered over (budget, occasion), then gluing affordable claims across views requires:

Both views agree on the base point (same budget, same occasion), OR
There exists a common refinement in the base where both types pull back, and the pulled-back claims match

This is why "affordable for Alice" and "affordable for Bob" cannot be directly merged without knowing their contexts. The claims live in different fibers. Merging requires either agreeing on a base point or finding a common refinement.

Failure Modes

Type collapse: Treating fibered predicates as flat. The system asks "Is this affordable?" without specifying context, as if "affordable" were a property of the item alone. It is not. The question is ill-typed.

Context smuggling: Implicitly assuming a context without declaring it. "The best dress" secretly means "best for some default user." The default is a hidden parameter. When different users get the same ranking, the system has smuggled a context.

Pullback failure: Refining context breaks predicates because the system did not implement proper pullback. The user zooms in, and the predicate vanishes or returns nonsense.

Fiber confusion: Mixing objects from different fibers. "Alice's affordable and Bob's affordable are both true" does not mean the items are affordable in some shared sense. The predicates are different and cannot be conjoined without first specifying how they relate.

T8 Formalized

T8 (Uncertainty/Value) is the touchstone for non-factual targets: "best," "relevant," "preferred." These are not factual in the way "color is blue" is factual. They are dependent predicates.

"Best" is not a single predicate but a family of scoring functions indexed by context:

\text{score}_\gamma : \text{Item} \to \mathbb{R} \quad \text{and} \quad \preceq_\gamma \text{ an ordering}

where γ = (budget, occasion, style, ...). "Best" is then the maximal elements under ⪯_γ. If you want a Bool predicate, derive it: best_γ(x) := x ∈ TopK_γ.

The honest system response:

Query: "Is this the best dress?"

Response: "Best relative to what context? Please specify (budget, occasion, style preference, ...)."

Or, if context is provided:

Query: "Is this the best dress for a beach wedding under $1000?"

Response: "In context (budget=1000, occasion=beach_wedding), dress X ranks highest on the composite metric defined for that fiber."

The second response is coherent because it specifies the fiber.

Remark

Special case: If the family of types is constant (E_b = E for all b), the predicate is global. This is context-free evaluation. Most preference/value predicates are not constant families. When they are, that is the exception, not the rule.

Consequence

Meaning lives in the fiber. In general, "best" is not well-typed without parameters. When it is context-free, that is a special case: a constant family.

A14 gives us the structure to handle dependent predicates: pullback functors that re-index types along refinements, with functoriality laws that make composition work. The sheaf condition (A13) then applies fiberwise: glue claims within a fiber, or find a common refinement where pullbacks agree.

Context-dependence is structure, not relativism — and the structure is called a fibration. One dimension of that structure, however, remains unexamined. The views described so far differ in their signatures and their types; they may also differ in something more fundamental: their logic. What "not p" means — whether it signals proof of absence, mere non-assertion, or something in between — varies with the view's proof rules and absence policy. When views with different logics overlap, their claims cannot be directly compared until the logical difference is surfaced. Negation, it turns out, is not universal.