Internal Diagrams and Archetypal Reasoning in Category Theory

Eduardo Ochs

Abstract. We can regard operations that discard information, like specializing to a particular case or dropping the intermediate steps of a proof, as projections, and operations that reconstruct information as liftings. By working with several projections in parallel we can make sense of statements like “Set is the archetypal Cartesian Closed Category”, which means that proofs about CCCs can be done in the “archetypal language” and then lifted to proofs in the general setting. The method works even when our archetypal language is diagrammatical, has potential ambiguities, is not completely formalized, and does not have semantics for all terms. We illustrate the method with an example from hyperdoctrines and another from synthetic differential geometry.

Mathematics Subject Classification (2010). Primary 18C50; Secondary 03G30.

1. Mental Space and Diagrams

My memory is limited, and not very dependable: I often have to rededuce results to be sure of them, and I have to make them fit in as little “mental space” as possible...

Different people have different measures for “mental space”; someone with a good algebraic memory may feel that an expression like Frob^{♮} : Σ_{f}(P ∧ f^{∗}Q) ⟶^{≅} Σ_{f}P ∧ Q is easy to remember, while I always think diagramatically, and so what I do is that I remember this diagram,

and I reconstruct the formula from it.

I cannot yet define precisely what it is to “think diagramatically”, but for the purposes of this paper a loose definition — or rather, a set of concepts and techniques for diagrammatical thinking, plus non-trivial consequences of “thinking” in that way — shall do. I will resort to a narrative device: I will speak as from a semi-fictional “I” who thinks as diagramatically as possible, and who always uses diagrams as a help for his bad algebraic thinking.

2. Projections and Liftings

Take the concept of “projection”, from the realm of covering spaces or from Linear Algebra. A projection map discards information — coordinates, maybe — and may collapse objects that were originally distinct.

I try to organize my diagrams to make the projection arrows — most of them, at least — go down. Figure 1 is an example.

Specialization acts like a projection. Look at the top arrow in Figure 1: except for the choice of a particular value for n, we have only lost information. Discarding intermediate steps, as in the bottom arrow, is a kind of erasing, and erasings are evidently projections.

[figure: \begin{aligned}2^{n+1} − 2^{n} & = & 2^{1+n} − 2^{n} \\ & = & 2 · 2^{n} − 1 · 2^{n} \\ & = & (2 − 1) · 2^{n} \\ & = & 2^{n} \end{aligned}; \begin{aligned}2^{100} − 2^{99} & = & 2^{1+99} − 2^{99} \\ & = & 2 · 2^{99} − 1 · 2^{99} \\ & = & (2 − 1) · 2^{99} \\ & = & 2^{99} \end{aligned}; \begin{aligned}2^{100} − 2^{99} & = & 2^{1+99} − 2^{99} \\ & = & 2 · 2^{99} − 1 · 2^{99} \\ & = & (2 − 1) · 2^{99} \\ & = & 2^{99} \end{aligned}; 2^{100} − 2^{99} = 2^{99}]

Figure 1. A specialization and an erasing.

The opposite of to project is to lift; projecting is easy, lifting is hard. A projection map, p : E → B, may have any number of preimages for a point b in the base space — one, many, none —, and, to make things worse, we will often be interested in very specific cases where we are somehow able to recognize whether a given lifting is “good” or not — for example, we may be looking for the “right” generalization for 2^{100} − 2^{99} = 2^{99} —, but where we are unable to define exactly what a “good lifting” is.

[figure: \begin{matrix}{a, b ≡ p : A×B \atop b ≡ π′p : B} π′ & b ↦ c ≡ f : B → C \\ c ≡ f(π′p) : C \end{matrix} app; \begin{matrix}{p : A×B \atop π′p : B} π′ & f : B → C \\ f(π′p) : C \end{matrix} app; \begin{matrix}{a, b ≡ p : A×B \atop b ≡ π′p : B} π′ & b ↦ c ≡ f : B → C \\ c ≡ f(π′p) : C \end{matrix} app; \begin{aligned}{a, b \atop b} π′ & & b ↦ c \\ & c \end{aligned} app; \begin{matrix}{p : A×B \atop π′p : B} π′ & f : B → C \\ f(π′p) : C \end{matrix} app; \begin{matrix}{p \atop π′p} π′ & f \\ f(π′p) \end{matrix} app; \begin{matrix}{p : A×B \atop π′p : B} π′ & f : B → C \\ f(π′p) : C \end{matrix} app; \begin{aligned}{A×B \atop B} & B → C \\ & C \end{aligned}; \begin{aligned}{a, b \atop b} π′ & & b ↦ c \\ & c \end{aligned} app; \begin{aligned}{a, b \atop b} & b ↦ c \\ & c \end{aligned}; \begin{aligned}{A×B \atop B} & B → C \\ & C \end{aligned}; \begin{aligned}{a, b \atop b} & b ↦ c \\ & c \end{aligned}; \begin{matrix}{p \atop π′p} π′ & f \\ f(π′p) \end{matrix} app; \begin{matrix}p & f \\ f(π′p) \end{matrix}; \begin{aligned}{A×B \atop B} & B → C \\ & C \end{aligned}; \begin{aligned}A×B & B → C \\ & C \end{aligned}; \begin{aligned}{a, b \atop b} & b ↦ c \\ & c \end{aligned}; \begin{aligned}a, b & b ↦ c \\ & c \end{aligned}; \begin{aligned}A×B & B → C \\ & C \end{aligned}; \begin{aligned}a, b & b ↦ c \\ & c \end{aligned}]

Figure 2. Downcased types.

3. Downcased Types

Suppose that we have a point p ∈ A × B and a function f : B → C. There is a single “obvious” way to build a point of C starting from this data. It is “obvious” because we have a search method that finds it; it is related to proof search (via the Curry-Howard isomorphism). Here’s how it works, briefly and informally.

A point p ∈ A × B is a pair made of an ‘a’ and a ‘b’. If we allow “long names” for variables we can replace the ‘p’ by another name, that reflects its type more closely; so let’s rename ‘p’ to ‘a, b’. Similarly, an f : B → C is an operation that takes each ‘b’ to a ‘c’, so let’s rename ‘f’ to ‘b ↦ c’. Now, with this new notation, we are looking for an operation that takes an ‘a, b’ and a ‘b ↦ c’ and produces a term that “deserves the name” ‘c’. We start at the tree in the lower right rectangle in Figure 2, and we want to arrive at the tree in the lower left; both trees have the same shape, and by relating them we will see that the term corresponding to c is f(π′p). Note that in this new language — “Downcased Types” — we have no syntactical distinction between variables and non-atomic terms.

All the solid arrows in Figure 2 are erasings. The dashed arrows are “uppercasings” when we go rightwards, “downcasings” when we go to the left; note that ‘×’ is downcased to ‘,’, and ‘→’ is downcased to ‘↦’. If we start at the lower left and we move right through the dashed arrow, we get the types of the (three) objects involved; what we still need to do from there is a kind of “term inference”...

“Type inference” is very well-known, and polymorphic languages like Haskell and ML implement algorithms for it; “term inference”, on the other hand, is rarely mentioned in the literature, but techniques like parametricity ([Wad89], [BJP10]) provide useful meta-theorems about properties that all possible inferrable terms must obey. It would be lovely if these techniques could do term inference for us, algorithmically — but they can’t, so when we need to infer terms we usually do the work by hand.

As term inference is hard, let’s turn our attention to something easier, and looser. “Inference” carries the connotation of something that can be done algorithmically, without any previous knowledge of the result. We will focus on the process of “reconstructing” the desired term, c ≡ f(π′p), from the downcased tree in the lower left of Figure 2. A “reconstruction” may need hints to be completed, and may depend on making the right choices at some points, motivated by unformalizable bits of common sense, or by intuition, hindsight, or by vague rememberances, by a sense of good style, or whatever else. A “reconstruction” is the result of an incomplete algorithm (or a “method”, rather than an “algorithm”); when we perfect a method for reconstruction, and finish filling up all its gaps, it becomes an “inference algorithm”.

For our purposes, “reconstruction” will be enough — and real “inference” will be close to impossible.

4. The Dictionary

The downcased notation has to be used with care, as it doesn’t come with any built-in devices to protect us from ambiguities. For example, we could have tried to find a term “deserving the name” ‘a, a ↦ a, a’ — and there are four different ones!...

One way to avoid this problem is to consider that the downcased “names” are just that, names, and that we have a dictionary that associates to each name its meaning.

In the case of λ-calculus, a dictionary relating each downcased name to its meaning can be extracted from a derivation tree (if all the rule names are present), and the derivation tree can be reconstructed from its associated dictionary. For example,

[figure: \begin{aligned}{a, b \atop b} π′ & & b ↦ c \\ & c \end{aligned} app; \begin{aligned}⟨⟨b⟩⟩ & := & π′⟨⟨a, b⟩⟩ \\ ⟨⟨c⟩⟩ & := & ⟨⟨b ↦ c⟩⟩⟨⟨b⟩⟩ \end{aligned}; \begin{aligned}{a, b \atop b} π′ & & b ↦ c \\ & c \end{aligned} app; \begin{aligned}⟨⟨b⟩⟩ & := & π′⟨⟨a, b⟩⟩ \\ ⟨⟨c⟩⟩ & := & ⟨⟨b ↦ c⟩⟩⟨⟨b⟩⟩ \end{aligned}]

and if we add to that dictionary the entries

\begin{aligned}⟨⟨a, b⟩⟩ & := & p \\ ⟨⟨b ↦ c⟩⟩ & := & f \end{aligned}

then we can reconstruct the tree

\begin{matrix}{p \atop π′p} π′ & f \\ f(π′p) \end{matrix} app

from that. Note that we use double angle brackets, ⟨⟨·⟩⟩, to separate names from one another and to distinguish them from standard notation, and that we use ‘≡’ to indicate change of notation — usually between downcased and standard.

5. Internal Diagrams

Several of the initial ideas for the system of downcased types came from attempts to formalize something that I will call “physicist’s notation”, and that should be familiar to most readers; I have never seen any detailed formalizations of it, though.

Suppose that we have a function f : ℝ → ℝ, and we draw the graph of y = f(x). Then, given points x_{0}, x_{1}, x_{2}, x′ on the “x-axis” we have default meanings for the names y_{0}, y_{1}, y_{2}, y′: namely, y_{0} := f(x_{0}), y′ := f(x′), and so on. It makes sense to write X for the domain of f and Y for its codomain, and if we draw the “internal diagram” (as in [LS97], p.14) of the map f, we get this:

[figure: external view; internal view; standard notation; downcased notation; X; Y; f; x; f(x); x_{0}; y_{0}; x_{1}; y_{1}; x′; y′; ⋮; ⋮; x_{n}; y_{n}; x_{2}; y_{2}; x_{n}; y_{n}; x; y]

Note that for each name like x_{2} of a point in the x-axis (the “space of ‘x’s”, X) we have chosen a similar name for a point in the y-axis (the “space of ‘y’s”, Y). We will call the implicit operation on names the syntactical action of the function f ≡ x ↦ y; in the case above, the syntactical action replaced the ‘x’ of each original name into a ‘y’, and kept all the “decorations” unchanged.

The syntactical action does not need to be defined for all possible names of points in X — in fact, we restrict ourselves to “good” names of points in X exactly to make the syntactical action easier to describe.

Now let’s take a function less abstract: \sqrt{·} : ℕ → ℝ. Its action is implicit in its name (“\sqrt{·} ”), and if we examine its internal diagram,

[figure: external view; internal view; standard notation; downcased notation; ℕ; ℝ; ^{\sqrt{·}}; n; _{\sqrt{n}}; 0; 0; 1; 1; 2; _{\sqrt{2}}; ⋮; ⋮; n; _{\sqrt{n}}; 2; _{\sqrt{2}}; n; _{\sqrt{n}}; n; r]

we may conclude that it should be possible to use ‘n ↦ \sqrt{n}’ as its name; or even ‘2 ↦ \sqrt{2}’ — “the function that takes 2 to \sqrt{2}, for every value of ‘2’ ”...

As the reader may have guessed, there is no clear separation between what are “good names” and “bad names” for an object; instead we have a murky line. We have just seen in the first example that ‘x_{0}’, ‘x′’, etc, can all be downcasings for ‘X’, and maybe the ‘1’ in second example, if taken as a name, should be uppercaseable both as ℕ and as ℝ... The trick is all in our use of the dictionary: we can define the meaning of ‘n ↦ \sqrt{n}’ to be \sqrt{·} : ℕ → ℝ, and, if we feel that #_{$}^{!} is a good name for the square root, we can define it to stand for the square root too...

6. Parallel Notations

We are using two notations — downcased and standard — in parallel; it is possible to use more. One way to visualize what is going on is to think in terms of computer interfaces. Imagine a user inspecting huge data structures by displaying them on a computer screen in several forms — he can toggle switches that control what gets shown and what is omitted.

The downcased notation of the previous sections is my compromise between my intuition and a formalization. Suppose that someone has created a third notation, that he claims that is much closer to his intuitions. He can set the controls to display only his favorite notation, as in the left side of the diagram below; or he can display all together at the same time — as at the top.

[figure: all that together; ineffable purely intuitive thought; all that together; \begin{matrix}{a, b ≡ p : A×B \atop b ≡ π′p : B} π′ & b ↦ c ≡ f : B → C \\ c ≡ f(π′p) : C \end{matrix} app; \begin{matrix}{a, b ≡ p : A×B \atop b ≡ π′p : B} π′ & b ↦ c ≡ f : B → C \\ c ≡ f(π′p) : C \end{matrix} app; \begin{aligned}{a, b \atop b} & b ↦ c \\ & c \end{aligned}; \begin{matrix}{a, b ≡ p : A×B \atop b ≡ π′p : B} π′ & b ↦ c ≡ f : B → C \\ c ≡ f(π′p) : C \end{matrix} app; \begin{matrix}{p : A×B \atop π′p : B} π′ & f : B → C \\ f(π′p) : C \end{matrix} app]

Figure 3. Parallel notations.

Working with three parallel notations is similar to working with two.

At this point our two notations, downcased and standard, generate trees with exactly the same shapes; in the next section we will begin to compare diagrams done in different notations, but having the same shapes; and starting on section 13 the parallelism will be looser — there will be correspondences between trees and dictionaries, on one side, and “strictly 2-dimensional” categorical diagrams, on another. In all cases it is convenient to work in a “projected view”, yet pretend that we are in the situation with total information — that the rest of the information “is there”, but hidden.

7. Functors

Fix a set A. It induces a functor (A×), that takes each set B to A × B and each function f : B → C to a function (A×)f : A × B → A × C. Let’s use the subscripts ‘0’ and ‘1’ to distinguish the two actions of a functor: (A×)_{0} is its action on objects (sets, in this case), (A×)_{1} is its action on morphisms (i.e., on functions).

It is quite common in the literature of Category Theory to see things like: “let (A×) : Set → Set the functor that takes each set B to A × B”. The action on morphisms is not described — it is “obvious”, and it is left to the reader to discover. The reader should apply a kind of search algorithm to find it. Which algorithm is this?

Let’s downcase this problem. The action on objects takes each “space of ‘b’s” to a “space of ‘a, b’s”; its syntactical action is to prepend an ‘a,’. The action on morphisms takes each b ↦ c to an a, b ↦ a, c — i.e., the syntactical action on morphisms consists of applying the syntactical action on objects to

[figure: Set; Set; (A×); B; A×B; external view; internal view; B; A×B; (A×)_{0}; C; A×C; B; C; f; (A×)_{1}; A×B; A×C; (A×)f; b; a, b; c; a, c; b; c; a, b; a, c; standard notation; downcased notation]

(a) Downcasing the functor (A×).

[figure: {b ↦ c \atop a, b ↦ a, c} (A×)_{1}; \begin{aligned}{[a, b]^{1} \atop a} & \begin{aligned}{[a, b]^{1} \atop b} & & b ↦ c \\ & c \end{aligned} \\ & a, c \end{aligned} ; a, b ↦ a, c ; 1; \begin{aligned}{[a, b]^{1} \atop a} & \begin{aligned}{[a, b]^{1} \atop b} & & b ↦ c \\ & c \end{aligned} \\ & a, c \end{aligned} ; a, b ↦ a, c ; 1; \begin{matrix}{[p]^{1} \atop πp} & \begin{matrix}{[p]^{1} \atop π′p} & f \\ f(π′p) \end{matrix} \\ ⟨πp, f(π′p)⟩ \end{matrix} ; λp:(A×B).⟨πp, f(π′p)⟩ 1]

(b) A way to reconstruct the “obvious” part.

Figure 4. Functors.

both the domain and the codomain. This is a general pattern: in all functors the two syntactical actions will be related in this way.

The diagram in Figure 4a is very similar to the ones in the previous section, but there the blobs were sets and they had points; now the blobs — which we are no longer drawing — are categories, that have objects, and between these objects we may have morphisms. Also, the downcasing is changing the notation more than before, and we are downcasing the ‘↦’s that were functor actions as ‘⇒’. The ‘⇒’ is to remind us that: 1) something non-obvious is going on — points of B are not being taken to points of A×B, instead the whole set B was fed into (A×)_{0}, and we got back A × B —, and 2) that ‘b ⇒ a, b’ is two actions.

So, we know just the “name” of the action on morphisms of this functor. How do we reconstruct its “meaning”? The answer is obtained by liftings, as in Figure 4b; we find that (A×)f := λp:A × B.⟨πp, f(π′p)⟩.

8. Natural Transformations

Now fix two sets, A and A′, and a map α : A → A′. We have natural constructions for functors (A×) and (A′×), and, besides that, a natural transformation (“NT”, from now on), (α×), going from (A×) to (A′×). An NT has a single action, that takes objects to morphisms.

We will need a convention. If X and Y are objects of a category C, then both f : X → Y and X →^{f} Y will denote a morphism, but X → Y will denote the full hom-set Hom_{C}(X, Y). With that convention, if F, G : A → B are functors and T : F →^{.} G is a NT, we can represent the internal view of T as:

A ↦ (F A →^{T A} GA).

Let’s take the convention up one level: A →^{.} (F A →^{T A} GA) will denote a specific NT, but A →^{.} (F A → GA) will mean the class of all NTs from F to G; and we downcase ‘→^{.}’ as ‘→^{•}’; see Figures 5a and 5b.

We know the “syntactical action” of (α×): it is B ↦ (A×B →^{α×B} A′×B) in standard notation, b →^{•} (a, b ↦ a′, b) after downcasing. To obtain a “meaning” for that we can apply the same procedure as in the previous section; we discover that α×B := λp : A×B.⟨f(πp), π′p⟩.

Now let’s look at the notations for the general case. Let F, G : A → B be functors, and T : F →^{.} G be an NT between them. Everything is similar, but we need a way to downcase the objects F A and GA... a good choice is as ‘a^{F} ’ and ‘a^{G}’ — because the idea of “an a^{F} ” suggests nothing at all, and so it reminds us that the functors F and G may be abstract.

We often have to deal with categories whose objects don’t have any reasonable notion of “elements”. If our B is a category like that, then a^{F} ↦ a^{G} will be a name for a morphism, but the names ‘a^{F} ’ and ‘a^{G}’ “will not have semantics” — our dictionary will not attribute any meanings to them. See [Krö07], especially its sections 3.3.4.4 and 5.3.2.1, for a discussion; our downcased notation is, in a sense, “a language for diagram chasing”.

9. Adjunctions

Fix an object B of Set, and let’s write B→C for C^{B}. Then we have a functor (B→) : Set → Set, whose syntactical action is C ↦ (B→C), in standard notation, and c ⇒ b ↦ c after downcasing. This functor is right adjoint to (×B) : Set → Set, and we will represent that diagrammatically as a square: Figure 6a.

The two transpositions, cur and uncur, are natural transformations with actions:

(A^{op}, C) ↦ ((A×B →^{f} C) ↦ (A →^{cur f} (B→C)))

(A^{op}, C) ↦ ((A →^{g} (B→C)) ↦ (A×B →^{uncur g} C))

where A^{op} is an object of Set^{op}, and (A^{op}, C) is an object of Set^{op} × Set.

[figure: A×; Set; Set; A′×; α×; B; α×B; B; A×B; A×; B; A′×B; A′×; B; .; B; α×; A×B; A′×B; α×B; b; a, b; b; a′, b; b; •; a, b; a′, b; external view; internal view; standard notation; downcased notation]

(a) The NT (α×) : (A×) →^{.} (A′×).

[figure: F; A; B; G; T; A; T A; A; F A; F; A; GA; G; A; .; A; T; F A; GA; T A; a; a^{F}; a; a^{G}; a; •; a^{F}; a^{G}; external view; internal view; standard notation; downcased notation]

(b) The generic case: T : F →^{.} G.

Figure 5. Natural transformations

The notation in the general case is similar. An adjunction L ⊣ R is represented diagrammatically as the square in Figure 6b.

We will usually draw L as going left, R as going right, and call the transpositions ‘♭’ and ‘♯’. Note that in a square drawn in this way the adjunction L ⊣ R itself, viewed “externally”, would be something vertical: \begin{matrix}L \\ ⊥ \\ R \end{matrix} — but its maps between hom-sets are horizontal arrows.

[figure: Set; Set; (×B); Set; Set; (B→); A×B; A; (×B); C; B→C; (B→); A×B; C; uncur g; A×B; C; f; uncur; cur; A; B→C; g; A; B→C; cur f; a, b; a; c; b ↦ c; a, b; c; a; b ↦ c; external view; internal view; standard notation; downcased notation]

(a) The adjunction (×B) ⊣ (B→).

[figure: B; A; L; B; A; R; LA; A; L; B; RB; R; LA; B; g^{♭}; LA; B; f; ♭; ♯; A; RB; g; A; RB; f^{♯}; a^{L}; a; b; b^{R}; a^{L}; b; a; b^{R}; external view; internal view; standard notation; downcased notation]

(b) Notation for a general case: L ⊣ R.

Figure 6. Adjunctions.

Just as a functor is two actions plus two properties — namely, that the action on morphisms respects identities and composition —, a natural isomorphism can be thought as two NTs going in opposite directions, plus the assurance that their composites are identities; the downcased squares for the (×B) ⊣ (B→) and L ⊣ R adjunctions in the Figures 6a and 6b can be considered as being (two-dimensional) downcased names themselves (for natural isomorphisms), having the same meaning as their “linearized” versions,

\begin{matrix}(a^{op}; c) →^{•} ((a, b ↦ c) ↔ (a ↦ (b ↦ c))) \\ (a^{op}; b) →^{•} ((a^{L} ↦ c) ↔ (a ↦ b^{R})) \end{matrix}

and those meanings can either be the 6-uples

(Set, Set, (×B), (B→), uncur, cur)
(A, B, L, R, ♭, ♯)

or longer tuples including, say, the properties and the unit and the counit of the adjunction. The possibility of changing some definitions while keeping the notations the same will be very important in sections 19 and 21, where that will be used to “project out” from the definitions all components which involve equalities of morphisms, keeping only the constructions.

10. Transmission

A good way to understand how reconstruction works is to think on a simpler, more extreme case. When I reconstruct something that I have half-forgotten, I do have vague memories about it... how do they act? On the other hand, if I am reconstructing something that I have received from someone else in an incomplete, but reconstructible, form, then the vague memories are out of the picture.

Consider the following diagram, which describes, in a simplistic way, how a theorem T, discovered by an author A and published in a paper P, is read and understood by a reader R. In the diagram the time flows to the left, and knowledge flows (roughly) downwards.

[figure: A_{0}; A_{2}; T_{1}; T_{2}; T_{3}; P; T′_{0}; T′_{1}; R_{0}; R_{1}]

The theorem was discovered in the form T_{1}, but in order to make it transmissible the author changed it a bit, and it became T_{2}, then T_{3} in written form, which was what got published. The author was also slightly transformed in the process, and at the time of the publication he had become A_{2}.

That particular theorem was difficult to state, so the reader R started (as R_{0}) by understanding just parts of its statement; let’s call that preliminary object understood by our reader a “statement with holes”. Then, through weeks of study, more and more of the theorem’s statement, and of the proof of the theorem (let’s use the term “theorem” to refer to both the statement and the proof), became clear to R, up to the point where the object in R’s mind has become T′_{1}, which no longer has any holes; all gaps have been filled, the statement is now clearly a consequence of its proof, and our reader R, who at this point has become a slightly different person, R_{1}, now has even some intuition about the theorem (whatever that means)...

Our reader R has reconstructed, in his mind, the author A’s theorem, from what was published in the paper P. R’s task was harder than the task I face when I try to reconstruct a theorem that at some point I knew — if I review all that I have studied before, I should be able to fill up all my gaps, but R has no guarantee that just by looking in the literature he will be able to find all the missing knowledge he needs... even though we expect published papers to be clear enough, and complete enough.

The process of reconstruction performed by R ought to be considered an algorithm — even though we know that what R did to understand the paper P was, at best, a “method”. Let’s see why, by examining an ideal case.

Suppose that the A wanted to be clear, that he was lucid in his choice of exposition, and that the paper P was submitted to a journal with no space constraints. So A, and also his editors and referees, want the paper P to be as readable as possible. The reader R_{0} receives the paper P being aware that the theorem T_{3} in it should be readable, and starts to devote his time to understand T_{3}. After a few weeks R succeeds.

What did the reader R do? And what did A and the journal’s editors do to be sure that A would succeed in his task?

When R checks the paper’s details and fills up the gaps his process is akin to proof search, and thus a kind of lifting... What R does is too complex to be formalizable as an “algorithm”; yet the author and the editors are aware of what their intended readers are expected to be able to do, and they added to the paper enough “hints” to let the readers succeed — so the reader performs a “proof search with hints”. There are algorithms that do proof searches with hints, so let’s commit an abuse of language here and take the analogy with algorithms seriously: the reader R is performing a proof search with hints, and A provided enough hints in the paper P to be sure that, given P as input, the reader R will check its theorems completing all the missing details, then stop.

Let’s now suppose that both A and R are people whose thinking is mostly diagrammatical, like the semi-fictional “me”. How does does R (re)construct in his mind some “intuition” about the theorems? The theorem T_{3} was published in algebraic form, so part of R’s task — and he needs to do this to be able to fill the logical gaps — is to find the diagrams to let him reason about the paper; another part of his task is to work out the details in the paper’s examples; for that he needs to take his “general” diagrams and apply them to particular cases; this is specialization, as in Section 2. What we call “intuition” should comprise the ability to specialize, plus a lot more.

11. Intuition

When R finally understands the paper P he would have developed some “intuitions” about the theorem T. His intuitions may or may not be the same as A’s, so let’s name them differently: I_{A} for the author’s intuitions, I_{R} for the reader’s.

Instead of taking the easy way and saying that “it is impossible to talk about what mathematical intuition is”, we will improvise a simple model that will let us talk about some aspects of having intuition about a theorem. Let’s suppose that that theorem T says that when the hypotheses H_{1} and H_{2} hold, then the conclusion C_{2} also does; and the proof of T is made of two lemmas, L_{1} and L_{2}, and structured like this:

\begin{matrix}{H_{1} \atop C_{1}} L_{1} & H_{2} \\ C_{2} \end{matrix} L_{2}

so the stronger theorem H_{1} ∧ H_{2} ⊢ C_{1} ∧ C_{2} is also true. Note that the tree above represents T′_{1}, not T_{3}; T_{3} was written in a “linear”, “algebraic” way, to comply with the usual mathematical practice, even though both A and R tend to think diagrammatically.

The reader R_{1} is able to do several things with T′_{1}; most of them can be understood diagrammatically, as movements through parts of the diagram below. Let’s use the following convention (that will hold for this diagram only): a double bar with the name of a lemma at its right will stand for all the steps in the lemma — they are known, but are not visible —, while a double bar without a label will mean a situation where the intermediate steps are not known at that moment, and will have to be reconstructed.

\begin{matrix}{H_{1} \atop C_{1}} L_{1} & H_{2} \\ C_{2} \end{matrix} L_{2}

{H_{1} \atop C_{1}} L_{1}

(1)

[figure]

\begin{matrix}{H_{1} \atop C_{1}} L_{1} & H_{2} \\ C_{2} \end{matrix} L_{2}

\begin{matrix}{H_{1} \atop C_{1}} & H_{2} \\ C_{2} \end{matrix}

(2)

[figure]

\begin{matrix}{H_{1} \atop C_{1}} L_{1} & H_{2} \\ C_{2} \end{matrix} L_{2}

H_{1}[C := Set] ; C_{1}[C := Set] L_{1} H_{2}[C := Set]

C_{2}[C := Set] L_{2}

(3)

[figure]

[figure]

{H_{1} \atop C_{1}} L_{1}

H_{1} ⊢ C_{1}

(4)

[figure]

\begin{matrix}{H_{1} \atop C_{1}} & H_{2} \\ C_{2} \end{matrix}

H_{1}, H_{2} ⊢ C_{2}

(5)

[figure]

H_{1}[C := Set] ; C_{1}[C := Set] L_{1} H_{2}[C := Set]

C_{2}[C := Set] L_{2}

H_{1}[C:=Set], H_{2}[C:=Set] ⊢ C_{2}[C:=Set]

(6)

[figure]

The center box is a sketch of the full proof, and the small box below it is the statement of the full theorem. If the reader R_{1} remembers any of those, he can reconstruct the other one by projecting or lifting through (5). The box at the top is the full proof, and R_{1} can reconstruct it by completing the sketch of the proof, lifting through (2).

One day R_{1} decides to present the theorem to some colleagues. He assigns a temporal order to the lemmas: “Lemma L_{1} has to be presented first”. Its statement and its proof are obtained by projecting through (1) and (4). Note that (1) is a case of zooming in into a part of the proof.

R_{1} is also able to use the theorem. He can apply it to a particular case, projecting through (3) and (6) or just through (3) (compare that with the arrow (3) in Figure 8). He can also reuse the structure of parts of the proof, but changing the theorem in deeper ways (e.g., in the Curry-Howard isomorphism); this is not shown above.

We will pretend that “having intuition about a theorem” means having the abilities discussed above: remembering parts, reconstructing, zooming out, zooming it, temporal order, transmission, specializing, reusing the structure.

12. Skeletons of proofs

Let’s call the “projected” version of a mathematical object its “skeleton”. The underlying idea in this paper is that for the right kinds of projections, and for some kinds of mathetical objects, it should be possible to reconstruct enough of the original object from its skeleton and few extra clues — just like paleontologists can reconstruct from a fossil skeleton the look of an animal when it was alive.

Now the irresistible questions are: which kinds of objects do have skeletons? What do these skeletons look like? How does the reconstruction process work, and how much of it can be performed by computers? When is it that the liftings become ambiguous, what kinds of hints are needed, and how should we specify them? And in what situations is this idea doomed to fail, because for each non-trivial way of separating the object’s data into “skeleton” and “non-skeleton” something doesn’t work?

Answering all this in a general setting is obviously a daunting task. A first natural step, though, is to start from a handful of natural examples — and then say: these are our archetypal examples of skeletons, projections, and liftings. How do we formalize and generalize what we got here?

In Section 19 we will sketch an approach that may yield a reasonbably rich family of examples: namely, that on a sizeable fragment of Category Theory all definitions can be split into a structure part plus properties, and each theorem into a construction plus an equational part. A big part of Mathematics is definitions plus theorems — and in that fragment of Category Theory these can be clearly split into a “syntactical” skeleton, with just the “structures” and “constructions”, plus, on top of that, a reconstructible, “equational” flesh. We will call the system with just this skeleton the “syntactical world”.

It would be very hard to explain precisely the general ideas here before first showing a language on which they can make sense, so we will now look at some examples. We will have to use hyperdoctrines, even though they are weaker, less familiar, and harder to define than toposes; that’s because of technical difficulties that we will discuss in section 20.

13. Hyperdoctrines

Let’s take the beginning of the definition of a hyperdoctrine ([Law69], [Law70], [See83], [Tay86], [Jac99]). A hyperdoctrine is a cloven fibration p : 𝔼 → 𝔹, where the “base category” 𝔹 has finite products and each fiber 𝔼_{B} is cartesian closed, plus for each morphism f : A → B in 𝔹 adjoints Σ_{f} ⊣ f^{∗} ⊣ Π_{f} for the change-of-base functor f^{∗}, plus more structure; but let’s skip the “plus more structure” part for the moment — we will describe that extra structure briefly at Section 14, and the full details can be found at [Och10].

It turns out that this definition generalizes a familiar object: the “codomain fibration”, Cod : Set^{↣} → Set — that we will abbreviate as Pred — is a hyperdoctrine. Actually Pred can be considered to be the archetypical hyperdoctrine, in a sense that can be made precise; we will return to “generalizations” and “archetypes” in Section 16.

An object P of Set^{↣} is a monic: P ≡ (A′ ↣ A). A morphism P → Q in Set^{↣}, where Q ≡ (B′ ↣ B), is a pair of arrows (f′ : A′ → B′, f : A → B) making the obvious square commute. The projection functor Cod takes P ≡ (A′ ↣ A) to A and (f′, f) : P → Q to f.

A monic with codomain A, (A′ ↣ A), is said to be a subobject of A. In Set we have canonical subobjects — the ones whose maps are inclusions — and we can think of them as being predicates over sets. We will have a special shorthand for predicates: instead of writing, for example,

{ (x, y) ∈ X × Y | P (x, y) } ↪ X × Y

we will write just:

{ x, y || P xy }

The double bar in ‘{ x, y || P xy }’ is to remind us that this is two objects, plus a map; and we write the ‘↣’ as ‘↪’ when we want to stress that the map is an inclusion.

We will draw objects of 𝔼 above their projections, and we’ll usually omit the projection arrows. We will downcase a predicate like ‘{ x, y || P xy }’ in diagrams as just ‘P (x, y)’ — the ‘x, y’ part can be recovered by looking down.

Let’s focus on what happens in Pred. For a map f : A → B in 𝔹, the change-of-base functor f^{∗} takes each predicate { b || P (b) } over B to a predicate { a || P (f(a)) } over A. When f is a projection map, like π : X × Y → X, the adjoints Σ_{π} and Π_{π} “are” ∃y and ∀y (Figure 7a); when f is the “diagonal” map Δ : B → B × B or the “dependent diagonal” δ : A × B → A × B × B, the adjoints “are” the operations ‘b=b′∧’ and ‘b=b′ [figure]’ (Figure 7b). This is not hard to believe if we start with the right examples, and we check first the particular cases and then generalize. Take X = {0, 1, 2, 3, 4}, Y = {3, 4}, A = {0}, B = {0, 1, 2, 3}, and let’s use a positional notation for predicates: we will write \{ x, y || x ≥ y \} as {00001 \atop 00011} , i.e.:

\begin{matrix}\{ (4,4), \\ (3,3),(4,3)\} \end{matrix} ↪ \begin{matrix}\{(0,4),(1,4),(2,4),(3,4),(4,4), \\ (0,3),(1,3),(2,3),(3,3),(4,3)\} \end{matrix}

In Figures 7a and 7b the left side shows the abstract view, the right side shows a very particular case, and in the middle, in downcased notation, we see how these change-of-base functors and their adjoints act on arbitrary predicates. Also, each arrow ‘↔’ in an adjunction square stands for two transpositions, one in each direction. Let’s establish another convention: P → f^{∗}Q is an hom-set, but P ⊢ f^{∗}Q is (the name of) a morphism — we have

[figure: P; Σ_{π}P; P; π^{∗}Q; Σ_{π}P; Q; π^{∗}Q; Q; π^{∗}Q; R; Q; Π_{π}R; R; Π_{π}R; X×Y; X; π; P xy; ∃y.P xy; P xy; Qx; ∃y.P xy; Qx; Qx; Qx; Qx; Rxy; Qx; ∀y.Rxy; Rxy; ∀y.Rxy; x, y; x; π; {00001 \atop 00011}; 00011; {00001 \atop 00011}; {00111 \atop 00111}; 00011; 00111; {00111 \atop 00111}; 00111; {00111 \atop 00111}; {01111 \atop 11111}; 00111; 01111; {01111 \atop 11111}; 01111; X×Y; X; π]

(a) Adjoints to π^{∗} (quantifiers).

A×B A×B×B_{δ} [figure]  a, b  a, b, b′_{b′:=b}[figure]  A×B A×B×B_{δ} [figure] P  Σ_{δ}P [figure] P δ^{∗}Q [figure]  Σ_{δ}P Q[figure] [figure] [figure] δ^{∗}Q  Q [figure] δ^{∗}Q R[figure]  Q Π_{δ}R [figure] [figure] [figure] R  Π_{δ}R [figure]  P ab b=b′∧P ab [figure] P ab Qabb [figure] b=b′∧P ab Qabb′ [figure] [figure] [figure] Qabb  Qabb′ [figure] Qabb Rab [figure]  Qabb′ b=b′ [figure]Rab [figure] [figure] [figure] Rab b=b′ [figure]Rab [figure]  _{1 0 0 0}  _{0001 0000 0000 0000} [figure]_{1 0 0 0}_{1 1 0 0} [figure]  _{0001 0000 0000 0000}_{0011 0011 0011 0000} [figure] [figure] [figure]_{1 1 0 0}  _{0011 0011 0011 0000} [figure]_{1 1 0 0}_{1 1 1 0} [figure]  _{0011 0011 0011 0000}_{1111 1111 1111 0111} [figure] [figure] [figure]_{1 1 1 0}  _{1111 1111 1111 0111} [figure]

(b) Adjoints to δ^{∗} (equality).

{ a || P (a) } { b || ∃a.f(a)=b ∧ P (a) } [figure] { a || P (a) } { a || Q(f(a)) } [figure]  { b || ∃a.f(a)=b ∧ P (a) } { b || Q(b) } [figure] [figure] [figure] { a || Q(f(a)) }  { b || Q(b) } [figure] { a || Q(f(a)) } { a || R(a) } [figure]  { b || Q(b) } { b || ∀a.f(a)=b [figure]R(a) } [figure] [figure] [figure] { a || R(a) } { b || ∀a.f(a)=b [figure]R(a) } [figure] A  B_{f}  [figure]

(c) Adjoints to an arbitrary change-of-base functor.

Figure 7. Adjoints to change-of-base in a hyperdoctrine.

P ⊢ f^{∗}Q : P → f^{∗}Q. With that convention we can write the transpositions rules (cf. the “mate rules” in [Jac99]) as:

{Q ⊢ Π_{π}R \atop π^{∗}Q ⊢ R} ∀^{♭}  {x; Qx ⊢ ∀y.Rxy \atop x, y; Qx ⊢ Rxy} ∀^{♭}

A fibration p : 𝔼 → 𝔹

plus for each f : A → B in 𝔹 adjoints Σ_{f} ⊣ f^{∗} ⊣ Π_{f}

[figure: 𝔼_{A}; 𝔼_{B}; Σ_{f}; 𝔼_{A}; 𝔼_{B}; f^{∗}; 𝔼_{A}; 𝔼_{B}; Π_{f}; ⊥; ⊥; 𝔼; 𝔹; p; A; B; f]

[figure: Set_{X×Y}^{↪}; Set_{X}^{↪}; Σ_{π}; Set_{X×Y}^{↪}; Set_{X}^{↪}; π^{∗}; Set_{X×Y}^{↪}; Set_{X}^{↪}; Π_{π}; ⊥; ⊥; Set^{↪}; Set; Cod; X×Y; X; π]

[figure: P; Σ_{f}P; P; f^{∗}Q; Σ_{f}P; Q; f^{∗}Q; Q; f^{∗}Q; R; Q; Π_{f}R; R; Π_{f}R; A; B; f]

[figure: {00001 \atop 00011}; 00011; {00001 \atop 00011}; {00111 \atop 00111}; 00011; 00111; {00111 \atop 00111}; 00111; {00111 \atop 00111}; {01111 \atop 11111}; 00111; 01111; {01111 \atop 11111}; 01111; X×Y; X; π]

A fibration p : 𝔼 → 𝔹

plus for each f : A → B in 𝔹 adjoints Σ_{f} ⊣ f^{∗} ⊣ Π_{f}

[figure: 𝔼_{A}; 𝔼_{B}; Σ_{f}; 𝔼_{A}; 𝔼_{B}; f^{∗}; 𝔼_{A}; 𝔼_{B}; Π_{f}; ⊥; ⊥; 𝔼; 𝔹; p; A; B; f]

(1)

[figure]

[figure: 𝔼_{A}; 𝔼_{B}; Σ_{f}; 𝔼_{A}; 𝔼_{B}; f^{∗}; 𝔼_{A}; 𝔼_{B}; Π_{f}; ⊥; ⊥; 𝔼; 𝔹; p; A; B; f]

[figure: P; Σ_{f}P; P; f^{∗}Q; Σ_{f}P; Q; f^{∗}Q; Q; f^{∗}Q; R; Q; Π_{f}R; R; Π_{f}R; A; B; f]

(2)

[figure]

[figure: 𝔼_{A}; 𝔼_{B}; Σ_{f}; 𝔼_{A}; 𝔼_{B}; f^{∗}; 𝔼_{A}; 𝔼_{B}; Π_{f}; ⊥; ⊥; 𝔼; 𝔹; p; A; B; f]

[figure: Set_{X×Y}^{↪}; Set_{X}^{↪}; Σ_{π}; Set_{X×Y}^{↪}; Set_{X}^{↪}; π^{∗}; Set_{X×Y}^{↪}; Set_{X}^{↪}; Π_{π}; ⊥; ⊥; Set^{↪}; Set; Cod; X×Y; X; π]

(3)

[figure]

[figure: P; Σ_{f}P; P; f^{∗}Q; Σ_{f}P; Q; f^{∗}Q; Q; f^{∗}Q; R; Q; Π_{f}R; R; Π_{f}R; A; B; f]

[figure: {00001 \atop 00011}; 00011; {00001 \atop 00011}; {00111 \atop 00111}; 00011; 00111; {00111 \atop 00111}; 00111; {00111 \atop 00111}; {01111 \atop 11111}; 00111; 01111; {01111 \atop 11111}; 01111; X×Y; X; π]

(4)

[figure]

[figure: Set_{X×Y}^{↪}; Set_{X}^{↪}; Σ_{π}; Set_{X×Y}^{↪}; Set_{X}^{↪}; π^{∗}; Set_{X×Y}^{↪}; Set_{X}^{↪}; Π_{π}; ⊥; ⊥; Set^{↪}; Set; Cod; X×Y; X; π]

[figure: {00001 \atop 00011}; 00011; {00001 \atop 00011}; {00111 \atop 00111}; 00011; 00111; {00111 \atop 00111}; 00111; {00111 \atop 00111}; {01111 \atop 11111}; 00111; 01111; {01111 \atop 11111}; 01111; X×Y; X; π]

(5)

[figure]

Figure 8. How the hyperdoctrine diagrams in Figure 7 were obtained.

{π^{∗}Q ⊢ R \atop Q ⊢ Π_{π}R} ∀^{♯}  {x, y; Qx ⊢ Rxy \atop x; Qx ⊢ ∀y.Rxy} ∀^{♯}

Note that ‘⊢’ has different meanings in standard and in downcased notations. We will only use ‘⊢’ to refer to vertical morphisms.

It turns out that it is possible to define the adjoints Σ_{f} ⊣ f^{∗} ⊣ Π_{f} in Pred, for an arbitrary f : A → B, from just f^{∗}, Σ_{π}, Π_{π}, Σ_{δ}, Π_{δ}. The transpositions and the functor actions implicit in the adjunction diagram in Figure 7c above can be expressed as derived rules. The proof is hard (see [See83]); we will see how to understand it diagrammatically in [Och10].

What really matters here is: how were the diagrams above obtained? Look at Figure 8; it shows some of the projections involved. We start with the definition in English, at the top. By representing

it diagrammatically (projection (1)) we lose the subtleties of the English language — see [Fre76] and [FS90] for a diagrammatic notation in which at least the quantifiers are preserved — but we add positional notation. The projections (3) and (4) are specializations: we take 𝔼 := Set^{↪}, p := Cod, A := X ×Y, and so on. The arrows (2) and (5) produce internal diagrams, as in the section 9. The downcased diagrams are not shown; Figure 8 is a map of interesting projections, and it could have been far larger than it is.

14. Preservations, Frobenius, Beck-Chevalley

The complete definition of a hyperdoctrine is what we have seen in the last section, plus these properties:

• each f^{∗} preserves, modulo iso, the ⊤, the ∧, and the [figure]of each fiber;

• the Frobenius Property holds,

• the Beck-Chevalley Condition holds.

We can regard these properties as structure. They can all be stated in the same way: for f : A → B in 𝔹 and for predicates P and Q over B, we have natural constructions P⊤^{♮}, P∧^{♮}, P [figure]^{♮}, Frob^{♮}, that produce arrows that we want to be isos; so we establish rules P⊤, P∧, P [figure], Frob, that produce arrows going in the opposite directions of the previous ones.

{f : A → B \atop f^{∗}⊤_{B} ⊢ ⊤_{A}} P⊤^{♮}  {f : A → B \atop ⊤_{A} ⊢ f^{∗}⊤_{B}} P⊤

\begin{matrix}f & P & Q \\ f^{∗}(P ∧Q) ⊢ f^{∗}P ∧f^{∗}Q \end{matrix} P∧^{♮}  \begin{matrix}f & P & Q \\ f^{∗}P ∧f^{∗}Q ⊢ f^{∗}(P ∧Q) \end{matrix} P∧

\begin{matrix}f & Q & R \\ f^{∗}P ∧f^{∗}Q ⊢ f^{∗}(Q [figure]R) \end{matrix} P [figure]^{♮}  \begin{matrix}f & Q & R \\ f^{∗}(Q [figure]R) ⊢ f^{∗}P [figure]f^{∗}Q \end{matrix} P [figure]

\begin{matrix}f & P & Q \\ Σ_{f}(P ∧f^{∗}Q) ⊢ (Σ_{f}P)∧Q \end{matrix} ^{Frob^{♮}}  \begin{matrix}f & P & Q \\ Σ_{f}(P ∧f^{∗}Q) ⊢ (Σ_{f}P)∧Q \end{matrix} Frob

The natural construction for the Frob^{♮} arrow is given by the diagram below. Note that it shows both Frob^{♮} (going rightwards, shortened to just ‘♮’) and Frob:

[figure: P; Σ_{f}P; P ∧f^{∗}Q; P; Σ_{f}(P ∧f^{∗}Q); Σ_{f}P; (Σ_{f}P)∧Q; Σ_{f}P; f^{∗}Q; Q; P ∧f^{∗}Q; f^{∗}Q; Σ_{f}(P ∧f^{∗}Q); Q; (Σ_{f}P)∧Q; Q; P ∧f^{∗}Q; Σ_{f}(P ∧f^{∗}Q); Σ_{f}(P ∧f^{∗}Q); (Σ_{f}P)∧Q; ♮; Σ_{f}(P ∧f^{∗}Q); (Σ_{f}P)∧Q; Frob; A; B; f]

Similarly to what we have done in the section 4, we can extract from the diagram above a dictionary defining some names in terms of the others; note that due to our conventions P ∧f^{∗}Q → P is a hom-set, but P ∧f^{∗}Q ⊢ P is a particular morphism, and we can treat it as a name. By expanding the definitions in Σ_{f}(P ∧f^{∗}Q) ⊢ (Σ_{f}P)∧Q, we obtain a definition for the Frob^{♮} rule:

\begin{matrix}f & P & Q \\ Σ_{f}(P ∧f^{∗}Q) ⊢ (Σ_{f}P)∧Q \end{matrix} ^{Frob^{♮}} :=

\begin{matrix}\begin{matrix}P & \begin{matrix}f & Q \\ f^{∗}Q \end{matrix} c.o.b. \\ P ∧f^{∗}Q ⊢ P \end{matrix} ; π & f \\ Σ_{f}(P ∧f^{∗}Q) ⊢ Σ_{f}P \end{matrix} Σ_{f} \begin{matrix}P & \begin{matrix}f & Q \\ f^{∗}Q \end{matrix} c.o.b. \\ P ∧f^{∗}Q ⊢ f^{∗}Q \end{matrix} ; π′ ; Σ_{f}(P ∧f^{∗}Q) ⊢ Q ; ^{Σ_{f}^{♭}}

Σ_{f}(P ∧f^{∗}Q) ⊢ (Σ_{f}P)∧Q ⟨, ⟩

The diagram also says that the arrow generated by the Frob rule is inverse to the arrow generated by the (derived) rule Frob^{♮}. This is by a convention: in a ‘⇆’ the two arrows are the two directions of an iso.

The statement of the Beck-Chevalley Condition (“BCC” from now on) is slightly more complex: it requires four arrows in 𝔹. For any commutative square in 𝔹 as below,

[figure: f^{′∗}P; P; f^{′∗}P; z^{′∗}f^{∗}Σ_{z}P; f^{′∗}P; f^{′∗}z^{∗}Σ_{z}P; P; z^{∗}Σ_{z}P; z^{′∗}f^{∗}Σ_{z}P; f^{′∗}z^{∗}Σ_{z}P; f^{′∗}z^{∗}Σ_{z}P; z^{∗}Σ_{z}P; f^{′∗}P; Σ_{z′}f^{′∗}P; P; Σ_{z}P; z^{′∗}f^{∗}Σ_{z}P; f^{∗}Σ_{z}P; z^{∗}Σ_{z}P; Σ_{z}P; f^{∗}Σ_{z}P; Σ_{z}P; Σ_{z}P; Σ_{z}P; id; Σ_{z′}f^{′∗}P; f^{∗}Σ_{z}P; ♮; Σ_{z′}f^{′∗}P; f^{∗}Σ_{z}P; BCCL; X×_{Y} Z; Z; f′; X×_{Y} Z; X; z′; Z; Y; z; X; Y; f]

and any object P over Z, we have a natural construction for an arrow:

BCCL^{♮} : Σ_{z′}f^{′∗}P → f^{∗}Σ_{z}P

The rule BCCL says that when f, f′, z, z′ form a pullback the arrow BCCL^{♮} has an inverse, BCCL:

\begin{matrix}f & z & f′ & z′ & P \\ f^{∗}Σ_{z}P ⊢ Σ_{z′}f^{′∗}P \end{matrix} BCCL

We will sometimes write BCCL^{♮} and BCCL together as an iso, and call that iso BCCL (by a slight abuse of language); and we simplify the diagram for Beck-Chevalley by drawing only its square in 𝔹 and on top of it the two faces of the cube in 𝔼 that border on the missing edge. We will sometimes draw the arrows generated by P⊤, P∧, P [figure]and Frob as isos, too.

15. The Eq-Elim rule

The main interest of hyperdoctrines is that they are exactly the categories in which we can interpret (a certain system of typed, intuitionistic) firstorder logic. The proof of this includes a way to interpret each deduction rule of first-order logic categorically, and another “translation” going in the opposite direction.

Let’s look at a tiny part — possibly the hardest one — of these translations.

The rule for equality-elimination in Natural Deduction can be formulated as this ([See83], p.507):

\begin{matrix}b=b′ & Qabb \\ Qabb′ \end{matrix} =E

Categorically, it will become this morphism (we will call it =E):

{ a, b, b′ || b=b′∧Qabb } ⊢ { a, b, b′ || Qabb′ }

There are three different natural constructions in a hyperdoctrine for objects deserving the name { a, b, b′ || b=b′∧Qabb }. We will use this one in =E:

\begin{matrix}a, b, b′↦b, b′ & \begin{matrix}b↦b, b′ & \{ b || ⊤ \} \\ \{ b, b′ || b=b′ \} \end{matrix} Σ_{0} \\ \{ a, b, b′ || b=b′ \} \end{matrix} ; c.o.b. \begin{matrix}a, b, b′↦a, b & \begin{matrix}a, b↦a, b, b′ & \{ a, b, b′ || Qabb′ \} \\ \{ a, b || Qabb \} \end{matrix} c.o.b. \\ \{ a, b, b′ || Qabb′ \} \end{matrix} ; c.o.b.

{ a, b, b′ || b=b′∧Qabb′ } ∧

\overline{π}′ \begin{matrix}Δ & ⊤_{B} \\ Σ_{Δ}⊤_{B} \end{matrix} Σ_{0} \overline{π}^{′∗}Σ_{Δ}⊤_{B} c.o.b. \begin{matrix}\overline{π} & \begin{matrix}δ & Q \\ δ^{∗}Q \end{matrix} c.o.b. \\ \overline{π}^{∗}δ^{∗}Q \end{matrix} ; c.o.b.

\overline{π}^{′∗}Σ_{Δ}⊤_{B}∧\overline{π}^{∗}δ^{∗}Q ∧

Note that \overline{π} : A×B×B → A×B is the projection on the first two coordinates, and \overline{π}′ : A×B×B → B×B the projection on the last two coordinates. To show that the rule =E can be interpreted in a hyperdoctrine we need a way to construct, for arbitrary objects A, B in the base category and an arbitrary predicate Q over A×B×B, a morphism \overline{π}^{′∗}Σ_{Δ}⊤_{B} ∧ \overline{π}^{∗}δ^{∗}Q ⊢ Q. We will construct it as a composite of three maps.

Take P := ⊤_{B} = \{ b || ⊤ \}, f := \overline{π}^{∗}, z := Δ, z′ := δ, f′ := π′ in the diagram for Beck-Chevalley. Then the BCCL iso says that two different categorical constructions for { a, b, b′ || b = b′ } are isomorphic, and by drawing also the P⊤ iso and its image by Σ_{δ} we get isos between the three different categorical constructions for { a, b, b′ || b = b′ }:

Now look at the diagram in Figure 9a. The arrow Frob^{′♮} (going rightwards, shortened to ♮) is built in the same way as Frob^{♮}, but using the maps ! and ≅ in place of π and π′. In any fibration we have natural isos f^{∗}g^{∗}P ↔ (f; g)^{∗}P and id^{∗}P ↔ P (for diagrammatic proofs for that, see [Och10]), and as δ; \overline{π} = id, this gives us the map ≅. The arrow Frob′ is

[figure: ⊤_{A×B}; Σ_{δ}⊤_{A×B}; δ^{∗}Q; ⊤_{A×B}; Σ_{δ}δ^{∗}Q; Σ_{δ}⊤_{A×B}; (Σ_{δ}⊤_{A×B})∧\overline{π}^{∗}δ^{∗}Q; Σ_{δ}⊤_{A×B}; δ^{∗}Q; Σ_{δ}δ^{∗}Q; Σ_{δ}δ^{∗}Q; (Σ_{δ}⊤_{A×B})∧\overline{π}^{∗}δ^{∗}Q; ♮; Σ_{δ}δ^{∗}Q; (Σ_{δ}⊤_{A×B})∧\overline{π}^{∗}δ^{∗}Q; _{Frob_{′}}; δ^{∗}Q; δ^{∗}\overline{π}^{∗}(δ^{∗}Q); ≅; Σ_{δ}δ^{∗}Q; \overline{π}^{∗}δ^{∗}Q; (Σ_{δ}⊤_{A×B})∧\overline{π}^{∗}δ^{∗}Q; \overline{π}^{∗}δ^{∗}Q; δ^{∗}\overline{π}^{∗}(δ^{∗}Q); \overline{π}^{∗}δ^{∗}Q; \overline{π}^{∗}δ^{∗}Q; δ^{∗}Q; δ^{∗}Q; Σ_{δ}δ^{∗}Q; δ^{∗}Q; δ^{∗}Q; id; Σ_{δ}δ^{∗}Q; Q; ϵ_{Q}; δ^{∗}Q; Q; A×B; A×B×B; δ; A×B×B; A×B; \overline{π}; A×B; A×B; id]

(a) The components ‘Frob′’ and ϵ_{Q} of the (=E) map (standard)

[figure: ⊤; b=b′; Qabb; ⊤; b=b′∧Qabb; b=b′; b=b′∧Qabb; b=b′; Qabb; b=b′∧Qabb; b=b′∧Qabb; b=b′∧Qabb; ♮; b=b′∧Qabb; b=b′∧Qabb; _{Frob_{′}}; Qabb; Qabb; ≅; b=b′∧Qabb; Qabb; b=b′∧Qabb; Qabb; Qabb; Qabb; Qabb; Qabb; Qabb; b=b′∧Qabb; Qabb; Qabb; id; b=b′∧Qabb; Qabb′; ϵ_{Q}; Qabb; Qabb′; a, b; a, b, b′; b′:=b; a, b, b′; a, b; a, b; a, b; id]

(b) The components ‘Frob′’ and ϵ_{Q} of the (=E) map (downcased)

Figure 9. (=E) via Frobenius

the inverse of Frob^{′♮}; its construction (not shown) is an easy consequence of Frobenius. The map ε_{Q} is a counit for the adjunction Σ_{δ} ⊣ δ^{∗}.

If Q ≡ { a, b, b′ || Qabb′ } then we can downcase the diagram above into the one in Figure 9b; the arrow =E is the composite in Figure 10c.

[figure: ⊤_{A×B}; π^{′∗}⊤_{B}; P⊤; π^{′∗}⊤_{B}; ⊤_{B}; ⊤_{A×B}; Σ_{δ}⊤_{A×B}; π^{′∗}⊤_{B}; Σ_{δ}π^{′∗}⊤_{B}; ⊤_{B}; Σ_{Δ}⊤_{B}; Σ_{δ}⊤_{A×B}; Σ_{δ}π^{′∗}⊤_{B}; Σ_{δ}⊤_{A×B}; \overline{π}^{′∗}Σ_{Δ}⊤_{B}; i; Σ_{δ}π^{′∗}⊤_{B}; \overline{π}^{′∗}Σ_{Δ}⊤_{B}; BCCL; \overline{π}^{′∗}Σ_{Δ}⊤_{B}; Σ_{Δ}⊤_{B}; A×B; B; π′; A×B; A×B×B; δ; B; B×B; Δ; A×B×B; B×B; _{\overline{π}_{′}}]

(a) The iso ‘i’ used to build (=E) (standard)

[figure: ⊤; ⊤; P⊤; ⊤; ⊤; ⊤; b=b′; ⊤; b=b′; ⊤; b=b′; b=b′; b=b′; b=b′; b=b′; i; b=b′; b=b′; BCCL; b=b′; b=b′; a, b; b; π′; a, b; a, b, b′; δ; b; b, b′; Δ; a, b, b′; b, b′; _{\overline{π}_{′}}]

(b) The iso ‘i’ used to build (=E) (downcased)

[figure: Σ_{δ}δ^{∗}Q; (Σ_{δ}⊤_{A×B})∧\overline{π}^{∗}δ^{∗}Q; ^{Frob′}; Σ_{δ}δ^{∗}Q; Q; ε_{Q}; (Σ_{δ}⊤_{A×B})∧\overline{π}^{∗}δ^{∗}Q; \overline{π}^{′∗}Σ_{Δ}⊤_{B}∧\overline{π}^{∗}δ^{∗}Q; i×\overline{π}^{∗}δ^{∗}Q; Q; \overline{π}^{′∗}Σ_{Δ}⊤_{B}∧\overline{π}^{∗}δ^{∗}Q; =E; b=b′∧Qabb; b=b′∧Qabb; b=b′∧Qabb; Qabb′; b=b′∧Qabb; b=b′∧Qabb; Qabb′; b=b′∧Qabb; =E]

(c) The map (=E) as a composite

Figure 10. (=E) as a composite

16. Archetypal Models

Imagine that we have placed side to side the downcased and the standard diagrams of the last section.

When we go from downcased to standard — e.g, from { a, b || b=b′ ∧ Qabb } to Σ_{δ}δ^{∗}Q — we are attributing a precise meaning to a (potentially ambiguous) “name”; however, when we go in the opposite direction, from standard to downcased, we are “attributing meaning” in another sense: we are giving an “intuitive meaning” (or better: “intuitive content”) to something that, if we had received it in an article, as in the section 10, could have felt initially as something purely abstract...

I had to make some “informal definitions” in the course of this paper, using terms that I could not define precisely, like diagrammatical reasoning, reconstruction, and intuition... I will have to make a few more.

The archetypal model for a structure — for example, the archetypal model for a hyperdoctrine, which is going to be Pred — is a particular case of that structure that “suggests” a certain “language” for working on that structure — i.e., for doing constructions and proofs on it. That “archetypical language” does not need to be unambiguous — think

in { a, b || b=b′ ∧Qabb } and its several different precise meanings —, does not need to have a downcased version — in section 13 the internal diagrams were what mattered, the downcasings were mentioned just in passing —, and does not need to be convenient for expressing all possible constructions. What is relevant is that the archetypical language, when used side-to-side with the “algebraic” language, should give us a way to reason, both intuitively and precisely, about the structure we’re working on; in particular, it should let us formulate reasonable conjectures quickly, and check them with reasonable ease... but what are “reasonable conjectures”, and where do they come from?

If we want to be able to reconstruct a theory from minimal information we need to have ways to: 1) generate “reasonable conjectures”, 2) filter out those which are either impossible or too hard to prove, 3) prove the others. Bounded proof search takes care of points (1) and (2); to give a partial answer to (1) we will concentrate our attention on Category Theory — more specifically, on situations where we are trying to generalize a “base case”. There we have two (non-disjoint) sources of “reasonable conjectures”: 1a) constructions and proofs that make sense and hold in the base case, that we may expect to generalize; 1b) language. Our choice of names for objects in a hyperdoctrine gave us several different formal meanings for { a, b || b=b′ ∧ Qabb } — we expect them to be at least equivalent modulo isomorphism. This is similar to writing a + b + c instead of a + (b + c) or (a + b) + c: our choice of language “suggests” that a + (b + c) = (a + b) + c.

An “archetypal example”, in which all the main ideas appear, is:

Set is the archetypical CCC.

17. Cartesian Closed Categories

A Cartesian Closed Category (C, ×, 1, →) is a category C plus a “cartesian closed structure” (×, 1, →) on it. The following diagram fixes the (categorical) notation that we will use for the operations induced by (×, 1, →):

[figure: A; B; f; A; B×C; ⟨f,g⟩; A; C; g; B; B×C; π; B×C; C; π′; A; 1; !; A×B; A; A×B; C; uncurg; A×B; C; f; A; B→C; g; A; B→C; curf; C; B→C]

Each of its three parts can be attributed a precise meaning, as we did with the adjunction square in section 9; and if we regard each of them as a different adjunction (see [Awo06], pages 182 and 188, for the three adjunctions), then we get the equations that these operations have to obey.

The Big Theorem is: CCCs are exactly the categorical models for the simply-typed λ-calculus with pairs and unit.

The precise, “standard” statement for that theorem, including definitions, statements, and proofs, is quite long. Amazingly, it can be reconstructed from just this downcased diagram,

[figure: a; b; a; b, c; a; c; b; b, c; b, c; c; a; ∗; a, b; a; a, b; c; a; b ↦ c; c; b ↦ c]

plus this downcasing of the Natural Deduction rules for ∧, ⊤, and [figure]:

\begin{matrix}\begin{matrix}a ; ⋮ . ; b & a ; ⋮ . ; c \\ b, c \end{matrix} ⟨, ⟩ & {b, c \atop b} π {b, c \atop c} π′ \\ {a \atop ∗} & ! \\ \begin{aligned}a ; ⋮ . ; b & a ; ⋮ . ; b ↦ c \\ & c \end{aligned} app & a [b]^{1} ; ⋮ . ; c ; b ↦ c λ; 1 \end{matrix}

Starting from that, we uppercase the downcased diagram in the following way, that makes clear how an intermediate, “sequent-like” form (as in [LS86], pp.47–49), should behave:

[figure: A; B; a⊢b; A; B×C; a⊢⟨b,c⟩; A; C; a⊢c; B; B×C; p⊢πp; B×C; C; p⊢πp′; A; 1; a⊢∗; A×B; A; A×B; C; a,b⊢fb; A×B; C; a,b⊢c; A; B→C; a⊢f; A; B→C; a⊢λb:B.c; C; B→C]

Then the next steps are to state precisely:

• the syntax and the rules of the type system,

• the operations of a CCC,

• the translation of each of the rules of the type system,

• the translation of each of the operations of the CCC,

• the reductions and conversions of the type system,

• the equations obeyed by the operations of a CCC, and then we have to prove that the CCC equations are respected by the translation to λ-calculus, and that the λ-calculus equations are respected by the translation to categories.

We also need to allow “impurities” in both the λ-calculus and in the CCCs. Take a look at the CCC of the next section: it has extra constants — an object A and morphisms ⌜0⌝, ⌜1⌝, +, · — that do not exist in all CCCs, and these constants obey certain equations. In a Pure Type System ([Geu93]) extra constants and equations are not allowed, but in theorems like the Big Theorem above ([Jac99] has many more like it) we allow in the type system exactly the kinds of constants and equations that are easy to interpret in the categorical models. The kinds of allowed “impurities” are usually defined in the beginning, in the definition of the type system and of the categorical structure, but this can be delayed until after the translations are presented.

18. Objects of Line Type

Our approach also works in cases where we do have an archetypical language with clear intuitive content, but where we have no concrete archetypical model besides a term model built purely syntactically. Through this section let’s pretend that we do not know Synthetic Differential Geometry ([Koc80], [Bel08], [MR91]).

Let (A, ⌜0⌝, ⌜1⌝, +, ·) be a commutative ring in a CCC. That means: we have a diagram

[figure: 1; A; ⌜0⌝; 1; A; ⌜1⌝; A; A×A; +; A; A×A; ·; ∗; 0; ∗; 1; a + b; a, b; ab; a, b]

and the morphisms ⌜0⌝, ⌜1⌝, +, · behave as expected.

Let D be the set of zero-square infinitesimals of A, i.e., { ε ∈ A | ε^{2} = 0 }; D can be defined categorically as an equalizer. If we take A := ℝ, then D = {0}; but if we let A be a ring with nilpotent infinitesimals, then {0} ⊊ A.

The main theorem of [Koc77] says that if the map

\begin{aligned}α : & A × A & → & (D→A) \\ & (a, b) & ↦ & λε:D.(a + bε) \end{aligned}

is invertible, then we can use α and α^{−1} to define the derivative of maps from A to A — every morphism f : A → A in the category C will be “differentiable” —, and the resulting differentiation operation f ↦ f′ behaves as expected: we have, for example, (fg)′ = f′g + fg′ and (f ∘ g)′ = (f′ ∘ g)g′.

Commutative rings with the property that their map α is invertible are called ring objects of line type. ROLTs are hard to construct, so most of the proofs about them have to be done in a very abstract setting. However, if we can use the following downcasings for α and α^{−1} — note that β = (α^{−1}; π), that γ = (α^{−1}; π′), and that these notations do not make immediately obvious that α and α^{−1} are inverses —,

[figure: A; A×A; π; A×A; A; π′; A; (D→A); β; A×A; (D→A); α; A×A; (D→A); α^{−1}; A; (D→A); γ; a; a, b; π; a, b; b; π′; a; (ε ↦ a + bε); β; a, b; (ε ↦ a + bε); α; b; (ε ↦ a + bε); γ; f(0); (f(0), f′(0)); π; (f(0), f′(0)); f′(0); π′; f(0); (ε ↦ f(ε)); β; (f(0), f′(0)); (ε ↦ f(ε)); α^{−1}; f′(0); (ε ↦ f(ε)); γ]

then all the proofs in the first two sections of [Koc77] can be reconstructed from half-diagrammatic, half-λ-calculus-style proofs, done in the archetypal language, where the intuitive content is clear. This will be shown in a sequel to [Och10].

19. The syntactical world

We can now explain our archetypal projection: the one from the “real world” to the “syntactical world” for a fragment of Category Theory, that we mentioned in section 12.

We have been avoiding all mentions to equations between morphisms — for example, in the section 9 we glossed over the usual standard requirement that f^{♯♭} = f. That was deliberate.

A category C is a 7-uple,

C = (C_{0}, Hom_{C}, id_{C}, ∘_{C}; assoc_{C}, idL_{C}, idR_{C})

where the three last components are assurances that the composition ∘_{C} is associative and that the identities behave as expected with respect to composition at the left and the right. These three last components are exactly the ones whose typings — all this can be formalized in an adequate type system — involve equalities of morphisms. By dropping them we get what we will call the proto-category associated to C:

C^{−} = (C_{0}, Hom_{C}, id_{C}, ∘_{C})

The same idea can be applied to lots of categorical structures. We can define, in a similar way, proto-functors, proto-natural transformations, protoisos, proto-adjunctions, proto-products, proto-terminals, proto-exponentials, proto-cartesian-closed categories, a proto-Yoneda lemma, proto-fibrations, and so on. Also, it turns out that many categorical proofs can be projected onto their corresponding “proto-proofs”, by dropping all parts that involve equalities of morphisms — and the resulting proto-proofs keep the constructions of the original proofs, but leave out the diagram chasings. This is explained in great detail, with many diagrams, at [Och10].

20. The problem with toposes

Elementary toposes are very simple to define — an elementary topos is just a CCC with pullbacks and a classifier object — and it is well-known that they are exactly the categorical models for a certain (intuitionistic) fragment of Set Theory (called “IST” in [Bel88]). Why did we have to resort to clumsy hyperdoctrines?

The problem is that we can’t define classifier object without defining monic arrow first; all my attempts to find a usable definition of “proto-monic” have failed rather miserably^{1}, so I can’t rely on either “proto-classifiers” or “proto-toposes”. This means that if I had to stick with toposes I wouldn’t be able to apply the idea of “projection into the syntactical world” to the metatheory, i.e., to the categorical models for the polymorphic type theory needed to formalize the projection from the real world into the syntactical world.

The usual approach to interpreting IST in a topos is to use the classifier object to define the logical connectives and the quantifiers, and then check that these definitions have all the expected properties. An alternative approach is to split this into two parts: 1) a classifier on a CCC with pullbacks induces a hyperdoctrine structure on it, and 2) the hyperdoctrine structure is exactly what is needed to interpret first-order logic with equality. This is how things are done in [Jac99], which then proceeds to show which extra structure is needed for interpreting polymorphism and dependent types... These are beautiful but hard theorems, whose details are not as widely-known as they should; what I felt was missing the most when I learned them was a way to make their intuitive content clearer. The tools in this paper can be a way to fill that gap — the next section sketches what that could mean.

21. Formalizing diagrams (in Type Theory)

We saw at sections 3 and 7 how to make each downcased “name” stand for both a “name” and its “meaning”. In our downcased categorical diagrams, each node and each arrow has a definite meaning as a categorical entity; so, let’s consider each node and arrow in a downcased diagram a diagrammatical name.

Note that diagrammatic names are positional — in the sense that entities with the same apparent names but at different positions of a diagram are allowed to have different meanings. That happened, for example, in Figure 9, where both δ^{∗}Q and δ^{∗}\overline{π}^{∗}(δ^{∗}Q) became \{ a, b || Qabb \} — abbreviated to a ‘Qabb’ above an ‘a, b’ — in the downcasing.

1The reader who doesn’t believe that this can be hard is urged to try to find the syntactical skeleton of the proof that in a topos every singleton map { · }_{A} : A → Ω^{A} is monic.

Now take any downcased diagram D, and draw two copies of it, one above another, like this:

\begin{matrix}D \\ ↓ \\ D^{−} \end{matrix}

Let’s take the positionality of names a step further. At the top diagram, D, all meanings are in the “real world”, and are non-proto categorical entities. At the lower diagram, D^{−}, in the “syntactical world”, each meaning is the proto-categorical entity corresponding to the non-proto entity above. For example, the meaning for an iso arrow ‘a, b ↔ b, a’ will be just a pair (⟨π′_{AB}, π_{AB}⟩, ⟨π′_{BA}, π_{BA}⟩) in the syntactical world, but in the real world it will be this plus the assurances that both composites are identities.

Suppose that we tag with a different number — in light gray, say — each node and each arrow in the diagram D → D^{−}; for example, our two copies of ‘a, b ↔ b, a’ may get tagged as ‘↔_{2099}’ in the real-world diagram, and as ‘↔_{99}’ in the syntactical world. With this we get numerical suffixes that we can use for the corresponding terms, and in the formalization of that diagram in a proof assistant the terms flip AB 99 and flip AB 2099 will, by convention, stand for the proto-iso and for the iso respectively.

Now imagine a diagram editor working in tandem with a text editor that not only edits a formalization of the diagram, but also controls a proof assistant. It shouldn’t be hard to make the occurrences of the term flip AB 99 be highlighted when the arrow ‘↔_{99}’ is selected, and vice-versa. Allowing 2D diagrammatic “names” in the editor, as, e.g., the squares of Section 9, as synonyms for some ascii terms, can be added later as a separate feature.

22. A Database of Categorical Theorems

We, the people who think mostly diagrammatically, would like to have a database of theorems from Category Theory, all presented in a diagrammatical form.

This database would include the theorems I know, the theorems I have half-forgotten, and lots of theorems that I never knew, that were added to the database by other people.

That database already exists, but in a non-ideal, not-very-diagrammatical form: it is the published literature on Category Theory. Each paper has its own notion of “obviousness”: when an author skips over details and claims that something is obvious, he supposes — in the spirit of section 10 — that the reader will be able to fill up the gaps.

I started to work on this subject because my notion of “obvious” seemed to be too different from the ones that I could find in the literature. The “archetypal models” being generalized are almost always mentioned in the papers, but only in passing, and after all the axioms having been laid down; all the formal arguments are made in the abstract notation only; and informal notations can only be presented when they are used to prove new nontrivial results, and when their formalization has been completed — but then they are not “informal” anymore, and they have been promoted to “internal languages”, “term calculi”, “proof nets”, “circuit diagrams”, etc ([JS91] is an early example of an informal notation made formal, with a nice discussion).

As each notion of “obvious” is backed by a method for proof search, it ought to be possible to formalize — even if roughly — how each such proofsearch method would work; and each different notion of what is “obvious” leads to a different way to present, and store, theorems. The same theorem T is remembered by a reader R_{1} as T_{1} and by a reader R_{2} as T_{2}; as the two readers reconstruct the missing details the theorems grow to T′_{1}, T′_{2}, T′′_{1}, T′′_{2}. If we could put these objects side to side we could clarify how these different kinds of reasonings work.

It is possible to reason coherently with infinitesimals. This became clear when Non-Standard Analysis was invented, and then even clearer when Synthetical Differential Geometry came up. One way to prove that a way of reasoning is coherent is to model it mathematically — and to show that the model has good properties. NSA and SDG “validate” reasonings with infinitesimals. Similarly, one way to validate reasonings based on internal diagrams, archetypal languages and informal notations is to formalize how these reasonings work — and to build bridges between them and the standard ways.

Diagrams like the ones in sections 14 and 15 can be interpreted formally: a diagram induces a dictionary, which induces trees, which then let us interpret each object and arrow from the diagram as a λ-term. A full set of rules for interpreting diagrams can be developed — including ways to deal with lists of exceptions and hints — and so it would be conceivable to have a database of categorical definitions and theorems in which the entries would appear as diagrams (plus their associated hints), but at the same time they would have precise meanings, understood by a proof assistant...

Note that diagrams are becoming more and more meaningful mathematically in the last decades. Compare these ideas with the discussion in [Krö07], p.83, where he quotes this from [ES52], p.xi:

The diagrams incorporate a large amount of information. Their use provides extensive savings in space and in mental effort. In the case of many theorems, the setting up of the correct diagram is the major part of the proof. We therefore urge that the reader stop at the end of each theorem and attempt to construct for himself the relevant diagram before examining the one which is given in the text. Once this is done, the subsequent demonstration can be followed more readily; in fact, the reader can usually supply it himself.

23. Epilogue

This is an atypical paper. It has no theorems, and it doesn’t prove any new mathematical truths — instead, we have shown several ways to represent constructions, and to structure proofs in several layers.

“Theorems” usually involve equalities between constructions, and hence they do not belong do the lowest layers; there are even ways — see Section 19 — to “project out” the parts of a theorem that involve equalities, and keep only the constructions... The result is a sort of a “syntactical skeleton” of the theorem.

Our “structuring” puts a situation with total information at the top, and below that, in different, parallel “legs”, we put different partial views. Theorems do not belong to the structuring, either.

At some point we will have “meta-theorems” about properties of this structuring. But finding these meta-theorems should not be top priority right now: these meta-theorems will use known theorems, and at this point it is more important to put more known theorems in this format.

The above may look too vague, too philosophical (in contraposition to “mathematical”), too abstract. Category Theory used to be called “abstract nonsense”; the ideas of this paper, then, especially the more technical sections, 13 to 20, could look like “meta-abstract nonsense”... However, we are not pointing only towards the more abstract: we are showing ways — and reasons — to do the general in parallel with the particular, and to arrange the results of doing mathematics like that in forms that are better for reconstruction and transmission.

Our structuring allows the controlled use of informal notations. Several different informal notations can be used in parallel at the same time. This can be useful for comparing different people’s notations, and for changing details on a notation and letting it evolve over time. The database of categorical knowledge proposed in the last section does not need a unified notation, and one of its functions could be to serve as a dictionary between notations — and as a way to make parts of the existing literature more accessible.

References

[Awo06] S. Awodey. Category Theory. Oxford University Press, 2006.

[Bel88] J. L. Bell. Toposes and Local Set Theories. Number 14 in Oxford Logic Guides. Oxford University Press, 1988.

[Bel08] J. L. Bell. A Primer of Infinitesimal Analysis. Cambridge, 2008.

[BJP10] J. P. Bernardy, P. Jansson, and R. Paterson. Parametricity and dependent types. International Conference on Functional Programming, 2010.

        http://www.cse.chalmers.se/~bernardy/ParDep/pardep.pdf.

[ES52] S. Eilenberg and N. Steenrod. Foundations of algebraic topology. Princeton, 1952.

32 Eduardo Ochs

[Fre76] P. Freyd. Properties invariant within equivalence types of categories. In A. Heller and M. Tierney, editors, Algebra, Topology and Category Theory: A Collection of Papers in Honour of Samuel Eilenberg, pages 55–61. Academic Press, 1976.

[FS90] P. Freyd and A. Scedrov. Categories, Allegories. North-Holland, 1990.

[Geu93] H. Geuvers. Logics and Type Systems. PhD thesis, University of Nijmegen, 1993.

[Jac99] B. Jacobs. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North-Holland, Elsevier, 1999.

[JS91] A. Joyal and R. Street. The geometry of tensor calculus i. Advances in Mathematics, 88:55–112, 1991.

[Koc77] A. Kock. A simple axiomatics for differentiation. Mathematica Scandinav-

        ica, 40(2):183–193, 1977. http://www.mscand.dk/article.php?id=2356.

[Koc80] A. Kock. Synthetic Differential Geometry. Cambridge, 1980.

        http://home.imf.au.dk/kock/sdg99.pdf.

[Krö07] R. Krömer. Tool and Object: A History and Philosophy of Category The-

ory. Birkhäuser, 2007.

[Law69] W. Lawvere. Adjointness in foundations. Dialectica, 23:281–296, 1969.

[Law70] W. Lawvere. Equality in hyperdoctrines and comprehension schema as an adjoint functor. Proceedings of the American Mathematical Society Symposium on Pure Mathematics XVII, 999:1–14, 1970.

[LS86] J. Lambek and P. Scott. Introduction to Higher-Order Categorical Logic. Cambridge, 1986.

[LS97] W. Lawvere and S. Schanuel. Conceptual Mathematics: A first introduction to categories. Cambridge, 1997.

[MR91] I. Moerdijk and G. E. Reyes. Models for Smooth Infinitesimal Analysis. Springer, 1991.

[Och10] E. Ochs. Downcasing types. Slides for a presentation at the UniLog’2010.

        http://angg.twu.net/math-b.html#unilog-2010, 2010.

[See83] R. A. G. Seely. Hyperdoctrines, natural deduction, and the beck condition. Zeitschrift f. math. Logik und Grundlagen d. Math., 29:505–542, 1983.

[Tay86] P. Taylor. Recursive Domains, Indexed Category Theory and Polymorphism. PhD thesis, Cambridge, 1986.

[Wad89] P. Wadler. Theorems for free! In Proc. FPCA’89, pages 347–359. ACM, 1989.

Eduardo Ochs LLaRC – Laboratório de Lógica e Representação do Conhecimento Depto. de Física e Matemática, Pólo Universitário de Rio das Ostras Universidade Federal Fluminense, Rio das ostras, RJ, Brazil

e-mail: eduardoochs@gmail.com

Submitted: November 1, 2010. Revised: April 27, 2013.