Framework Lexicon
Part of the cognition series. Reference post β updated as vocabulary sharpens.
Several mathematical communities have independently formalized overlapping structures under different names. This post maps the translations.
If youβre here because you found your name: The Rosetta stone below maps your work to parallel results in other communities. The dashes mark where one community has no term for a concept the other has named.
Authors cited: Fritz, Spivak, Gaboardi, Katsumata, Kura, Jacobs, Liell-Cock, Staton, Perrone, Leinster, Baez, Sato, Chen, Vigneaux, Rezagholi.
π Run these papers interactively
Rosetta stone: same objects, different names
Corrections welcome β june@june.kim.
| PL theory | Categorical probability | Shared object | Framework | Confidence |
|---|---|---|---|---|
| Kleisli(D) Jacobs 2014 |
FinStoch Fritz 2020 |
Category of finite sets + stochastic matrices | Ambient category post |
Exact. Same category |
| Hoare triple {P} c {Q} Gaboardi 2021 |
β | Predicate on morphism outputs, preserved under composition | Contract Graded.lean |
Plausible. Grade algebra matches: PreorderedMonoid typeclass with additive composition, weakening, Nat instance (Graded.lean). Gaboardi's categorical semantics (graded Freyd categories, coherent fibrations, soundness theorem) not formalized. |
| Restricted pointwise order Kura-Gaboardi 2026 Def 7 |
β | Post(N) implies Pre(N+1), restricted to support | Handshake Comp.lean |
Exact. forward_triple chains four COMP rules through real pre/postconditions. Each stage's postcondition is the next stage's precondition β the restricted pointwise order, machine-checked. |
| wp via poset fibration over Kleisli(D) Jacobs 2014 |
Posetal imperative category Staton 2025 Cor. 76 |
Predicate logic over a stochastic category | "Fibration" post |
Exact. Staton proves Hoare rules over Stoch (Thm 79) |
| Graded Freyd category Gaboardi 2021 |
Graded Markov category Liell-Cock & Staton 2025 |
Effectful computation with tracked side-effects | Stage + contract Lean |
Plausible. Freyd vs. Markov differ on exponentials |
| Divergence on monad Sato-Katsumata 2023 |
Enriched Markov category Perrone 2023 |
Metric on morphism spaces for verification | NonExpanding Lean |
Plausible. nonExpanding_iff_threshold_triple characterizes NonExpanding as a family of unary threshold Hoare triples (Divergence.lean). Analogous in spirit to Sato-Katsumata, but their framework is relational (compares two morphisms via graded divergence), ours is unary. Not a formal instance of their construction. |
| β | Possibilistic shadow Ξ₯ Fritz et al. 2023 |
Possibilistic collapse of a probabilistic morphism | Support typeclass Support.lean |
Exact. support_bind = monad multiplication |
| β | supp : V β H Fritz-Perrone-Rezagholi 2021 |
Monad morphism: valuations β closed subsets | support_bind Support.lean |
Exact. Same composition law |
| β | Static idempotent Fritz et al. 2023 Prop 4.4.1 |
Idempotent that stabilizes after one step | IterationStable Contracts.lean |
Plausible. IterationStable = Hoare triple {'{'}c{'}'} f {'{'}c{'}'} (definitional). StaticOn (output = input) is strictly stronger. The splitting factorization of Fritz Prop 4.4.1 is not yet formalized: stableSplit in Static.lean is a placeholder. Gap is characterized but not closed. |
| β | Magnitude Leinster 2021 |
Categorical cardinality / effective species count | Diversity post |
Speculative. No composition law for magnitude |
| Free β-semimodule monad Kidney & Wu 2021 |
Double dualization Fritz-Perrone-Rezagholi 2021 |
Counting monad parameterized by semiring S | Gap supp composed with |Β·| |
Speculative. Exists on Set, not via double dualization on Top |
| Selection relation on parametrised optics Capucci et al. 2021 |
β | "What is a goal but a predicate on a system?" Compositional predicate on morphisms. | Contract post |
Plausible. Same role (behavioral predicate); different ambient structure (optics vs. Kleisli) |
| Nash equilibrium as compositional predicate Ghani-Hedges et al. 2018 |
β | Equilibrium checked locally on subgames, preserved under game composition | Contract preserved under composition Lean |
Plausible. Structural parallel; games β pipelines |
| Bayesian lens / statistical game Smithe 2021 |
Bayesian inversion in Markov category Braithwaite-Hedges-Smithe 2023 |
Optic with forward (inference) and backward (learning) pass over stochastic morphisms | Forward pipeline + Consolidate post |
Plausible. Both have forward+backward; optic composition β Kleisli composition |
| β | Dagger structure on kernels Parzygnat 2020 |
Bayesian inversion as categorical involution on morphisms | Consolidate (backward pass) post |
Speculative. Consolidate updates policy; dagger inverts morphisms. Related but not the same operation |
| Effect algebra predicates (X β 1+1) Cho-Jacobs 2015 |
β | Predicates as effects, not subobjects. States/effects duality. | Contract Effects.lean |
Plausible. Boolean contracts embed as {0,1}-valued effects (Effects.lean), but the bridge is a Bool-to-Prop encoding, not a full effect algebra structure. The quantitative case (effects in [0,1]) is not formalized. |
| Partial correctness Standard PL |
Partial Markov categories Di Lavore-Roman-Sobocinski 2025 |
Morphisms can fail. Observations, normalization, conditioning in restriction categories. | β (pipeline assumes total morphisms) |
Plausible. Pipeline stages don't fail; but Filter's rejection maps to partiality |
| Program equivalence metrics Panangaden 2009 |
β | Bisimulation metrics = behavioral distance between stochastic processes | β (no framework analog) |
Speculative. Could connect to magnitude as behavioral distance. Nobody has tried. |
Pipeline structure
| Terminology | Source | Connection | Framework term |
|---|---|---|---|
| Operad algebra | Spivak 2013 | The six roles are boxes in a wiring diagram. Typed ports constrain which boxes connect. | Pipeline |
| Type forcing | Type Forcing post + Lean proof | Given the six interface types, the supplier assignment is unique. Pipeline topology is forced. | Wiring uniqueness |
| Stoch β Markov category | Fritz 2020 | The category the pipeline lives in. Measurable spaces + Markov kernels. Copy/delete structure. | Ambient category |
| Kleisli arrow Ξ± β M Ξ² | Standard | Each pipeline stage is a monadic kernel. When M = Id, it's a deterministic function. | Kernel |
| Kleisli composite of five kernels | Lean proof (Pipeline.lean) | Perceive β Cache β Filter β Attend β Transmit. Five morphisms composed via >=>. | Forward pipeline |
| Traced monoidal category | Joyal-Street-Verity 1996 | Transmit's output feeds Perceive's input. The loop closes via a trace operator. | Feedback loop |
| Forward + Consolidate | Lean proof (Pipeline.lean) | One complete iteration: forward pass produces ranked output, Consolidate updates policy. | Cycle |
Deterministic / stochastic boundary
| Terminology | Source | Connection | Framework term |
|---|---|---|---|
| Copy-natural morphism | Fritz 2020 Β§10 | Filter is deterministic: same input, same gate. Commutes with copy. Lives in Cdet. | Deterministic morphism |
| Copy-non-natural morphism | Fritz 2020 | Attend must be stochastic: deterministic selectors cycle, killing diversity. | Stochastic morphism |
| Cartesian subcategory Cdet | Fritz 2020 Β§10 | Filter lives inside. Attend crosses out. Cdet closed under composition: two det morphisms compose to det. | Cdet boundary |
| Pigeonhole β state collision | Lean proof (Stochasticity.lean, Pigeonhole.lean) | Deterministic transducer over Fin N must collide within N+1 steps. Confusion β error. | Stochasticity is mandatory |
Information theory
| Terminology | Source | Connection | Framework term |
|---|---|---|---|
| F(f) = c(H(p) β H(q)) | Baez-Fritz-Leinster 2011 | The pipeline's information budget. Unique form under functoriality + convex-linearity + continuity. FinProb only. | Information loss |
| Functorial nonneg loss accumulates | Baez-Fritz-Leinster 2011 | Information only decreases through pipeline stages. Post-processing can't recover lost bits. | DPI |
| t β€ s iff t = c β s (a.s.) | Fritz 2020 Def 16.1 | Consolidate's output is a sufficient statistic. Retains task-relevant info, discards the rest. | Informativeness preorder |
| Distance from determinism | Fritz-Gonda-Perrone-Rischel 2024 | Measures how far a morphism is from being deterministic. Enriched Markov categories. | Categorical entropy |
| Divergences in enriched hom-spaces | Perrone 2023 | Fisher metric lives in the enrichment. Potential home for Consolidate's update dynamics. | Info geometry |
| Magnitude / Hill number | Leinster 2021 | Hill at q=0 = support size = species richness. Diversity IS categorical cardinality (magnitude). | Diversity |
Support and possibilism
| Terminology | Source | Connection | Framework term |
|---|---|---|---|
| Possibilistic shadow Ξ₯ : C β SetMulti | Fritz et al. 2023 | The Lean proof's Support class IS this. Collapses probabilistic to possibilistic. support_bind = monad multiplication for supp : V β H. | Support typeclass |
| Unit of Hoare hyperspace monad H | Fritz-Perrone-Rezagholi 2021 | Ο(x) = cl({x}). Pure computation has singleton support. | support_pure |
| supp(E(ΞΎ)) = U(supp#(supp(ΞΎ))) | Fritz-Perrone-Rezagholi 2021 | Support of composite = closure of union of conditional supports. Bind distributes support via existential. | support_bind |
| Closed subsets, lower Vietoris topology | Fritz-Perrone-Rezagholi 2021 | The codomain of the support monad morphism. Algebras are complete join-semilattices. | Hoare hyperspace H |
| Functorial iff causal | Fritz et al. 2023 Thm 3.1.19 | Causality axiom = composition condition for supports. The pipeline is causal. | Support is functorial |
| Static idempotent (e =e id) | Fritz et al. 2023 | Iteration-stable = static idempotent. Splitting = having a support (Prop 4.4.1). Fixed-point structure captured by support object. | IterationStable |
| Gap: |Ξ₯(p)| as lax functor | Nobody yet | Cardinality of possibilistic shadow. Would connect Leinster magnitude to Fritz support. Missing bridge for diversity. | Diversity (Attend) |
Contracts and composition
| Terminology | Source | Connection | Framework term |
|---|---|---|---|
| Predicate on outputs (Ξ² β Prop) | Lean proof | Each pipeline stage carries a postcondition. All six contracts quantify over the support of the kernel. | Contract |
| Hoare postcondition | Gaboardi et al. ESOP 2021 | Graded Hoare logic gives pre/postconditions for graded monads categorically. ContractPreserving IS a Hoare triple. | ContractPreserving |
| Restricted pointwise order | Kura-Gaboardi et al. 2026 Def 7 | f β€P g iff ordering holds where predicate is non-bottom. Post(N) implies Pre(N+1), restricted to support. forward_triple chains four COMP rules through real pre/postconditions. Machine-checked. | Handshake (Comp.lean) |
| Graded monad lifting | Kura-Gaboardi et al. 2026 | Lifting through predicate fibration PredΞ©(C) β C. Interpreting in total category preserves fibrational structure. | Contracts propagate |
| PredΞ©(C) β C | Jacobs 2001 | Standard construction. SCCompC gives dependent types on top. The fiber over each morphism carries its contracts. | Predicate fibration |
| Para construction CΞ³(X,Y) = C(Ξ³βX, Y) | Liell-Cock & Staton POPL 2025 | The grade is a tensor factor. Grading and stochastic semantics are the same structure. | Graded monad = Markov cat |
| Op-lax functor R : ImP β Kl(CP) | Liell-Cock & Staton 2025 Thm 5.6 | R(gβf) β R(g)βR(f). Composing in ImP gives tighter uncertainty sets than composing in the quotient. Subset = refinement. | Tighter bounds under composition |
| Bop β PreMon | Kura-Gaboardi et al. 2026 Def 6 | The grading monoid varies with the base index. Effects (contracts) are value-dependent, not just type-dependent. | Indexed preordered monoid |
Variational derivations
| Terminology | Source | Connection | Framework term |
|---|---|---|---|
| Optimality over feasible set | Lean proof | Element-level: x is feasible and no feasible y has lower cost. Used for Consolidate and Filter. | MinimizesOn |
| Incumbent is always admissible | Lean proof | The current policy is always a feasible candidate. Optimal output β€ incumbent. Derives Consolidate's lossiness. | self_feasible |
| Nontrivial feasible reduction exists | Lean proof | For every input, a strictly smaller feasible output exists. Minimality + witness β strict reduction. Derives Filter's gating. | strict_witness |
| Contract as optimality condition | Lean proof | Constructors that build contract structures from optimization problems. Plug into existing handshake machinery. | fromOptimal |
Open bridges
| Bridge | Connects | Would give us | Search terms |
|---|---|---|---|
| Hoare logic over Markov category | Bonchi-Di Lavore-Roman-Staton 2025 | CLOSED. Stoch is a posetal imperative category (Cor. 76). All Hoare rules (SKIP, COMP, ASSIGN, LOOP, WHILE...) derived as theorems (Thm 79). Predicates = morphisms X β 1. Triples = inequalities in posetal structure. | Staton's "imperative category" = traced distributive copy-discard category. Markov categories ARE copy-discard categories. Paper explicitly names Stoch and proves the rules. |
| Semiring-valued monad via change of base | Fritz-Perrone-Rezagholi supp : V β H + Leinster magnitude | Diversity contract derived variationally: DPP maximizes support cardinality under capacity | Double dualization uses a semiring S: {0,1} β reachability, [0,β) β probability. (β, +, 0) β counting. Not via double dualization, but the free β-semimodule monad (= multiset monad) exists on Set. Jacobs proves a distributive law MβD β DβM (multiset over distribution). Compose with support to track cardinality. |
| Categorical DPPs | Exterior algebra functor + Markov categories | The concrete Attend mechanism (DPP kernel) with categorical semantics | determinantal point process categorical; DPP monoidal; L-ensemble categorical |
| Coding theorems | Fritz entropy + Shannon theory | Consolidate's compression as a categorical rate-distortion theorem | rate-distortion Markov category; Wyner-Ziv categorical |
| Natural gradient as morphism | Perrone info geometry + optimization | Consolidate's update step as a gradient flow on the statistical manifold | natural gradient categorical; gradient descent enriched Markov |
Authors and papers
| Author | Paper | What it does |
|---|---|---|
| Tobias Fritz | Markov categories (2020) | Defines the ambient category for stochastic morphisms. Copy-naturality distinguishes deterministic from stochastic. Informativeness preorder captures sufficient statistics. |
| Markov Categories and Entropy (2024) | Defines entropy categorically as distance from determinism. Enriched Markov categories with divergences on hom-sets. Data processing inequality proved abstractly. | |
| Supports and idempotent splitting (2023) | Defines supports abstractly in Markov categories. Supports are functorial iff the category is causal. Static idempotents split iff they have supports. | |
| Fritz, Perrone, Rezagholi | Support as monad morphism (2021) | Proves supp : V β H is a monad morphism from valuations to Hoare hyperspace. Both constructed via double dualization against different semirings. |
| Baez, Fritz, Leinster | Entropy characterization (2011) | Shannon entropy is the unique functorial, convex-linear, continuous information loss assignment in FinProb, up to scale. |
| Sam Staton | Program Logics via Distributive Monoidal Categories (2025) | Derives Hoare logic from traced distributive copy-discard categories ("imperative categories"). Proves Stoch is a posetal imperative category. All Hoare rules follow as theorems. |
| Compositional Imprecise Probability (POPL 2025) | Graded monads over Markov categories for imprecise probability. The para construction makes the graded model itself a Markov category. | |
| Marco Gaboardi | Graded Hoare Logic (ESOP 2021) | Hoare triples parameterized by a preordered monoid grade. Categorical semantics via graded Freyd categories over coherent fibrations. Instantiated for cost, privacy, and probability. |
| Indexed graded monads (2026) | Graded monads parameterized fibrewise over a predicate fibration. Restricted pointwise order propagates pre/postconditions through composition. | |
| Shin-ya Katsumata | Divergences on Monads (MSCS 2023) | Divergences on a monad = enrichments of its Kleisli category. Connects metric structure on morphism spaces to relational Hoare logic. Instantiated for differential privacy and cost. |
| Bart Jacobs | Weakest preconditions in fibrations (2014) | Derives wp-semantics from order-enriched Kleisli categories via poset fibrations. Instantiated for the distribution monad, whose Kleisli category is FinStoch. |
| Structured Probabilistic Reasoning (2025 draft) | Book-length treatment of distributions, predicates, channels, conditioning via effectus theory. Cites Fritz extensively but uses his own formalism. FPred fibration for fuzzy predicates. | |
| Tom Leinster | Entropy and Diversity (2021) | Hill diversity numbers are the unique axiomatic diversity measures. Diversity is a special case of magnitude, the categorical generalization of cardinality for enriched categories. |
| Paolo Perrone | Categorical Information Geometry (2023) | Information geometry inside enriched Markov categories. Divergences in hom-spaces recover Shannon/Renyi entropy, DPI, and the Gini-Simpson index. |
| David Spivak | Operad of wiring diagrams (2013) | Typed ports and supplier assignment for composing boxes in wiring diagrams. Gives the syntax layer: which boxes connect to which. |
| Kidney & Wu | Algebras for Weighted Search (ICFP 2021) | Free semimodule monad parameterized by arbitrary semiring S. S = β gives multiset monad (counting). S = [0,1] gives probability. Unifies search and probability via semiring choice. |
| Chen & Vigneaux | Categorical Magnitude and Entropy (2023) | Unifies Shannon entropy and log(magnitude) for finite categories with probability. Recovers magnitude under uniform distribution. Invariant of individual categories, not a functor on morphisms. |
| Luca Reggio | Semiring-valued measures (2020) | Codensity monad of finite S-semimodules gives S-valued measures on Stone spaces. Change-of-semiring framework for codensity monads. Requires finite semirings. |
| Kenta Cho | Introduction to Effectus Theory (2015) | With Jacobs. Predicates as effect-algebra-valued maps (X β 1+1), not subobjects. States/effects duality with Born rule. Parallel formalism to Markov categories. |
| Dario Stein | Probabilistic Programming with Exact Conditions (2023) | With Staton. Internal language of CD categories gives precise correspondence between Markov categories and a class of programming languages. Exact conditioning as categorical structure. |
| Eigil Rischel | Infinite products and zero-one laws (2020) | With Fritz. Kolmogorov and Hewitt-Savage zero-one laws proved in categorical probability. Exchangeability and independence axiomatized. |
| TomΓ‘Ε‘ Gonda | Markov Categories and Entropy (2024) | With Fritz, Perrone, Rischel. Categorical entropy recovers Shannon, Renyi, and the Gini-Simpson index used in ecology, direct bridge to Leinster's diversity. |
| Arthur Parzygnat | Quantum Markov categories (2020) | Bayesian inversion as dagger structure on morphisms. Three levels of reversibility: inverses, disintegrations, Bayesian inverses. No-broadcasting theorem. |
| Elena Di Lavore | Partial Markov Categories (2025) | With Roman, Sobocinski. Blends Fritz's Markov categories with restriction categories. Observations, Bayes' theorem, Pearl's and Jeffrey's updates in categorical terms. |
| Prakash Panangaden | Labelled Markov Processes (2009) | Continuous-state probabilistic transition systems as coalgebras. Bisimulation metrics = behavioral distance between processes. Logical characterization of bisimulation. |
| Jules Hedges | Compositional Game Theory (2018) | With Ghani, Kupke, Forsberg. Nash equilibrium as a compositional predicate on strategy profiles, checked locally on subgames. Open games via string diagrams. |
| Mixed Strategies (2020) | With Ghani, Kupke, Lambert. Relational Kleisli lifting of the probability monad lifts equilibrium predicates from pure to probabilistic games. | |
| Matteo Capucci | Towards Foundations of Categorical Cybernetics (2021) | With GavranoviΔ, Hedges, Rischel. Selection relations on parametrised optics. "What is a goal but a predicate on a system?" Goals unify optimization, homeostasis, learning, equilibria. |
| Toby Smithe | Bayesian Lenses. Statistical Games (2021) | Bayesian inversions compose as lenses in a Markov category. Statistical games = optics + free-energy objective. Explicit bridge between Fritz and the cybernetics community. |
| Ho, Wu, Raad | Bayesian Separation Logic (POPL 2026) | Hoare logic for Bayesian probabilistic programming. Model is s-finite kernels. Internal Bayes' theorem via disintegration. Frame rule = probabilistic independence. |
Jargon decoder
For software engineers who know code but not the math vocabulary.
| Term | SE equivalent | What it is | Why it matters |
|---|---|---|---|
| Category theory | |||
| Category | Composable interfaces | A collection of types and arrows between them, with associative composition and identities. | Reason once about composition instead of re-proving it per pipeline. |
| Morphism | Function | A β B. Takes input, produces output. | Every pipeline stage is one. Five compose into the forward pass. |
| Functor | Structure-preserving map | Applies a function inside a container, preserving composition. Array.map, Promise.then, Optional.map β same law, different wrapper. | If a theorem works for Set, check if it works for Stoch. Functors carry it across. |
| Natural transformation | Uniform container conversion | F<A> β G<A> that treats the inner A generically and commutes with mapping. | Change the surrounding effect without changing element-level logic. |
| Monad | Composable effect type | A context with unit and flatMap, so effectful steps compose into one pipeline. | Distribution is a monad. flatMap = marginalization. Same pattern as async, optional, nondeterministic. |
| Kleisli category | Functions returning an effect | Functions A β M<B> where M is the effect. Kleisli(Promise) = async functions. | Kleisli(Distribution) = stochastic functions. Same composition law. |
| Kleisli composition (>=>) | flatMap chain | Run the first, feed each result into the second. | This is how the five pipeline stages compose: >=> five times. |
| String diagram | Data flow diagram with algebraic guarantees | Boxes are functions. Wires are types. Connecting wires = composition. | If the diagram connects, the types check. |
| Traced monoidal category | Structured feedback loop | Output feeds back to input, governed by coherence laws. More constrained than while. | Transmit's output feeds Perceive's input. The trace closes the pipeline. |
| Categorical probability (Fritz et al.) | |||
| FinStoch | Stochastic function | Each input maps to a probability distribution over outputs. In Python: Dict[K, Dict[V, float]]. | Probabilistic programs compose like ordinary functions. |
| Markov category | Stochastic functions + copy + discard | FinStoch equipped with the ability to duplicate and discard data. | One test distinguishes deterministic from stochastic: does copying commute? |
| Copy-natural (Cdet) | Deterministic function | Copying input before or after running the function gives the same paired result. | Filter must be deterministic. Attend must not be. Copy-naturality is the test. |
| Support | Set of possible outputs | Which outputs have nonzero probability. Forget the weights, keep the keys. | Prove safety without computing probabilities. |
| Possibilistic shadow (Ξ₯) | Reachability set | Collapse probabilities to yes/no. {'{k for k,v in d.items() if v>0}'}. | Reason about what's reachable before worrying about how likely. |
| Monad morphism | Structure-preserving effect translation | Converts one monad to another without breaking composition. supp maps Distribution β Set. | Translate between probability and reachability. Composition survives. |
| Static idempotent | Idempotent operation | Running it twice gives the same result as once. f(f(x)) = f(x) on the support. | IterationStable in the Lean proof. A stable pipeline stage doesn't drift. |
| DPI | Post-processing can't recover lost information | Once a signal passes through a channel, later processing cannot add information about the source. | The pipeline must have external input (Perceive) or it starves. |
| Magnitude | Effective diversity count | Effective number of independent things. Hill diversity = categorical cardinality. | Measures the diversity that Attend must preserve. |
| PL theory (Hoare, Dijkstra, Gaboardi, Kura) | |||
| Hoare triple {'{P}'} c {'{Q}'} | assert pre; run(); assert post | If P holds before running c, then Q holds after. | ContractPreserving in the Lean proof. Machine-checked correctness. |
| Weakest precondition | Inferred input constraint | Given run() and post, compute the minimum pre that guarantees post. | Don't guess preconditions. Derive them from the postcondition. |
| Restricted pointwise order | Contract chaining | post(stage N) implies pre(stage N+1), restricted to the support. | The handshake. Four COMP rules chain the forward pipeline. Machine-checked. |
| Graded monad | Effect system with cost tracking | A monad that tracks how much side effect each step uses. Costs compose additively. | Budget resources across the pipeline. Each stage declares its cost. |
| Preordered monoid | Cost type with + and <= | Costs add (monoid) and compare (preorder). Nat, privacy budget, latency. | The grade algebra. Tracks the bill through composition. |
| Fibration | Type-indexed properties | Each type carries a layer of predicates that transport along programs. Properties propagate backward through composition. | Move correctness obligations through composition systematically. |
| Cybernetics (Capucci, Hedges, Smithe) | |||
| Optic / Lens | Getter + setter pair | Forward: read data. Backward: update parameters. Compose bidirectionally. | Forward pipeline + Consolidate as one composable structure. |
Updated 2026-03-23. Previous vocabulary: Type Forcing (Spivak), Ambient Category (Fritz).