Jon Sterling’s Forest

On this website, I organize my thoughts on a variety of topics at a granular level. Sometimes these thoughts are self-contained, and at times I may organize them into larger notebooks or lecture notes. My nascent ideas about the design of tools for mathematical thought are here. I welcome collaboration on any of the topics represented in my forest.

Designing Tools for Mathematical Thought [tfmt-0001]

This document records what I have learned about the design of “tools for mathematical thought” over the past couple years. One of my goals in writing this is to set out both the unique requirements of an information data model that is needed to record and facilitate mathematical thought, as well as the technical requirements for tools that can be used for mathematics.

Definition (tool for mathematical thought) [tfmt-0002]

A “tool for mathematical thought” could be many things, but it must be a tool for the development and interlinking of mathematical ideas in a way that facilitates authoring, publishing, teaching, learning, and the maintenance of evergreen notes.

A tool for mathematical thought could be a piece of software, or it could be an organizing principle for physical notes on paper. In these notes, we will primarily explore the design of computerized tools for mathematical thought.

Existing Tools for Mathematical Thought [tfmt-0004]

The existing tools for mathematical thought can be divided into two main categories: interactive proof assistants and textual authoring and publishing tools (including \LaTeX , as well as the Gerby software that runs the Stacks Project).

Evergreen Notes [tfmt-0003]

The phrase evergreen note is due to Andy Matuschak, who has written extensively about it in his public Zettelkasten. Evergreen notes are permanent notes that evolve and accumulate over time, cutting across different projects.

Hierarchy in Evergreen Notes [tfmt-0005]

Matuschak describes a number of organizing principles for evergreen notes, which are quite compelling; one design principle (Prefer associative ontologies to hierarchical taxonomies) deserves additional discussion in the context of mathematical thought. In particular, the problem of circular reference must be grappled with immediately rather than incidentally: in ordinary knowledge management, circularity represents the completion of a train of thought, whereas in mathematical thinking it remains very important to distinguish assumptions from consequences.

Hence a purely associative organization of mathematical knowledge is not viable (although it often happens by accident), and so the hierarchical organization of mathematics must be taken seriously from the start. We find that Matuschak has in fact already grappled with the need for hierarchy in his note It’s hard to navigate to unlinked “neighbors” in associative note systems, where he discusses the difficulty of traversing the “neighbor”-relationship between notes that are related by another note’s context, but are not related on their own. Matuschak proposes to solve the problem by grafting hierarchy onto the associative ontology after the fact through “outline notes”:

“Outline notes” can create pseudo-hierarchies with order and structure by linking to many child notes. Then we need the UI to support navigating between neighbors “through” these outline notes.

The viewpoint of outline hierarchy as a structure imposed on the existing associative ontology is a convenient organizing principle for evergreen notes in the sense of Matuschak, but it is a necessary principle for the design of tools for mathematical thought.

Hierarchical Structure as Non-Unique Narrative [tfmt-0006]

Multiple hierarchical structures can be imposed on the same associative network of nodes; a hierarchical structure amounts to a “narrative” that contextualizes a given subgraph of the network. One example could be the construction of lecture notes; another example could be a homework sheet; a further example could be a book chapter or scientific article. Although these may draw from the same body of definitions, theorems, examples, and exercises, these objects are contextualized within a different narrative, often toward fundamentally different ends.

As a result, any interface for navigating the neighbor-relation in hierarchically organized notes would need to take account of the multiplicity of parent nodes. Most hypertext tools assume that the position of a node in the hierarchy is unique, and therefore have a single “next/previous” navigation interface; we must investigate the design of interfaces that surface all parent/neighbor relations.

The Best Structure to Impose Is Relatively Flat [tfmt-0009]

It is easy to make the mistake of prematurely imposing a complex hierarchical structure on a network of notes, which leads to excessive refactoring. Hierarchy should be used sparingly, and its strength is for the large-scale organization of ideas. The best structure to impose on a network of many small related ideas is a relatively flat one. I believe that this is one of the mistakes made in the writing of foundations of relative category theory, whose hierarchical nesting was too complex and quite beholden to my experience with pre-hypertext media.

There are many ways to model hierarchy, but there are two salient orthogonal distinctions in the different designs:

Absolute vs. Relative Hierarchy in Document Markup Languages [tfmt-000B]

Both HTML and \LaTeX support a form of hierarchical organization with “absolute” heading levels, i.e. levels that count upward from a single root. In HTML, there is <h1>, <h2>, <h3>…, and in \LaTeX there is \part, \chapter, \section, \subsection,\subsubsection, …, \paragraph depending on the document class. This is in contrast to a relative model of hierarchy, in which there is a single command to introduce a section heading at the “current” level, and there are other commands to introduce hierarchical nesting.

The absolute sectioning model is completely inadequate for the hierarchical organization of ideas, for the simple reason that it is the context of a node that determines what its level in the hierarchy is, not the node itself. When this is mixed up, it makes re-contextualization an extremely painful and time-consuming process: you must recursively increment or decrement all section levels that occur underneath a given node, as anyone who has used \LaTeX for any significant writing project can attest.

In traditional texts, re-contextualization occurs when you want to move a section from one place in the hierarchy to another; in the more fluid media I am pursuing, there may be many orthogonal hierarchical structures imposed on the network, so re-contextualization ceases to be a refactoring task and is elevated as a basic unit of mathematical activity. In either case, we are drawn to prefer relative hierarchy over absolute hierarchy. See relative hierarchy in existing tools for existing implementations of this idea.

This is similar to the relationship between De Bruijn levels (global levels) and De Bruijn indices (local levels) in type theory: conventional section headings are like De Bruijn indices in that they count from the root node, whereas what we would want are section headings that count from the present node.

Implicit vs. Explicit Hierarchy in Document Markup Languages [tfmt-000D]

Many document markup languages, including \LaTeX and HTML, use sectioning commands that evince an implicit hierarchical structure: for instance, consider the following HTML code:

<h1>Foo</h1>
<h2>Bar</h2>
<h3>Baz</h3>
<h3>Qux</h4>
<h1>Boo</h1>

The above corresponds to the tree [Foo > [Bar > [Baz, Qux]], Boo]. On the other hand, it is also possible to consider a model in which the hierarchy is made explicit through the syntactical tree structure of the markup language. This style is also supported (but not forced) in HTML:

<section>
  <h1>Foo</h1>
  <section>
    <h2>Bar</h2>
    <section>
      <h3>Baz</h3>
    </section>
    <section>
      <h3>Qux</h3>
    </section>
  </section>
</section>

<section>
  <h1>Boo</h1>
</section>

We greatly prefer the combination of (relative, explicit) hierarchy.

Atomicity of Mathematical Notes [tfmt-0007]

One of the design principles for evergreen notes described by Matuschak is atomicity (Evergreen notes should be atomic): a note should capture just one thing, and if possible, all of that thing. A related point is that it should be possible to understand a note by (1) reading it, and (2) traversing the notes that it links to and recursively understanding those notes.

Traditional mathematical notes do not achieve this kind of atomicity: understanding the meaning of a particular node (e.g. a theorem or definition) usually requires understanding everything that came (textually) before it. In the context of the hierarchical organization of evergreen mathematical notes, this would translate to needing to go upward in the hierarchy in order to understand the meaning of a leaf node. I regard this property of traditional mathematical notes as a defect: we should prefer explicit context over implicit context.

High-equality mathematical notes should make sense without context; hierarchical context is imposed in order to tell a story, but consumers of mathematical notes should not be forced into a particular narrative. Indeed, as many different hierarchical structures can be imposed, many different narratives can be explored.

My first exploration of hypertext mathematics was the lecture notes foundations of relative category theory; in hindsight, these lecture notes are very much traditional lecture notes, not written with the atomicity principle in mind. As a result, it is often difficult to understand a given node without ascending upward in the hierarchy.

Achieving Atomic Mathematical Notes [tfmt-0008]

Atomicity in evergreen mathematical notes is enhanced by adhering to the following principles:

  1. no free variables: do not rely on one-off objects that are defined incidentally upwards in the hierarchy; turn them into atomic nodes that can be linked;
  2. favor explicit dependency: whenever using a terminology or construction that has been defined elsewhere, link it;
  3. notation should be decodable: all notations (except the most very basic) should be recalled via a link.

It can be a bit excessive to link every word: but the pertinent links could be added to a “related pages” section.

Requirements for Typesetting Mathematics [tfmt-000E]

Many non- \LaTeX hypertext tools boast some compatibility with mathematical typesetting: for instance, in any HTML-based tool it is possible to use MathML or, for better cross-browser support and easier authoring, import \KaTeX or MathJax. For instance: Logseq, Obsidian, and Notion all support rendering of \LaTeX math code using either \KaTeX or MathJax. Unfortunately, the “support” provided is so limited that it is not usable for a working mathematician — so it is somewhat puzzling why the support is present in the first place. Here we will discuss some fundamental requirements for any tool that aims to support mathematical note, without which it is not applicable for use by professionals.

Notational Macros in Mathematical Authoring [tfmt-000F]

Mathematical writing tends to involve a variety of notations which (1) can be difficult to typeset by hand, and (2) will likely change over time. The difficulty of hand-typesetting is somewhat less important than the propensity of notation to change over time: when we change notations within a given mathematical work, we must update every occurrence of the notation: but when the representation of the notation is unstructured, it is not in fact possible for a tool (e.g. find-and-replace) to detect every instance that needs to be updated. Therefore, it is mandatory that the representation of mathematical notations be structured.

\LaTeX allows authors to structure their notations very simply using macros, which can be introduced using \def or \newcommand or \NewDocumentCommand. It is trivial to update all occurences of a notation by simply changing the definition of the corresponding macro.

Unfortunately, most tools that purport to support the inclusion of mathematical expressions do not have adequate support for macros. Both \KaTeX and MathJax have excellent support for configuring macros, but these configuration options are not available in most of the tools that build on \KaTeX and MathJax: for instance, Logseq and Obsidian and Notion all support embedding mathematics, but they do not support configuring macros. In fact there is a community plugin for Obsidian that adds this functionality, but it only supports imposing a global macro library on the entire “vault”, which is inadequate.

Notational Macros Are Local, Not Global [tfmt-000H]

In \LaTeX , macros are organized into packages that are then globally imported into a single document. Because a \LaTeX document comprises just one project and thus any transclusions (via \input or \include) are of components local to that one project, this model is adequate — although experienced users of \LaTeX are nonetheless all too aware of the difficulties of namespacing macro commands when interacting with multiple packages or document classes.

The requirements for a tool that aims to bring together multiple projects over a very long period of time are somewhat different: many distinct packages of notation will be used across the body of work, and it is not possible to fix a single global notation package.

Indeed, it is not reasonable to expect that all notes within a person’s mathematical life shall share the same notations, and in many cases, it would moreover be necessary for the names of the macros associated to these notations to clash. This can happen because two projects are orthogonal, or it can happen as the author’s tastes change over time — and it is not reasonable for such a tool to force enormous and weighty refactorings (touching thousands or tens of thousands of notes) every time the author’s taste changes. The need for arduous refactorings of this kind is one of the main ways that large mathematical projects tend to collapse under their own weight.

It follows that any tool for thought whose support for mathematical notations involves a globally-defined macro package is inadequate for mathematical uses. On the other hand, it is also not reasonable to require the author to define all their macros in each note: notes tend to be small, and there will always be large clusters of notes that share the same notations — and for which the small refactoring tasks involved when notations change are a positive feature rather than a negative one, as one of the goals of a cluster is to accumulate cohesion.

Therefore, the precise requirement for macro library support is as follows:

  1. The author must be able to define (in their own files) multiple notational macro libraries.

  2. A given note must be able to specify which macro library (if any) it employs.

Finally, careful attention must be paid to the interaction between the above requirements and the transclusion of mathematical notes: a transcluded note must be rendered with respect to its own macro library, and not that of the parent note.

Mathematical Diagrams and Macro Support [tfmt-000G]

A basic requirement of tools for mathematical thought is to support the rendering of mathematical diagrams. What kinds of diagrams are needed depends, of course, on the problem domain: for my own work, the main diagram-forms needed are commutative diagrams and string diagrams.

Mathematical Expressions and Diagrams Are Tightly Coupled [tfmt-000P]

Although diagramming may seem to non-mathematicians to be somewhat orthogonal to notational macro support, in reality any solution to the diagramming problem must be tightly and natively integrated with the rendering of mathematical expressions — simply because most diagrams involve mathematical expressions, and these invariably involve notational macros. The reason PGF/TikZ has been so successful is that it respects this tight coupling.

The situation for hypertext mathematical tools is somewhat less advanced than that of \LaTeX and PFG/TikZ, but there are several options which we discuss below.

Commutative Diagrams in KaTeX [tfmt-000J]

\KaTeX has a very rudimentary support for commutative diagrams built-in, by emulating the amscd package. Unfortunately, this support is completely inadequate for usage by mathematicians today:

  1. Only square diagram shapes are supported: commutative diagrams in general have diagonal and curved lines, but these are not supported.

  2. The rendering of the limited gamut of supported commutative diagrams is broken in most browsers (at least Safari and Firefox). In particular, lines are jagged as they are pieced together from pipes and arrows that are subtly misaligned.

Commutative Diagrams in MathJax [tfmt-000K]

Like \KaTeX , MathJax supports the amscd commands for rudimentary square-shaped commutative diagrams. Unlike the \KaTeX implementation of amscd, the supported diagrams are rendered correctly without jagged lines; this means that for the vanishingly small population of mathematicians whose needs are limited to square-shaped diagrams, MathJax’s builtin support is viable.

On the other hand, there is a more advanced option available for users of MathJax: the XyJax-v3 plugin, which adds support for the full gamut of xypic diagrams to MathJax. Notably, this plugin is used by the Stacks Project. The only downside of the xypic support is that it interacts poorly with accessibility features (but no worse than any other solution to rendering non-trivial commutative diagrams), and diagrams created using xypic look considerably less professional than those created using tikz or quiver.

Both \KaTeX and MathJax have the benefit that diagrams created using them will respect the ambient macro package with which the tool has been configured; therefore, if one looks past the rudimentary nature of the support for commutative diagrams, our main requirement is indeed satisfied. Another tool worth discussing is quiver.

The Quiver Interactive Diagramming Tool [tfmt-000I]

The quiver application is an excellent graphical interface for interactively constructing commutative diagrams, with very high-quality rendering.

One positive aspect of quiver is that it is possible to load it with your own macro library, so that diagrams involving custom notations render correctly in the graphical interface. The downside of the approach here is that the macro library must be located on a publicly accessible URL that can be pasted into the quiver interface.

Quiver also offers excellent support for embedding the resulting diagrams in existing \LaTeX documents: after creating your diagram, you can request a \LaTeX snippet that includes a URL which allows you to resume editing your diagram. For example:

% https://q.uiver.app/?q=WzAsMixbMCwwLCJBIl0sWzEsMCwiQiJdLFswLDFdXQ==
\[
  \begin{tikzcd}
    A & B
    \arrow[from=1-1, to=1-2]
  \end{tikzcd}
\]

Unfortunately, the support for embedding quiver diagrams in HTML documents is currently inadequate for professional use. The HTML embed code provided simply produces an <iframe> with a very large watermark, and it is not possible to style the interior of the embedded frame (e.g. to change the background color, or decrease the margins):

<!-- https://q.uiver.app/?q=WzAsMixbMCwwLCJBIl0sWzEsMCwiQiJdLFswLDFdXQ== -->
<iframe class="quiver-embed" src="https://q.uiver.app/?q=WzAsMixbMCwwLCJBIl0sWzEsMCwiQiJdLFswLDFdXQ==&embed" width="304" height="176" style="border-radius: 8px; border: none;"></iframe>

Therefore, we must conclude that although quiver is an excellent tool for authors of traditional \LaTeX documents, it is not currently a candidate for inclusion in tools for hypertext mathematical authoring.

Because of the currently inadequate support of quiver for embedding diagrams in hypertext settings, we cannot consider it any further. There is a final option that turns out to be the most used in practice: generating SVG images statically from embedded \LaTeX code.

Generating Images Statically Using LaTeX [tfmt-000L]

Because of the general inadequacy of the other available tools, most authors of hypertext mathematics with diagramming needs tend to rely on the static generation of images from \LaTeX code using a local \LaTeX toolchain. It is not difficult to instrument pandoc with a Lua filter to render tikz code to SVG images.

There are also a variety of other tools that do something similar, which tend to be employed in static site generation:

The basic architecture of such a tool is to scan for \LaTeX blocks, and then identify them by a hash of their contents. This hash is used as a filename for .tex files, which are compiled to .dvi and thence to .svg using the dvisvgm tool. Alternatively, it is also possible to transclude the resulting <svg> element directly, but one must be careful to rename all identifiers in the <svg> element uniquely, as it is possible for two different <svg> elements on a single page to interfere one each other.

Both antex and forester support passing a macro library to be used when rendering. Both jekyll-sheafy and forester set their macro libraries on a page-local basis through Markdown “front matter”.

A serious downside of generating images from \LaTeX code is the negative impact on accessibility tools. This seems only slightly mitigated by the transclusion of the <svg> element as opposed to using <img>. Ultimately accessibility for mathematical diagrams remains an unsolved problem, and it does not seem that the existing discussion on accessibility of hypertext mathematics has much to say about this problem.

Finally, we comment on more principled approaches using web standards such as SVG and MathML that we hope will take form in the future.

SVG Is Not an Authoring Language [tfmt-000N]

SVG is an extremely powerful low-level language for vector images and diagrams with a variety of applications. Unfortunately, it is not reasonable to compose such diagrams directly in SVG as an author: in contrast to programmatic tools like PGF/TikZ, all positions in SVG are fixed, and there is no possibility to impose important abstractions (e.g. the concept of a line that is “glued” to a pair of nodes). On the other hand, there are many advantages to SVG, including the possibility to intermix SVG with other formats such as MathML.

Because of the low level of abstraction, SVG images that appear in practice today are nearly always produced by a tool or compiler from an input that is defined at a much higher level of abstraction.

MathML Is Not an Authoring Language [tfmt-000O]

Despite some preliminary support for structured representation of high-level mathematical idioms via Content MathML, MathML is not intended to be an authoring language: it is a target language for other tools. Moreover, the content dictionaries (collections of basic elements) of Content MathML are chosen to pertain to the needs of grade-school and secondary-school mathematics and not at all to the needs of professional mathematics:

The base set of content elements is chosen to be adequate for simple coding of most of the formulas used from kindergarten to the end of high school in the United States, and probably beyond through the first two years of college, that is up to A-Level or Baccalaureate level in Europe.

Nonetheless, it seems that the goal was for the content dictionaries of Content MathML to be extended by the individual “communities of practice” to meet their specific needs:

Hence, it is not in general possible for a user agent to automatically determine the proper interpretation for definitionURL values without further information about the context and community of practice in which the MathML instance occurs.

However, in contexts where highly precise semantics are required (e.g. communication between computer algebra systems, within formal systems such as theorem provers, etc.) it is the responsibility of the relevant community of practice to verify, extend or replace definitions provided by OpenMath CDs as appropriate.

It seems that there is a possibility to use XSLT to define your own semantic notational macros, and this certainly bears further investigation. Due to the mutually reinforcing combination of historically poor vendor support and near-absolute isolation from actual communities of practice, i.e. working mathematicians, sophisticated direct use of MathML has never caught on. On the other hand, there is a great deal of MathML on the web today in the form of MathJax and \KaTeX output — tools which are not only currently necessary for obtaining consistent (and professional-quality) rendering of mathematics across browsers, but also are necessary for authoring due to their more succinct markup and easy support for macros.

It seems that the future of MathML is brighter than it was in the past, as we are finally seeing a vital project to improve vendor support led by Igalia. Currently, even browsers that support the MathML standard do so with completely inadequate and unprofessional rendering quality, which means that tools like MathJax and \KaTeX may remain necessary for some time even after vendors finally support MathML. But we hope that with improved vendor support comes new and productive experiments with using semantic tools like XSLT to handle macros, etc. Unfortunately, given the tight coupling between the authoring of mathematical expressions and of mathematical diagrams, this transformation will not take place unless high-level hypertext-compatible tools for drawing diagrams are simultaneously developed.

Towards Mixing SVG and MathML in Hypertext Mathematics [tfmt-000M]

The W3C MathML Core Working Draft points out that MathML can be embedded into <svg> elements using the <foreignObject> element. This is a great strength of the modularity of the model, and I believe that in the future, we will be able to use this as a way to render accessible mathematical diagrams in hypertext.

What is missing? Essentially the current issue preventing widespread use of this method is the fact that neither SVG nor MathML is an authoring language: they are both currently too low-level to be seriously used by authors.

For exactly so long as diagrams must be drawn using \LaTeX -based tools rather than something MathML-compatible, it would be non-negotiable for the support of notational macros to itself be based in \LaTeX syntax (e.g. as in both \KaTeX and MathJax). But it is worth imagining a future in which mathematical diagrams are drawn using a high-level interface to SVG, and then a pure MathML approach to notational macros becomes quite viable. This is not currently the world we live in, but it is something to hope for.

Notes on Duploid Theory [dpl-0001]

This is an investigation of Guillaume Munch-Maccagnoni’s theory of duploids, working in the setting of univalent foundations. Most of what we do could be done in non-univalent foundations; the purpose of univalence is to sharpen our perspective on the relationship between structure and property in duploid theory.

Conventions of Univalent Mathematics [dpl-000B]

A category has hom sets, and is always assumed to be univalent / Rezk-complete; we use the term precategory to refer to a structure that has hom sets and a type of objects with no univalence condition.

Deductive Systems [dpl-0006]

The most basic construct of duploid theory is a deductive system, a variant on the concept of a precategory that relaxes the associativity axiom to reflect the evaluation order of execution in effectful programming languages and proof theories. In this section, we define deductive systems and develop their basic properties.

Definition (deductive system) [dpl-0002]

A deductive system \mathcal{D} is given by a type \Ob{\mathcal{D}} of “objects”, and for every pair A,B\in\Ob{\mathcal{D}} a set \Hom{\mathcal{D}}{A}{B} of morphisms, together with cut and identity laws:

  1. cut: for each A,B,C\in\Ob{\mathcal{D}} and f\in \Hom{\mathcal{D}}{A}{B} and g\in\Hom{\mathcal{D}}{B}{C} , a morphism f;g\in\Hom{\mathcal{D}}{A}{C} .

  2. identity: for each A\in\Ob{\mathcal{D}} , a morphism 1\Sub{A}\in\Hom{\mathcal{D}}{A}{A} such that 1\Sub{A};f = f and f;1\Sub{B} for each f\in\Hom{\mathcal{D}}{A}{B} .

Notation (deductive system notation) [dpl-0003]
Given a deductive system \mathcal{D} , we will write A\in\mathcal{D} to mean A\in\Ob{\mathcal{D}} and f:A\vdash\Sub{\mathcal{D}} B when f\in\Hom{\mathcal{D}}{A}{B} . When \mathcal{D} is clear from context, we will write \vdash instead of \vdash\Sub{\mathcal{D}} .
Definition (linear and thunkable maps) [dpl-0004]

Let f:C \vdash D be a morphism in a deductive system \mathcal{D} .

  1. We say that f is linear when for all g:B\vdash C and h:A\vdash B , we have h;\prn{g;f} = \prn{h;g};f .

  2. We say that f is thunkable when for all g:D\vdash E and h : E\vdash F , we have f;\prn{g;h} = \prn{f;g};h .

Definition (positive and negative objects) [dpl-0005]
An object B in a deductive system \mathcal{D} is called positive when every map B\vdash C is linear; it is called negative when every map A\vdash B is thunkable.
Lemma (characterization of full associativity) [dpl-0007]

The following are equivalent for a deductive system \mathcal{D} :

  1. every map is linear;
  2. every map is thunkable;
  3. every object is positive;
  4. every object is negative;
  5. the cut law is associative;
  6. \mathcal{D} is a precategory.
Proof.

Supposing that every map is linear, we must check that each f:A\vdash B is thunkable. Fixing g:B\vdash C and h:C\vdash D , we must check that f;\prn{g;h} = \prn{f;g};h ; as h is assumed linear, the equation holds. The converse holds by identical reasoning.

Clearly every object is positive if and only if every map is linear; likewise, every object is negative if and only if every map is thunkable.

Finally, when every map is both linear and thunkable, the cut law is associative — but this is exactly the condition that the deductive system give rise to a precategory.

Polarization and Preduploids [dpl-0008]

Definition (polarized object) [dpl-000A]
An object A in a deductive system is called polarized when it is either positive or negative.
Definition (preduploid) [dpl-0009]
A deductive system \mathcal{D} is called a preduploid when every object A\in\mathcal{D} is polarized.

Foundations of Relative Category Theory [frct-003I]

We assume knowledge of basic categorical concepts such as categories, functors, and natural transformations. The purpose of this lecture is to develop the notion of a category over another category.

We will draw on the following materials:

Benedick Ahrens; Peter LeFanu Lumsdaine. Displayed Categories. In: Logical Methods in Computer Science. Mar 5, 2019. 10.23638/LMCS-15%281%3A20%292019. [ahrens-lumsdaine-2019]
We introduce and develop the notion of displayed categories. A displayed category over a category C is equivalent to “a category D and functor F : D \to C , but instead of having a single collection of “objects of D ” with a map to the objects of C , the objects are given as a family indexed by objects of C , and similarly for the morphisms. This encapsulates a common way of building categories in practice, by starting with an existing category and adding extra data/properties to the objects and morphisms. The interest of this seemingly trivial reformulation is that various properties of functors are more naturally defined as properties of the corresponding displayed categories. Grothendieck fibrations, for example, when defined as certain functors, use equality on objects in their definition. When defined instead as certain displayed categories, no reference to equality on objects is required. Moreover, almost all examples of fibrations in nature are, in fact, categories whose standard construction can be seen as going via displayed categories. We therefore propose displayed categories as a basis for the development of fibrations in the type-theoretic setting, and similarly for various other notions whose classical definitions involve equality on objects. Besides giving a conceptual clarification of such issues, displayed categories also provide a powerful tool in computer formalisation, unifying and abstracting common constructions and proof techniques of category theory, and enabling modular reasoning about categories of multi-component structures. As such, most of the material of this article has been formalised in Coq over the UniMath library, with the aim of providing a practical library for use in further developments.
Jean Bénabou. Fibered categories and the foundations of naïve category theory. [benabou-1985]
En hommage à Alexandre Grothendieck.
Francis Borceux. Handbook of Categorical Algebra 2: Categories and Structures. [borceux-hca-2]
A Handbook of Categorical Algebra is designed to give, in three volumes, a detailed account of what should be known by everybody working in, or using, category theory. As such it will be a unique reference. The volumes are written in sequence, with the first being essentially self-contained, and are accessible to graduate students with a good background in mathematics. Volume 1, which is devoted to general concepts, can be used for advanced undergraduate courses on category theory. After introducing the terminology and proving the fundamental results concerning limits, adjoint functors and Kan extensions, the categories of fractions are studied in detail; special consideration is paid to the case of localizations. The remainder of the first volume studies various ‘refinements’ of the fundamental concepts of category and functor.
Bart Jacobs. Categorical logic and type theory. Studies in Logic and the Foundations of Mathematics. Jan 14, 1999. [jacobs-1999]
This book is an attempt to give a systematic presentation of both logic and type theory from a categorical perspective, using the unifying concept of fibred category. Its intended audience consists of logicians, type theorists, category theorists and (theoretical) computer scientists.
Thomas Streicher. Fibred Categories à la Jean Bénabou. Dec 16, 2022. 10.48550/arXiv.1801.02927. [streicher-fcjb]
These are notes about the theory of Fibred Categories as I have learned it from Jean Benabou. I also have used results from the Thesis of Jean-Luc Moens from 1982 in those sections where I discuss the fibered view of geometric morphisms. Thus, almost all of the contents is not due to me but most of it cannot be found in the literature since Benabou has given many talks on it but most of his work on fibered categories is unpublished. But I am solely responsible for the mistakes and for misrepresentations of his views. And certainly these notes do not cover all the work he has done on fibered categories. I just try to explain the most important notions he has come up with in a way trying to be as close as possible to his intentions and intuitions. I started these notes in 1999 when I gave a course on some of the material at a workshop in Munich. They have developed quite a lot over the years and I have tried to include most of the things I want to remember.

These lecture notes are deeply influenced by Thomas Streicher.

Foundational Assumptions [frct-000R]

Definition (meta-category) [frct-001F]

A meta-category \mathfrak{C} is defined by explaining what an object of \mathfrak{E} is, and, given two objects x,y\in \mathfrak{E} , what a morphism from x to y is, together with the following operations:

  1. for each object x\in \mathfrak{E} , an identity map \Idn{x} : x \to x ,
  2. for any two maps f:x\to y and g:y\to z , a composite map f;g : x \to z ,
  3. such that the following equations hold:
    \Idn{x};h = h\qquad h;\Idn{y} = h\qquad f;(g;h) = (f;g);{h}
Remark (collections) [frct-003J]

In the definition of meta-category, we have not imposed any restrictions on what kinds of things the objects and morphisms are; our definition is pre-mathematical, so we do not assume beforehand that there is a such thing as a collection of “all” meta-categories.

We may define analogous notions of meta-functor, etc. But we do not assume that the notion of “all meta-functors \mathfrak{C}\to\mathfrak{D} ” is well-defined; the notion is entirely schematic.

Assumption. We assume a meta-category \BoldSymbol{\mathfrak{Coll}} whose objects we will refer to as “collections”. We assume that the meta-category of all collections satisfies the axioms of Lawvere’s ETCS.

Definition (category) [frct-001G]
A category E is defined to be a meta-category whose objects are defined to be the elements of some collection, and for any two objects x,y\in E the morphisms x\to y are defined to be the elements of some collection.
Remark (cartesian closure of the meta-category of all categories) [frct-003K]

Consequently there exists a meta-category \BoldSymbol{\mathfrak{Cat}} of all categories. Following Lawvere (but deviating from some other authors that ground the notion of meta-categories in classes) we notice that \BoldSymbol{\mathfrak{Cat}} is cartesian closed; in other words, all functor categories exist regardless of size.

Assumption. At times we may assume that there exists a category \SET\subseteq\BoldSymbol{\mathfrak{Coll}} of collections that we will refer to as sets, such that \SET is closed under the axioms of ETCS. Rather than work with \SET at all times, our approach is to use the tools of relative category theory to objectify the notions of “small” and “locally small” category over any category B , generalizing the role of \SET from classical category theory.

Displayed Categories and Fibrations [frct-0008]

Definition (displayed category) [frct-0000]

Let B be a category. A displayed category E over B is defined by the following data according to (Ahrens and Lumsdaine):

  1. for each object x\in B , a collection of displayed objects E\Sub{x} ,

  2. for each morphism \Mor{f}{x}{y}\in B and displayed objects \bar{x}\in E\Sub{x} and \bar{y}\in E\Sub{y} , a family of collections of displayed morphisms \Hom{E\Sub{f}}{\bar{x}}{\bar{y}} , an element of which shall denote by \DispMor{\bar{f}}{f}{\bar{x}}{\bar{y}} ,

  3. for each x\in B and \bar{x}\in E\Sub{x} , a displayed morphism \DispMor{\Idn{\bar{x}}}{\Idn{x}}{\bar{x}}{\bar{x}} ,

  4. for each \Mor{f}{x}{y} and \Mor{g}{y}{z} in B and objects \bar{x}\in E\Sub{x}, \bar{y}\in E\Sub{y}, \bar{z}\in E\Sub{z} , a function

    \Hom{E\Sub{f}}{\bar{x}}{\bar{y}} \times \Hom{E\Sub{g}}{\bar{y}}{\bar{z}} \to \Hom{E\Sub{f;g}}{\bar{x}}{\bar{z}}
    that we will denote like ordinary (diagrammatic) function composition,

  5. such that the following equations hold:

    \Idn{\bar{x}};\bar{h} = \bar{h}\qquad \bar{h};\Idn{\bar{y}} = \bar{h}\qquad \bar{f};(\bar{g};\bar{h}) = (\bar{f};\bar{g});\bar{h}
    Note that these are well-defined because of the corresponding laws for the base category B .

Notation (square brackets for subscripts) [frct-003R]
When we have too many subscripts, we will write E[x] instead of E\Sub{x} .

Definition (cartesian morphisms) [frct-0001]

Let E be displayed over B , and let \Mor{f}{x}{y} \in B ; a morphism \DispMor{\bar{f}}{f}{\bar{x}}{\bar{y}} in E is called cartesian over f when for any \Mor{m}{u}{x} and \DispMor{\bar{h}}{m;f}{\bar{u}}{\bar{y}} there exists a unique \DispMor{\bar{m}}{m}{\bar{u}}{\bar{x}} with \bar{m};\bar{f} = \bar{h} . We visualize this unique factorization of \bar{h} through \bar{f} over m as follows:

  \begin{tikzpicture}[diagram]
    \SpliceDiagramSquare{
      west/style = lies over,
      east/style = lies over,
      north/node/style = upright desc,
      height = 1.5cm,
      nw = \bar{x},
      ne = \bar{y},
      sw = x,
      north = \bar{f},
      south = f,
      se = y,
      nw/style = pullback,
    }
    \node (u') [above left = 1.5cm of nw,xshift=-.5cm] {$\bar{u}$};
    \node (u) [above left = 1.5cm of sw,xshift=-.5cm] {$u$};
    \draw[lies over] (u') to (u);
    \draw[->,bend left=30] (u') to node [sloped,above] {$\bar{h}$} (ne);
    \draw[->] (u) to node [sloped,below] {$m$} (sw);
    \draw[->,exists] (u') to node [desc] {$\bar{m}$} (nw);
  \end{tikzpicture}

Above we have used the “pullback corner” to indicate \bar{x}\to\bar{y} as a cartesian map. We return to this in our discussion of the self-indexing (the fundamental self-indexing) of a category.

Definition (cartesian fibration) [frct-0002]

A displayed category E over B is said to be a cartesian fibration, when for each morphism \Mor{f}{x}{y} and displayed object \bar{y}\in E\Sub{y} , there exists a displayed object \bar{x}\in E\Sub{x} and a cartesian morphism \DispMor{\bar{f}}{f}{\bar{x}}{\bar{y}} in the sense of cartesian morphisms. Note that the pair (\bar{x},\bar{f}) is unique up to unique isomorphism, so being a cartesian fibration is a property of a displayed category.

There are other variations of fibration. For instance, E is said to be an isofibration when the condition above holds just for isomorphisms f : x\cong y in the base.

The Fundamental Self-Indexing [frct-0003]

Construction (the fundamental self-indexing) [frct-001X]

Let B be an ordinary category; there is an important displayed category \SelfIx{B} over B given fiberwise by the slices of B .

  1. For x\in B , we define \SelfIx{B}\Sub{x} to be the collection \Sl{B}{x} of pairs (\bar{x}\in B,\Mor{p\Sub{x}}{\bar{x}}{x}) .
  2. For \Mor{f}{x}{y}\in B , we define \SelfIx{B}\Sub{f} to be the collection of commuting squares in the following configuration:
  \DiagramSquare{
    height = 1.7cm,
    nw = \bar{x},
    ne = \bar{y},
    sw = x,
    se = y,
    west = p\Sub{x},
    east = p\Sub{y},
    south = f,
    north = \bar{f},
    west/style = {->,exists},
    east/style = {->,exists},
    north/style = {->,exists},
  }
Exercise [frct-001Y]
Prove that \SelfIx{B} from the fundamental self-indexing is a cartesian fibration if and only if B has pullbacks.

The Generalized Pullback Lemma [frct-0014]

In light of the fundamental self-indexing, the following result for displayed categories generalizes the ordinary “pullback lemma.”

Lemma (generalized pullback lemma) [frct-001H]

Let \DispMor{\bar{f}}{f}{\bar{x}}{\bar{y}} , and suppose that \DispMor{\bar{g}}{g}{\bar{y}}{\bar{z}} is cartesian over g . Then \bar{f};\bar{g} is cartesian over f;g if and only if \bar{f} is cartesian over f .

  \begin{tikzpicture}[diagram]
    \SpliceDiagramSquare{
      height = 1.5cm,
      west/style = lies over,
      east/style = lies over,
      nw/style = pullback,
      sw = y,
      nw = \bar{y},
      se = z,
      ne = \bar{z},
      south = g,
      north = \bar{g},
    }
    \node (x*) [dotted pullback, left = of nw] {$\bar{x}$};
    \node (x) [left = of sw] {$x$};
    \draw[->] (x*) to node [above] {$\bar{f}$} (nw);
    \draw[lies over] (x*) to (x);
    \draw[->] (x) to node [below] {$f$} (sw);
  \end{tikzpicture}
Proof.

Suppose first that \bar{f} is cartesian. To see that \bar{f};\bar{g} is cartesian, we must construct a unique factorization as follows:

  \begin{tikzpicture}[diagram]
    \SpliceDiagramSquare{
      west/style = lies over,
      east/style = lies over,
      north/node/style = upright desc,
      height = 1.5cm,
      nw = \bar{x},
      ne = \bar{y},
      sw = x,
      north = \bar{f},
      south = f,
      se = y,
      nw/style = pullback,
      ne/style = pullback,
    }
    \node (z') [right = 2cm of ne] {$\bar{z}$};
    \node (z) [right = 2cm of se] {$z$};
    \draw[lies over] (z') to (z);
    \draw[->] (se) to node [below] {$g$} (z);
    \draw[->] (ne) to node [desc] {$\bar{g}$} (z');

    \node (u') [above left = 1.5cm of nw,xshift=-.5cm] {$\bar{u}$};
    \node (u) [above left = 1.5cm of sw,xshift=-.5cm] {$u$};
    \draw[lies over] (u') to (u);
    \draw[->,bend left=30] (u') to node [sloped,above] {$\bar{h}$} (z');
    \draw[->] (u) to node [sloped,below] {$m$} (sw);
    \draw[->,exists] (u') to (nw);
  \end{tikzpicture}

Because \bar{g} is cartesian, we can factor \bar{h} = i;\bar{g} for a unique \DispMor{i}{m;f}{\bar{u}}{\bar{y}} . Then, because \bar{f} is cartesian, we can further factor i = j;\bar{f} for a unique \DispMor{j}{m}{\bar{u}}{\bar{x}} . We conclude that there is a unique \DispMor{j}{m}{\bar{u}}{\bar{x}} for which \bar{h} = j;\bar{f};\bar{g} , as required.

Conversely, suppose that \bar{f};\bar{g} is cartesian. To see that \bar{f} is cartesian, we must construct a unique factorization as follows:

  \begin{tikzpicture}[diagram]
    \SpliceDiagramSquare{
      west/style = lies over,
      east/style = lies over,
      north/node/style = upright desc,
      height = 1.5cm,
      nw = \bar{x},
      ne = \bar{y},
      sw = x,
      north = \bar{f},
      south = f,
      se = y,
      ne/style = pullback,
    }
    \node (z') [right = 2cm of ne] {$\bar{z}$};
    \node (z) [right = 2cm of se] {$z$};
    \draw[lies over] (z') to (z);
    \draw[->] (se) to node [below] {$g$} (z);
    \draw[->] (ne) to node [desc] {$\bar{g}$} (z');

    \node (u') [above left = 1.5cm of nw,xshift=-.5cm] {$\bar{u}$};
    \node (u) [above left = 1.5cm of sw,xshift=-.5cm] {$u$};
    \draw[lies over] (u') to (u);
    \draw[->,bend left=30] (u') to node [sloped,above] {$\bar{h}$} (ne);
    \draw[->] (u) to node [sloped,below] {$m$} (sw);
    \draw[->,exists] (u') to (nw);
  \end{tikzpicture}

Because \bar{f};\bar{g} is cartesian, we can factor \bar{h};\bar{g} = i;\bar{f};\bar{g} for a unique \DispMor{i}{m}{\bar{u}}{\bar{x}} . On the other hand, because \bar{g} is cartesian, there is a unique \DispMor{j}{m;f}{\bar{u}}{\bar{y}} for which \bar{h};\bar{g} = j;\bar{g} ; as both \bar{h} and i;\bar{f} satisfy this condition, we conclude \bar{h}=i;\bar{f} . Therefore, there is a unique \DispMor{i}{m}{\bar{u}}{\bar{x}} for which \bar{h} = i;\bar{f} , as required.

An Alternative Definition of Fibration [frct-0029]

Warning. Some authors including Grothendieck give an equivalent definition of cartesian fibration that factors through a nonequivalent definition of cartesian morphisms. Such authors refer to our notion of cartesian morphism as hypercartesian (see Streicher).

Definition (hypocartesian morphisms) [frct-002A]

Let E be displayed over B , and let f:x\to y \in B ; a morphism \DispMor{\bar{f}}{f}{\bar{x}}{\bar{y}} in E is called hypocartesian over f when for any \bar{u}\in E\Sub{x} and \DispMor{\bar{h}}{f}{\bar{u}}{\bar{y}} there exists a unique \DispMor{i}{\Idn{x}}{\bar{u}}{\bar{x}} with i;\bar{f} = \bar{h} as follows:

  \begin{tikzpicture}[diagram]
    \SpliceDiagramSquare{
      west/style = lies over,
      east/style = lies over,
      north/node/style = upright desc,
      height = 1.5cm,
      nw = \bar{x},
      ne = \bar{y},
      sw = x,
      north = \bar{f},
      south = f,
      se = y,
    }
    \node (u') [above left = 1.5cm of nw,xshift=-.5cm] {$\bar{u}$};
    \node (u) [above left = 1.5cm of sw,xshift=-.5cm] {$x$};
    \draw[lies over] (u') to (u);
    \draw[->,bend left=30] (u') to node [sloped,above] {$\bar{h}$} (ne);
    \draw[double] (u) to (sw);
    \draw[->,exists] (u') to node [desc] {$i$} (nw);
  \end{tikzpicture}
Remark [frct-003G]
Cartesian morphisms are clearly hypocartesian (setting u=x and m=\Idn{x} ), but the converse does not hold. The problem is that in an arbitrary displayed category, hypocartesian morphisms may not be closed under composition.
Lemma (hypocartesian = cartesian in a cartesian fibration) [frct-002C]

Let E be a cartesian fibration in the sense of cartesian fibration, and let \DispMor{\bar{f}}{f}{\bar{x}}{\bar{y}} be displayed over \Mor{f}{x}{y} . The displayed morphism \bar{f} is cartesian if and only if it is hypocartesian.

Proof.

Any cartesian map is clearly hypocartesian. To see that a hypocartesian map \DispMor{\bar{f}}{f}{\bar{x}}{\bar{y}} in a cartesian fibration is cartesian, we consider the cartesian lift of \Mor{f}{x}{y} under \bar{y} :

\DiagramSquare{
  height = 1.5cm,
  west/style = lies over,
  east/style = lies over,
  nw/style = pullback,
  nw = \bar{x}\tick,
  ne = \bar{y},
  se = y,
  sw = x,
  south = f,
  north = \bar{f}\tick,
  north/style = {->,exists},
}

As the cartesian lift \bar{x}\tick\to \bar{y} is also hypocartesian, it follows that there is a unique vertical isomorphism identifying \bar{x} with \bar{x}\tick factoring \DispMor{\bar{f}}{f}{\bar{x}}{\bar{y}} through \DispMor{\bar{f}\tick}{f}{\bar{x}\tick}{\bar{y}} . Being cartesian over f is clearly stable under isomorphism, hence we conclude that \bar{f} is cartesian from the fact that \bar{f}\tick is cartesian.

Grothendieck defines a fibration in terms of (what we refer to as) hypocartesian morphisms rather than (what we refer to as) cartesian morphisms, and therefore imposes the additional constraint that the hypocartesian morphisms be closed under composition. In equivalence with Grothendieck's fibrations below, we verify that these two definitions of cartesian fibration coincide.

Lemma (equivalence with Grothendieck's fibrations) [frct-002B]

Let E be displayed over B . Then E is a cartesian fibration if and only if the following two conditions hold:

  1. Hypocartesian lifts. For each f:x\to y\in B and \bar{y}\in E\Sub{y} there exists a displayed object \bar{x}\in E\Sub{x} and hypocartesian morphism \bar{f}:\bar{x}\DispTo{f}\bar{y} .
  2. Closure under composition. If \bar{f}:\bar{x}\DispTo{f}\bar{y} and \bar{g}:\bar{y}\DispTo{g}\bar{z} are hypocartesian, then \bar{f};\bar{g} is hypocartesian.
Proof.

Suppose first that