Fibrations

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.

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. Chapter 11 treats compatible local sections and their gluing; A14 makes the indexing of types and their reindexing along context maps explicit. The connection to dependent type theory supplies one account of T8 (Uncertainty/Value), with predicates such as "best" and "affordable" indexed by declared 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. An identical ranking might suit both users. The defect would be to ignore parameters the promised ranking should take into account. A type system can help expose that omission; identical outputs alone do not prove it.

"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. Whether their rankings should differ depends on the candidates and the stated criteria; the evaluation must nevertheless account for each set of requirements.

Affordable wedding dress vs affordable cocktail dress. The budget thresholds differ by occasion. A person might allow $5,000 for a wedding dress and $200 for a cocktail dress; a $3,000 item falls on different sides of those chosen thresholds. "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.

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

A presheaf assigns a set to each context and a restriction map to each relevant context morphism; those sets need not be identical. A fibration makes objects over each context, and their reindexing, part of the account. Reindexing can carry a nonconstant family or leave a constant one unchanged. The distinction is what the chosen presentation organizes, not a universal contrast between an unchanging and a changing type.

The Reindexing Property

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). An implementation may realize the chosen reindexing by a compiler; it must still establish that the compiler preserves the declared structure.

Ordinary parameterized functions can also specialize a predicate. The fibration specifies the compositional laws that a more general family of such operations must satisfy; it does not make other implementations impossible.

Dependent Types

Fibrations supply categorical models of aspects of dependent type theory; the required type formers need additional structure³.

Γ ⊢ A type: In context Γ, the type A is well-formed⁴.

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 attraction is that parameter dependence can enter the type discipline. Ordinary functions can also make it explicit: affordable : Context → Dress → Bool is adequate for the simple budget test. Dependent types become useful when the type of the result or its admissible evidence itself varies with the context. Neither composability nor versioning requires their use in every implementation.

affordable : Dress → Bool

affordable : (ctx : Context) → Dress → Bool_ctx

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):

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

What goes wrong when the promised budget is ignored:

• 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 applied the wrong budget policy; a suitable type discipline could prevent this particular omission

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

A14 organizes reindexing. Gluing requires a further descent condition. A fibration over a site is not automatically a stack, and applying a sheaf condition separately in each fiber does not establish effective descent of objects across a cover.⁵

For sets of claims, A13 supplies unique gluing when its exact matching and sheaf hypotheses hold. In a category-valued account, compatible objects and their isomorphisms require coherence on overlaps and an effective global realization; the stack condition supplies that additional work. No such general theorem for the predicate bundles used here has been proved.

“Affordable for Alice” and “affordable for Bob” can coexist in one indexed record, or be conjoined as two separate propositions. To turn them into a single unindexed judgment, the receiving system needs a declared rule about whose budget governs. Reindexing does not choose that rule.

Failure Modes

Type collapse: A context-indexed predicate is used without an argument its declared type requires. That application is ill-typed. A different evaluator may legitimately use a fixed, disclosed budget; its Bool result is not ill-typed merely because the context is constant.

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. The failure is concealing the default where a user reasonably expects a different parameter to govern.

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. They can be conjoined with their parameters intact. What does not follow is affordability for a third person, or under an unspecified common budget.

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:

where γ = (budget, occasion, style, ...). "Best" can mean membership in the maximal set under ⪯_γ. A top-K selection is a different contract: for K greater than one it can include nonmaximal items, and it needs a tie rule. Either can supply a Bool predicate once the intended selection is declared.

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 specifies the claim to check. Its correctness still depends on the candidate set, metric and evaluation.

Consequence

The budget parameter can change an answer while leaving its result type Bool. A14 is useful where the types over a context and their reindexing need to be explicit; an ordinary parameterized evaluator may suffice for a simpler task. The recipient must be able to find the dependency that changes its answer, whichever presentation is chosen.

A further dependency enters when one view treats a missing report as a negative and another leaves it open. Their signatures and item sets may match while their inferences differ. Chapter 13 follows that difference into the rules under which the recipient reasons.