Modification (Higher Category Theory)¶
An object-indexed family of 2-cells comparing parallel transformations of higher functors, constrained by compatibility along every source 1-cell.
Core Idea¶
A modification compares two parallel transformations of higher functors. For pseudofunctors \(F,G:\mathcal B\to\mathcal C\) and pseudotransformations \(\eta,\theta:F\Rightarrow G\), it has a 2-cell \(\Gamma_a:\eta_a\Rightarrow\theta_a\) at every source object \(a\). These components must satisfy a compatibility equation along each source 1-cell. Parallel transformations alone need not admit a modification.[1]
There is also a strict version between 2-natural transformations of 2-functors. The strict and bicategorical forms share the object-indexed comparison pattern, but their equations account for their respective transformation data.[2][1]
How would you explain it like I'm…
Comparing Two Comparisons
Coherent Transformation Comparison
Scope of Application¶
The idea belongs to higher category theory, where transformations themselves can be compared by 2-cells. Miranda constructs strict modifications from structural maps of internal categories. Ahrens and collaborators construct bicategorical modifications from supplied paths between homotopies of 2-types.[3][1] An ordinary alteration of an object is not a modification in this sense.
Clarity¶
First specify the two higher functors, then the two transformations between them, then the 2-cell at each object. A family of pointwise 2-cells is insufficient if it fails the law for a source 1-cell. The law is a condition indexed by that 1-cell, not a separately chosen morphism-indexed component.[1]
Manages Complexity¶
The definition packages many local 2-cell comparisons with one rule saying how they fit together. It thereby turns a collection of unrelated objectwise choices into a coherent higher comparison, where one exists.[1] In the internal-category example, source and target maps at each ambient category form modifications that remain coherent under finite-limit-preserving functors.[3]
Abstract Reasoning¶
To test a proposed modification, check that both transformations have the same higher-functor endpoints. Type every proposed component as a 2-cell between corresponding transformation components. Then check the compatibility equation for an arbitrary source 1-cell. A failed equation rules out the proposed modification even when each pointwise cell is well typed.[1]
Knowledge Transfer¶
The recognition test works in two unlike constructions within higher category theory. For internal categories it concerns the source and target maps of evaluation constructions; for fundamental bigroupoids it concerns paths between pointwise homotopies.[3][1] Both supply object-indexed 2-cells that must respect source 1-cells. This shared test does not turn unrelated everyday changes into literal instances.
Relations¶
The Relation and Comparison primes offer loose analogies, but their live signatures do not supply the typed 2-cell family and law. Transformation and Identity-Preserving Modification concern different operations or changes. A strict 2-Category gives one setting; the bicategorical form is broader, so the strict entry is not automatically a parent. Compatibility is a substantial near neighbor because nontrivial 1-cell laws require local comparisons to fit. For a terminal source 2-category the law is automatic and a single target 2-cell is already a modification; the full Compatibility signature is therefore not a strict parent. The reviewed placement is an unparented root.[1]
Examples¶
Internal-category evaluation. Miranda's parallel evaluation transformations \(\mathrm{ev}_1,\mathrm{ev}_0\) admit two distinct modifications \(d_0,d_1\), assembled from source and target maps of internal categories. They are each modifications from \(\mathrm{ev}_1\) to \(\mathrm{ev}_0\), not modifications between each other. Mapped back: the evaluation transformations are the compared pair; each family of source or target maps supplies compatible object components.[3]
Paths in fundamental bigroupoids. For two pointwise homotopies \(e_1,e_2\) between functions of 2-types, a supplied family of paths \(h_x:e_1(x)=e_2(x)\) yields a modification between the induced pseudotransformations. Mapped back: the homotopies are the compared transformations; the paths give object components, with the induced compatibility described in the source. The construction requires the path family.[1]
Neighborhood in Abstraction Space¶
Modification (Higher Category Theory) sits in a moderately populated region (58th percentile for distinctiveness): it has near-neighbors but no dense thicket of look-alikes.
Family — Unclustered & Miscellaneous (2835 abstractions)
Nearest neighbors
- Monoidal Natural Transformation — 0.86
- Direct Limit — 0.85
- 2-Category — 0.85
- Beck–Chevalley Condition — 0.85
- Strictification — 0.84
Computed from structural-signature embeddings · 2026-10-31
Not to Be Confused With¶
- An ordinary natural transformation: it compares functors by arrows, one comparison level lower.
- A pseudotransformation: this is one of the objects a modification compares.
- A pointwise family alone: it may fail the 1-cell compatibility equation.
- A general revision: the everyday word lacks the higher-categorical types.
References¶
[1] Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, and Niels van der Weide (2022), Bicategories in univalent foundations, Mathematical Structures in Computer Science, Definitions 2.12–2.14 and Examples 2.6 and 2.15. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i
[2] Michael Lambert (2024), Discrete 2-Fibrations, Higher Structures 8(1), Example 4.17. registry ↩
[3] Adrian Toshar Miranda (2018), Internal Categories, Macquarie University Masters by Research thesis, Remark 1.2.6, Proposition 3.1.1 and Theorem 3.1.9. registry ↩a ↩b ↩c ↩d