Downcasing Types Eduardo Ochs PURO/UFF, LLaRC eduardoochs@gmail.com http://angg.twu.net/

I first presented this, in an incomplete form, at the UniLog’2010 (Cascais, Portugal, april 2010)... The current version (see the footer for the date) has many more slides, and I am still adding more.

What you are reading is a work in progress. Page 8 contains an outline, and explains how close to being finished each section is.

For the latest version look at:

http://angg.twu.net/math-b.html

or go straight to:

http://angg.twu.net/LATEX/2010unilog-current.dvi
http://angg.twu.net/LATEX/2010unilog-current.pdf

I find navigation a bit better in the dvi, with xdvik. Comments are very welcome!

Index of the slides:

LLaRC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 Outsiders . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6 Abstract . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 The internal diagram of a map . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 The internal diagram of a map (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .10 Physicists’ notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

Introduction: Curry-Howard . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 Erasings as projections . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 Generalization is a kind of lifting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 Where we are heading . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 Why topos theory (is important) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 Lifting basic topos theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 Downcasing diagrams . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 Downcasing diagrams (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .19 Can we make Topos Theory more accessible? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 From trees to dictionaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 Ambiguities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 Ambiguities (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 Ambiguities (3) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 More on the ‘wd’ symbol: the syntactical world . . . . . . . . . . . . . . . . . . . . . . . . . . . .25 The syntactical world: proto-things . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .26 Downcasing functors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Adjunctions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Cheap and expensive adjunctions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Cheap and expensive adjunctions (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Programming with long names . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31

The Yoneda Lemma: The Yoneda Lemma . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 The Yoneda Lemma (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33

Monads: Monads . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 From monads to adjunctions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 The Kleisli category of a monad . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 The Kleisli adjunction of a monad . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 The Eilenberg-Moore category of a monad . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .38 The comparison theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Beck’s lemma . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 Beck’s lemma (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .41 Monads and cohomology . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42

Cartesian Closed Categories: Cartesian Closed Categories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Cheap and expensive toposes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 λ-calculus in a CCC: an example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 λ-calculus in a CCC: an example (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 The product property . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 Product diagrams . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 Product diagrams (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 Products as adjunctions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 Exponentials . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 Exponentials (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 Morphisms as sequents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53

Hyperdoctrines: Hyperdoctrines . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .54 Subobjects . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 Subobjects (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 Subobjects (3) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 Subobjects (4) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 Cartesianness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 Cartesianness (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .60 Pullbacks are cartesian . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 Cleavages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 Cleavages (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .63 Cleavage induces change-of-base . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 Adjoints to change-of-base . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .65 Semantics for ND in Pred(Set): quantifiers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 Rules for the quantifiers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 Rules for the quantifiers (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68 Rules for equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 Adjoints to change-of-base: quantifiers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .70 Adjoints to change-of-base: equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71 Adjoints to change-of-base: generic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 Adjoints to change-of-base: candidates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 Preservation of ‘and’ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 Preservation of ‘and’ (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .75 Preservation of ‘true’ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76 Preservation of ‘implies’ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 Beck-Chevalley for the left adjoint . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .78 Beck-Chevalley for the right adjoint . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 Frobenius . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80 Cheap hyperdoctrines . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81 Pimp implies Frob . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .82 Pimp implies Frob (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83 Pimp implies Frob (3) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 BCCL implies BCCR . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .85 Lemmas about equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86 λ-calculus in a hyperdoctrine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87 Propositional calculus in a hyperdoctrine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88 Interpreting ‘∀I’ in a hyperdoctrine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89 Interpreting ‘∀E’ in a hyperdoctrine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90 Interpreting ‘∃I’ in a hyperdoctrine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91 Interpreting ‘∃E’ in a hyperdoctrine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92 Equality types: Hofmann 1995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93

Models for polymorphism:

PL categories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94 PL categories (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95

Typing proto-categories: Uppercasing names . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .96 Uppercasing names (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 Uppercasing names (3) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98 Uppercasing names (4) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99 Currying long names . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100 Typing proto-categories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101

Etc: Introduction to Heyting Algebras . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .102 Introduction to Lawvere-Tierney Topologies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103 Introduction to Lawvere-Tierney Topologies (2) . . . . . . . . . . . . . . . . . . . . . . . . . . 104 Map of the world . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .105 There are no (new) theorems in these slides . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106 Typing proto-adjunctions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107 Typing proto-CCCs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108 Typing proto-fibrations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .109 LLaRC LLaRC = Laboratório de Lógica e Representação do Conhecimento = Laboratory of Logic and Representation of Knowledge at PURO/UFF = Pólo Universitário de Rio das Ostras/ Universidade Federal Fluminense

Rio das Ostras is city in the countryside of the state of Rio de Janeiro, Brazil. RO is ∼180Km away from Rio de Janeiro and ∼150Km away from Niterói, which is where the main campi of UFF are situated.

The LLaRC is a research laboratory that, despite our efforts in the last two years, 8-(, still doesn’t have a physical room, (the PURO has been facing severe space problems), neither a decent internet connection (we still have only about 3KB/s per machine at PURO), and from nov/2009 to mar/2010 none of the printers at PURO had toner...

We have decided that in order to give some kind of official existence to our current research we would temporarily lower the bar for what we would “publish”, and work-in-progress versions of seminar notes, like these, could be put in the LLaRC home page.

(We do not get brownie points for these).

This page should be removed for the final version, I guess... But the Silent Majority just repealed in the last departmental meeting an informal agreement that in my opinion was the main tool that kept everyone working together and in good spirits in spite of all difficulties... Anyway: the details don’t fit here, I am saddened and pissed off, and this page will be part of the first official release of these notes. Cheers.

Outsiders This is Category Theory (from here on: “CT”) done by an outsider, in a place where no one else is doing research in CT, or even using CT in non-trivial ways...

If the ideas in these notes were perfect AND crystal-clear AND had the best impact possible then this is more or less what would happen:

• Local people close to me (non-CT-ists) would become able to read CT books and articles;

• CT-ists (would...) find the method described here trivial, and would start to circulate notes describing the archetypical models behind several constructions that I’ve been struggling to understand (sheafification, classifying toposes, *- autonomous categories, differential categories, Kan extensions, the Grothendieck construction on a fibration, schemes, parametric models, DTT on LCCCs, etc); I get hold of their notes and understand everything;

• Type theorists find out the right type systems for the syntactical world, the real world and the projection; they also find classes of type equations (for the “hints”) that can be extracted from the diagrams and solved automatically;

• Proof-assistants people come up with very good ways to formalize CT proofs by doing the syntactical part first, then completing the details;

• Parametricity people grok immediately everything here, and we work together on the missing meta-theorems;

• Philolophical Logic people would help me to fit these ideas in a grander scheme of things: synthetical vs. analytical reasoning, external diagrams vs. internal diagrams, the roles of intuition, of archetypal models and generalization;

• Diagrammatic logic people find out how to enrich my categorical diagrams with some extra hints, so that diagrams like these, when stored in a computer with the those extra hints would automatically generate the derivation trees — and the code for proof-assistants.

Abstract I presented (a much shorter version of) this at UniLog’2010, with this abstract:

When we represent a category C in a type system it becomes a 7uple, whose first four components — class of objects, Hom, id, composition — are “structure”; the other three components are “properties”, and only these last three involve equalities of morphisms.

We can define a projection that keeps the “structure” and drops the “properties” part; it takes a category and returns a “proto-category”, and it also acts on functors, isos, adjunctions, proofs, etc, producing proto-functors, proto-proofs, and so on.

We say that this projection goes from the “real world” to the “syntactical world”; and that it takes a “real proof”, P, of some categorical fact, and returns its “syntactical skeleton”, P^{−}. This P^{−} is especially amenable to diagrammatic representations, because it has only the constructions from the original P — the diagram chasings have been dropped.

We will show how to “lift” the proto-proofs of the Yoneda Lemma and of some facts about monads and about hyperdoctrines from the syntactical world to the real world. Also, we will show how each arrow in our diagrams is a term in a precise diagrammatic language, and how these diagrams can be read out as definitions. The “downcased” diagrams for hyperdoctrines, in particular, look as diagrams about Set (the archetypical hyperdoctrine), yet they state the definition of an arbitrary hyperdoctrine, plus (proto-)theorems.

I am not totally sure that I fulfill all the promises of the abstract in the current version of these slides. (Actually I submitted a longer version of the abstract, where I promised even more — but what got published was the short version above).

In particular, the section on hyperdoctrines should be much clearer and should contain at least the full translation and the full (proto-)proof of lemma in page 9 in [Lawvere70] (“all constructions for b = b′ ∧ Qbb′ are isomorphic”) and for “we only need to require adjoints to π^{∗} and Δ^{∗}, plus a few cases of Frobenius and Beck-Chevalley” in [Seely83] (page?)... Also, my exposition of how to interpret ND in a hyperdoctrine is quite incomplete — the method for interpreting some subtrees of an ND derivation as vertical morphisms (and then glueing the interpretations) requires lots of details that I’m not going into...

But these slides are not intended to be totally self-contained — they are meant to help people to read the original papers! 8-)

Outline

• Introduction

• The Yoneda Lemma

• Monads

• Cartesian Closed Categories

• Hyperdoctrines

• Models for polymorphism

• Typing (proto-)fibrations

• Etc

The introduction is quite good as it is now — no urgent changes needed.

The section about the Yoneda Lemma needs more details — it shows just the first ideas, and doesn’t show the implementation in Coq.

The section about monads is a curiosity, and it is there mostly to show the power of the method. It is not especially interesting to type theorists.

The section about CCCs is quite good as it is now — no urgent changes needed.

The section about hyperdoctrines is huge, but it still needs a lot of work — it is the main basic application (and the main testbed) for Downcasing Types. I need to make the translation between hyperdoctrine operations and first-order logic very clear (for many reasons), and in comparison with how complete and clear I need that section to be it is still vary incomplete, and very messy.

The section on “models for polymorphism” is in a very preliminary stage. It should show how to translate (or: how to “understand”) at least four texts on models for polymorphic λ-calculus: Seely’s “Categorical Semantics for Higher Order Polymorphic λ-Calculus”, Reynolds’s “Polymorphism is not Set-Theoretic”, Pitts’s “Polymorphism is Set-Theoretic, constructively”, and chapter 8 of Jacobs’s book, “Categorical Logic and Type Theory”.

The section on “typing proto-fibrations” is in a very preliminary stage too.

The section “Etc” is currently just a handful of slides pointing to other applications (works in progress).

The bilbiography section is missing.

Also, several important ideas for the method of downcasings came to me while I was struggling to understand and translate two papers: Blute, Cockett and Seely’s “Differential Categories” (2005) and Kock’s “A simple axiomatics for differentiation” (1977). My translations for parts of those papers will be included in a later version.

The internal diagram of a map

The idea of internal diagram of a map is crucial for understanding the method of downcasing types. (It took me several years to identify it (!), and to find a few scattered references to it in the literature — it is not mention often...)

In our early school years we used to see a function like

\begin{aligned}\sqrt{·} & : & ℕ & → & ℝ \\ & & n & ↦ & \sqrt{n} \end{aligned}

as the “internal view” below, in “standard notation” — only we used to draw it with ‘→’s in place of the ‘↦’s.

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

The notation n ↦ \sqrt{n} is “generic enough” to let us reconstruct the definition of the function from it (except maybe for the codomain; but let’s not worry about that). Note that from ‘n ↦ \sqrt{n}’ we can infer the “syntactical action” of the function: it puts the “name” of its argument under a ‘√ ’. We can define syntactical actions in L^{A}TEX:

      \def\myf#1{\sqrt{#1}}
      \def\myg#1{(#1)\sqrt{#1} - 42}

The internal diagram of a map (2)

Not only ‘n ↦ \sqrt{n}’ is “generic enough” (to let us reconstruct \sqrt{·} from it) but also ‘2 ↦ \sqrt{2}’ can be “generic enough” in some contexts... We can recognize it as the function that takes 2 to \sqrt{2}, generalized “to any value of 2”.

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

We can think of ‘2 ↦ \sqrt{2}’ as being the archetypal case that we want to generalize.

We can also think of ‘n ↦ \sqrt{n}’ as being an archetypical case (in a certain context, of course) for a function from ℕ to ℝ; then a further generalization would be to move to a (possibly arbitrary) function from ℕ to ℝ, that we would downcase as ‘n ↦ r’...

Physicists’ notation We can also think in physicists’ notation... If we have a function whose graph is given by the equation y = f(x), then given x_{0}, x_{1}, …, x_{n}, x′, x′′, we have default definitions for y_{0}, y_{1}, …, y_{n}, y′, y′′... we define y_{0} = x_{0}, y′ = f(x′), etc. The “real action” of the function is x ↦ f(x), but its “syntactical action” on names like x_{0}, x_{1}, …, x_{n}, x′, x′′ is to change ‘x’s to ‘y’s, but keep the “decorations”.

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

I would downcase this function f as x ↦ y. Note that the “space of ‘x’s”, i.e., the set where x_{0}, … live, is ℝ, and the “space of ‘y’s” is ℝ too, which is a bit funny —

If we start with sets A = {a_{1}, a_{2}, a_{3}} and B = {b_{1}, b_{2}, b_{3}, b_{4}} then it feels much more natural to downcase a function g : A → B as ‘a ↦ b’...

Sometimes we think of the two ‘ℝ’s in the f : ℝ → ℝ above as being “different copies” of ℝ — maybe the horizontal and the vertical axes in ℝ^{2}, thought as subsets, or submanifolds, of ℝ^{2}— but I don’t recall ever having seen the details fully worked out... (To do: check Spivak’s books)

I have never seen any thorough discussion of physicists’ notation — how to parse it, how to formalize it, what are the usual defaults, how it has changed through history, etc... Anyone has any pointers, please?...

Curry-Howard

\begin{aligned}{[P ∧ Q]^{1} \atop P} & \begin{aligned}{[P ∧ Q]^{1} \atop Q} & Q [figure]R \\ & R \end{aligned} \\ & P ∧ R \end{aligned} ; P ∧ Q [figure]P ∧ R ; 1  \begin{matrix}{[p : A × B]^{1} \atop πp : A} π & \begin{matrix}{[p : A × B]^{1} \atop π′p : B} π′ & f : B → C \\ f(π′p) : C \end{matrix} app \\ ⟨πp, f(π′p)⟩ : A × C \end{matrix} ; ⟨, ⟩ ; λp:(A × B).⟨πp, f(π′p)⟩ : 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 : A × B]^{1} \atop πp : A} π & \begin{matrix}{[p : A × B]^{1} \atop π′p : B} π′ & f : B → C \\ f(π′p) : C \end{matrix} app \\ ⟨πp, f(π′p)⟩ : A × C \end{matrix} ; ⟨, ⟩ ; λp:(A × B).⟨πp, f(π′p)⟩ : A × B → A × C ; λ; 1

The Curry-Howard isomorphism (in its simplest form — there are several) establishes a correspondence between trees in (propositional) Natural Deduction and trees in (simply-typed) λ-calculus.

λ-calculus is the language for expressing constructions. The terms in the bottom of λ-calculus trees get bigger and bigger, so people usually don’t draw λ-calculus trees — they work “algebraically”, just with term at the bottom. A λ-calculus tree can be reconstructed from its bottom term. Humans like full λ-calculus trees, though, because the trees explain the types of all subterms.

The tree at the bottom left above describes the “intuitive meaning” behind the λ-calculus tree.

Erasings as projections

[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}]

The “downcased tree” at the bottom right above is an “intuitive view” of the (λ-calculus) construction. How do we formalize an “intuitive construction” like that? Answer: erasings act like projections. We add the missing information by lifting and then we erase some things.

Here’s how we read the “downcased tree” aloud. “If we have a meaning for ‘b’ and a meaning for ‘b ↦ c’ we have a natural meaning for ‘c’ ”... Linguistic tricks:

• long names: ‘b ↦ c’ is a name

• no syntactical distinction between variables and non-atomic terms • ‘b ↦ c’ to ‘B → C’: the types can be recovered by uppercasing • each bar is a definition

• indefinite articles: “if I have a ‘b’ and a ‘b ↦ c’ I have a ‘c’˙’’...

Generalization is a kind of lifting To generalize is the opposite of to specialize, and specialization is obviously a projection.

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

2^{99+1} − 2^{99} = 2^{99} holds “for any value of 99”... We are going to see how to do something like this for categories (esp. hyperdoctrines, ≈ toposes), using “dictionary tricks”.

How generalizations work? How do we think? What are the possible/usual roles of diagrams? Which kinds of reasonings are closer to intuition? I discovered something quite surprising at UniLog’2010... (at the talks of Danielle Macbeth and Juan Luis Gastaldi) it is time to look for further conceptual tools in Kant and Frege!

Where we are heading Fact: every “pure” term that deserves the name

(A, B) ↦ (a, b ↦ b, a)

is the (polymorphic) “flip” function.

More precisely: we have a procedure, T ↦ P_{T}, that produces for each “pure” type T (a term is pure when it has no constants besides the sorts) a property P_{T} that every pure term t : T obeys.

This is called parametricity. (A good introductory reference: Phil Wadler’s “Theorems for Free”, 1988).

All the categorical constructions that I will show are “pure”, and it must be possible to use tools from parametricity to prove meta-theorems about properties of pure constructions.

However, these tools (from parametricity) are hard to understand, especially if we are outside the Category Theory/λ-calculus communities, without much acess to the “oral culture” of these areas.

Why topos theory (is important) Models:

• Sheaves form (Grothendieck) toposes

• Every Set^{U} is a topos (← Non-Standard Analysis)

• There are toposes with nilpotent infinitesimals (← SDG)

• There are toposes with polymorphism and parametricity

• There are toposes in which everything is constructive/computable

By realizing that a certain category C is (or can be enlarged to) a topos we immediately know a lot about it... We can carry a lot of our knowledge about Set (constructions, properties) to C, and important constructions in C may turn out to correspond to something simple and well-known in Set...

Topos theory (and Categorical Semantics in general) is about translating knowledge and recycling theorems.

And this point is becoming more and more important: most proof assistants are based on (intuitionistic) type theories whose models do not fit well in ZFC (Reynolds 1984: “Polymorphism is not Set-Theoretic”) and learning Topos Theory is (perhaps) one of the best ways to make all this make sense...

Lifting basic topos theory Here’s a conjecture, whose technical details should not be deep: it should be possible to develop and prove almost all of the basic theory of toposes, modalities, sheaves and geometrical morphisms in the archetypical cases (i.e., in ‘Set^{𝔻}’s), where everything is very concrete, and then lift all the constructions and proofs to the general case.

Downcasing diagrams

abstract/generic:

[figure: f^{∗}g^{∗}P; g^{∗}P; f^{∗}g^{∗}P; (f; g)^{∗}P; g^{∗}P; P; (f; g)^{∗}P; P; A; B; f; B; C; g; A; C; f;g]

archetypal (long form):

[figure: { a || P (f(g(a)) }; { b || P (g(b)) }; { a || P (f(g(a)) }; { a || P (f(g(a)) }; { b || P (g(b)) }; { c || P (c) }; { a || P (f(g(a)) }; { c || P (c) }; A; B; f; B; C; g; A; C; f;g]

[figure]

archetypal (long form):

[figure: { a || P (f(g(a)) }; { b || P (g(b)) }; { a || P (f(g(a)) }; { a || P (f(g(a)) }; { b || P (g(b)) }; { c || P (c) }; { a || P (f(g(a)) }; { c || P (c) }; A; B; f; B; C; g; A; C; f;g]

archetypal (shorthand):

[figure: A; B; f; { a || P }; { b || P }; { a || P }; { a || P }; { b || P }; { c || P }; { a || P }; { c || P }; B; C; g; A; C; f;g]

[figure] abstract/generic:

[figure: f^{∗}g^{∗}P; g^{∗}P; f^{∗}g^{∗}P; (f; g)^{∗}P; g^{∗}P; P; (f; g)^{∗}P; P; A; B; f; B; C; g; A; C; f;g]

downcased (long form):

[figure: a||P fga; b||P gb; a||P fga; a||P fga; b||P gb; c||P c; a||P fga; c||P c; a; b; b:=f(a); b; c; c:=g(b); a; c; c:=f(g(a))]

[figure]

[figure]

downcased (long form):

[figure: a||P fga; b||P gb; a||P fga; a||P fga; b||P gb; c||P c; a||P fga; c||P c; a; b; b:=f(a); b; c; c:=g(b); a; c; c:=f(g(a))]

downcased (shorthand):

[figure: P; P; P; P; P; P; P; P; a; b; b; c; a; c]

[figure]

The ideas from the method of “downcasing types” are often used in disguise... The way of structuring diagrams (both for the generic case, in abstract notation, and for the archetypal case — plus its shorthands) comes from what has to be done to make the corresponding diagrams make sense in downcased notation. The dictionary tricks — which include making ‘P ↦ g^{∗}P ’ stand for a functor, and putting corresponding diagrams side to side — also come from downcased notation. (Also the ideas like lifting, etc.)

Downcasing diagrams (2)

abstract/generic:

[figure: f^{∗}g^{∗}P; g^{∗}P; f^{∗}g^{∗}P; (f; g)^{∗}P; g^{∗}P; P; (f; g)^{∗}P; P; A; B; f; B; C; g; A; C; f;g]

archetypal (long form):

[figure: { a || P (f(g(a)) }; { b || P (g(b)) }; { a || P (f(g(a)) }; { a || P (f(g(a)) }; { b || P (g(b)) }; { c || P (c) }; { a || P (f(g(a)) }; { c || P (c) }; A; B; f; B; C; g; A; C; f;g]

[figure]

Also, the abstract/generic case often makes distinctions that disappear when we look at the archetypical case... For example, the archetypal fibration, CanSub(Set), is split, and so f^{∗}g^{∗}{ c || P } = (f; g)^{∗}{ c || P }; in the generic case there’s a canonical iso f^{∗}g^{∗}P ↔ (f; g)^{∗}P, but it doesn’t need to be the identity.

If we are trying to model categorically a certain archetypical case (by generalizing it “in the right way”) then certain equalities in the archetypical case should become at least canonical isos in the generic case... in CCCs and hyperdoctrines “one half” (i.e., one direction) of these canonical isos will comes from natural constructions; what we will do is to impose that the these natural constructions should be invertible.

As we will work with (proto-)structure instead of with properties we will require “proto-inverses” instead of requiring invertibility.

Can we make Topos Theory more accessible? Can we make Topos Theory more accessible using these techniques? At the moment, unfortunately, not really — the rules for the \underline{classifier object} are problematic. However, one of the most interesting ideas in Topos Theory is how we can interpret first-order logic inside a topos — and this can also be done in hyperdoctrines.

Hyperdoctrines came a few years before toposes. Hyperdoctrines are exactly the categories where we can interpret (intuitionistic, typed) first-order logic. The definition of a hyperdoctrine seems much more convoluted that the definition of a topos, but that’s because the presence of a classifier object simplifies everything — if we add a classifier rule to the hyperdoctrine rules we see that many of the rules that we had before can be discarded — they become redundant.

From trees to dictionaries

[figure: \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} app \\ & 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} app \\ & a, c \end{aligned} ; ⟨, ⟩ ; a, b ↦ a, c ; λ; 1; \begin{aligned}⟨⟨a⟩⟩ & := & π⟨⟨a, b⟩⟩ \\ ⟨⟨b⟩⟩ & := & π′⟨⟨a, b⟩⟩ \\ ⟨⟨c⟩⟩ & := & ⟨⟨b ↦ c⟩⟩(⟨⟨b⟩⟩) \\ ⟨⟨a, c⟩⟩ & := & ⟨⟨⟨a⟩⟩, ⟨⟨c⟩⟩⟩ \\ ⟨⟨a, b ↦ a, c⟩⟩ & := & λ⟨⟨a, b⟩⟩:(A × B).⟨⟨a, c⟩⟩ \end{aligned}; \begin{aligned}⟨⟨a⟩⟩ & := & π⟨⟨a, b⟩⟩ \\ ⟨⟨b⟩⟩ & := & π′⟨⟨a, b⟩⟩ \\ ⟨⟨c⟩⟩ & := & ⟨⟨b ↦ c⟩⟩(⟨⟨b⟩⟩) \\ ⟨⟨a, c⟩⟩ & := & ⟨⟨⟨a⟩⟩, ⟨⟨c⟩⟩⟩ \\ ⟨⟨a, b ↦ a, c⟩⟩ & := & λ⟨⟨a, b⟩⟩:(A × B).⟨⟨a, c⟩⟩ \end{aligned}; \begin{matrix}{[p]^{1} \atop πp} π & \begin{matrix}{[p]^{1} \atop π′p} π′ & f \\ f(π′p) \end{matrix} app \\ ⟨πp, f(π′p)⟩ \end{matrix} ; ⟨, ⟩ ; λp:(A × B).⟨πp, f(π′p)⟩ ; λ; 1; \begin{aligned}⟨⟨a, b⟩⟩ & ≡ & p \\ ⟨⟨b ↦ c⟩⟩ & ≡ & f \end{aligned}; \begin{matrix}{[p]^{1} \atop πp} π & \begin{matrix}{[p]^{1} \atop π′p} π′ & f \\ f(π′p) \end{matrix} app \\ ⟨πp, f(π′p)⟩ \end{matrix} ; ⟨, ⟩ ; λp:(A × B).⟨πp, f(π′p)⟩ ; λ; 1]

Each bar of a downcased tree is a definition. If we list all these definitions together we get a “dictionary” that almost gives us back the λ-tree... we need just a few more hints — the standard names of the variables and the constants.

Ambiguities

Liftings are not usually unique... What should be the type of ‘a’? A or A′? To lift we usually need “hints”. The downcasing that starts with “a, a” below is (apparently?) valid, but ambiguous. I am not going to define what a good downcasing is.

[figure: \begin{matrix}{a, a′ \atop a′} & {a, a′ \atop a} \\ a′, a \end{matrix}; \begin{matrix}{A × A′ \atop A′} & {A × A′ \atop A} \\ A′ × A \end{matrix}; \begin{matrix}{a, a′ \atop a′} & {a, a′ \atop a} \\ a′, a \end{matrix}; \begin{matrix}{A × A \atop A} & {A × A \atop A} \\ A × A \end{matrix}; \begin{matrix}{A × A \atop A} & {A × A \atop A} \\ A × A \end{matrix}; \begin{matrix}{a, a \atop a} & {a, a \atop a} \\ a, a \end{matrix}]

Ambiguities (2)

Composition is not well-behaved syntactically. One solution (? — or workaround) is to have a rule ‘ren’ that renames objects (i.e., create aliases)...

\begin{matrix}\begin{matrix}π : A × A → A & f : A → B \\ π; f : A × A → B \end{matrix} & \begin{matrix}a, a′ ↦ a & a ↦ b \\ a, a′ ↦ b \end{matrix} \\ \begin{matrix}π′ : A × A → A & f : A → B \\ π′; f : A × A → B \end{matrix} & \begin{matrix}a, a′ ↦ a′ & a ↦ b \\ a, a′ ↦ b′ \end{matrix} & \begin{matrix}a, a′ ↦ a′ & {a ↦ b \atop a′ ↦ b′} ren \\ a, a′ ↦ b′ \end{matrix} \end{matrix}

Ambiguities (3) Composition is associative, and that’s the reason why we can write f; g; h.

[figure: A; B; f; B; C; g; C; D; h; A; C; f;g; B; D; g;h]

Twisting this idea a bit: we write f; g; h to indicate that (f; g); h = f; (g; h). We have two different “natural constructions” for things that “deserve the name” f; g; h. Downcasing them, we get:

[figure: \begin{matrix}\begin{matrix}a ↦ b & b ↦ c \\ a ↦ c \end{matrix} ; & c ↦ d \\ a ↦ d \end{matrix} ;; \begin{aligned}a ↦ b & \begin{matrix}b ↦ c & c ↦ d \\ b ↦ d \end{matrix} ; \\ & a ↦ d \end{aligned} ; ;; \begin{matrix}\begin{matrix}a ↦ b & b ↦ c \\ a ↦ c \end{matrix} ; & c ↦ d \\ a ↦ d \end{matrix} ;; \begin{aligned}a ↦ b & b ↦ c & c ↦ d \\ & a ↦ d \end{aligned}; \begin{aligned}a ↦ b & \begin{matrix}b ↦ c & c ↦ d \\ b ↦ d \end{matrix} ; \\ & a ↦ d \end{aligned} ; ;; \begin{aligned}a ↦ b & b ↦ c & c ↦ d \\ & a ↦ d \end{aligned}]

I used to express that the two “obvious” natural constructions for (a ↦ d) from (a ↦ b), (b → c), (c → d) give the same result by:

wd \left[{a ↦ b b ↦ c c ↦ d \atop a ↦ d}\right]

The entry for that ⟨⟨wd[…]⟩⟩ in the dictionary would have to say which “obvious constructions” were involved.

More on the ‘wd’ symbol: the syntactical world A category C is a tuple:

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

Where the first four components are “structure” and the last three are “properties” — equations. The last three are ‘wd’ things.

I used to carry all the ‘wd’s around, as if they were very very important. I don’t anymore. It turns out that we can define a projection

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

psyn

that drops the equations. This works for isos, functors, NTs, adjunctions, monads, etc, also. We can do a “projected version” of Category Theory and then lift the results back to the “Real World” (not automatically — many steps have to be done by hand — but whatever). I call the “projected version” the “Syntactical World”. The projection keeps the “syntactical part” — the “structure” — and drops the “equational part” — the “properties”.

The “projection on the syntactical world”, psyn, is the main operation that we are studying here. Warning: it will often be used implicitly! Warning 2: psyn can be defined in many different, slightly incompatible ways, so before studying its meta-properties we need to collect enough non-trivial examples of it at work...

Each projection of a non-trivial categorical theorem, T into the syntactical world, T^{−} := psyn(T), gives a non-trivial example of a lifting: T^{−} lifts to T.

The syntactical world: proto-things I use the prefix “proto” to refer to the projected structures. A proto-category is a 4-uple (C_{0}, Hom_{C}, id_{C}, ∘_{C}). A proto-functor F : A → B is a 2-uple: (F_{0}, F_{1}) (an “action on objects” and an “action on morphisms” — the equational components, respcomp and respids, have been dropped).

Sometimes there are several possible “design choices” for a proto-structure... I will just say which definitions of proto-things work best. (No time for the full rationale today!)

A proto-inverse for a morphism f : A → B is a just a morphism f^{−1} : B → A. Note that we don’t have the conditions f; f^{−1} = id_{A} and f^{−1}; f = id_{B}, so the name f^{−1} may be a bit misleading. A proto-iso is a pair (f, f^{−1}), where f^{−1} is a proto-inverse for f.

A proto-natural transformation (“proto-NT”) T : F → G is just an operation A ↦ (F A →^{T_{A}} GA) (we drop the “square condition” that says that for each f : A → B the “obvious square” must commute).

A proto-inverse for a (proto-)natural transformation T : F → G is just a (proto-)natural transformation T^{−1} : G → F — for each object A the morphisms T A and T^{−1}A are the two directions of a proto-iso. A proto-natural isomorphism is a proto-NT plus a proto-inverse for it.

What are proto-products, proto-exponentials, proto-fibrations...?

Downcasing functors

Fix a set A. Let (A×) : Set → Set denote the functor that takes each set B to A × B.

“\underline{The}” functor? In some contexts the action on morphisms, (A×)_{1}, is “obvious” once the action on objects, (A×)_{0}, is given. How?

[figure: b; a, b; b; c; a, b; a, c; c; a, c; B; A × B; A×; C; A × C; A×; B; C; f; A × B; A × C; \begin{matrix}(A×)f := \\ λp:A×B.⟨πp,f(π′p)⟩ \end{matrix}]

By lifting:

[figure: {b ↦ c \atop a, b ↦ a, c}; \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]

(a double bar is like a folded accordion)

Adjunctions

If L and R are functors going in opposite directions between two categories, say,

B [figure: L; R] A

then a proto-adjunction, L ⊣ R, is an 8-uple,

(A, B, L, R, ♭, ♯, η, ϵ)

that we draw as:

[figure: LRB; B; ε_{B}; A; RLA; η_{A}; LA; A; LA; B; g^{♭}; LA; B; f; A; RB; g; A; RB; f^{♯}; B; RB; B; A; L; B; A; R]

There is a lot of redundancy in this definition... Most operations can be reconstructed from the others.

Our archetypal adjunction will be this one: (not the usual F ⊣ U!)

[figure: (B→C)×C; C; _{ev_{BC}}; A; B→(A×B); η_{A}; A×B; A; A×B; C; uncur g; A×B; C; f; A; B→C; g; A; B→C; cur f; C; B→C; Set; Set; ×B; Set; Set; B→]

Cheap and expensive adjunctions

In the supermarket you can buy DeLuxe adjunctions, that are expensive but come with all the bells and whistles, and you can buy the cheap, minimal, economy models, that come in kit form, and (apparently) do much less...

There are theorems that take cheap adjunctions and produce expensive adjunctions from them — for free.

In the Real World cheap and expensive adjunctions are equivalent: if you do

[figure: (A, B, L, R, ♭, ♯, η, ϵ); (A, B, L, R_{0}, ♯, ϵ); (A, B, L, R, ♭, ♯, η, ϵ); (A, B, L_{0}, R, ♭, η ); (A, B, L, R_{0}, ♯, ϵ); (A, B, L, R, ♭, ♯, η, ϵ); (A, B, L_{0}, R, ♭, η ); (A, B, L, R, ♭, ♯, η, ϵ)]

you get the original expensive adjunction back. In the Syntactical World you may get something different, but that doesn’t matter.

Cheap and expensive adjunctions (2) An “expensive” proto-adjunction L ⊣ R is an 8-uple:

(A, B, L, R, ♭, ♯, η, ϵ).

Here is how to reconstruct some of its components from the other ones.

[figure: LA; A; LA; B; \begin{matrix}g^{♭} := \\ Lg;ε_{B} \end{matrix}; LA; LRB; Lg; A; RB; g; LRB; RB; LRB; B; ε_{B}; A; RLA; η_{A}; LA; RLA; LA; B; f; RLA; RB; Rf; A; RB; \begin{matrix}f^{♯} := \\ η_{A};Rf \end{matrix}; B; RB; B; RB; ε_{B}; LRB; RB; LRB; B; \begin{matrix}ε_{B} := \\ id_{RB} & ^{♭} \end{matrix}; RB; RB; _{id_{RB}}; B; RB; LA; A; LA; LA; _{id_{LA}}; A; RLA; \begin{matrix}η_{A} := \\ id_{LA} & ^{♯} \end{matrix}; LA; RLA; LA′; A′; LA′; LA; \begin{matrix}Lα := \\ (α;η_{A})^{♭} \end{matrix}; A′; RLA; A′; A; α; A; RLA; η_{A}; LA; RLA; LRB; RB; LRB; B; ϵ_{B}; B; B′; β; LRB; B′; RB; RB′; \begin{matrix}Rβ := \\ (ϵ_{B};β)^{♯} \end{matrix}; B′; RB′]

Programming with long names

⟨⟨a,b|->a,c⟩⟩ = function (⟨⟨a,b⟩⟩)
local a = pi1(⟨⟨a,b⟩⟩)
local b = pi2(⟨⟨a,b⟩⟩)
local c = ⟨⟨b|->c⟩⟩(b)
local ⟨⟨a,c⟩⟩ = {a, c}
return ⟨⟨a,c⟩⟩
end

⟨⟨a, b ↦ a, c⟩⟩ = function (⟨⟨a, b⟩⟩)

local a = pi1(⟨⟨a, b⟩⟩)
local b = pi2(⟨⟨a, b⟩⟩)
local c = ⟨⟨b ↦ c⟩⟩(b)
local ⟨⟨a, c⟩⟩ = {a, c}

return ⟨⟨a, c⟩⟩

end

[figure]

⟨⟨a,b|->a,c⟩⟩ = function (⟨⟨a,b⟩⟩)
local a = pi1(⟨⟨a,b⟩⟩)
local b = pi2(⟨⟨a,b⟩⟩)
local c = ⟨⟨b|->c⟩⟩(b)
local ⟨⟨a,c⟩⟩ = {a, c}
return ⟨⟨a,c⟩⟩
end

                                 dnc00 = function (dnc01)
                                     local a = pi1(dnc01)
                                     local b = pi2(dnc01)
                                     local c = dnc02(b)
                                     local dnc03 = {a, c}
                                     return dnc03
                                   end

[figure]

Note that diagrams are perfectly good as names. We can have:

⟨⟨ [figure: a, b; a; a, b; c; a; b↦c; c; b↦c] ⟩⟩ := {...}

In the (ascii) source code this would be:

⟨⟨\diag{adjunction1}⟩⟩ := {...}

The Yoneda Lemma

(η ↔ ♯) in adjunctions:

[figure: (; a; a^{LR}; η; a^{L}; a^{LR}; ); (; a^{L}; c; a; c^{R}; c; •; (iso); )]

Lemma on preuniversals:

[figure: (; a; b^{R}; b; b^{R}; ); (; b; c; a; c^{R}; c; •; )]

[figure] Lemma on preuniversals:

[figure: (; a; b^{R}; b; b^{R}; ); (; b; c; a; c^{R}; c; •; )]

Yoneda Lemma:

[figure: (; ∗; b^{R}; b; b^{R}; ); (; b; c; ∗; c^{R}; c; •; ); (; ∗; b^{R}; b; b^{R}; ); b^{R}; (; b; c; ∗; c^{R}; c; •; ); (; b; c; c; •; c^{R}; )]

[figure] Yoneda Lemma:

[figure: (; ∗; b^{R}; b; b^{R}; ); (; b; c; ∗; c^{R}; c; •; ); (; ∗; b^{R}; b; b^{R}; ); b^{R}; (; b; c; ∗; c^{R}; c; •; ); (; b; c; c; •; c^{R}; )]

Corollary:

[figure: (; ∗; a↦b; b; a↦b; ); (; b; c; ∗; a↦c; c; •; ); (; ∗; a↦b; b; a↦b; ); a↦b; (; b; c; ∗; a↦c; c; •; ); (; b; c; a; c; c; •; )]

[figure]

(η ↔ ♯) in adjunctions:

[figure: (; a; a^{LR}; η; a^{L}; a^{LR}; ); (; a^{L}; c; a; c^{R}; c; •; (iso); )]

Definition of universal arrow:

[figure: (; a; b^{R}; univ; b; b^{R}; ); (; b; c; a; c^{R}; c; •; (iso); )]

[figure]

[figure]

Definition of universal arrow:

[figure: (; a; b^{R}; univ; b; b^{R}; ); (; b; c; a; c^{R}; c; •; (iso); )]

Definitions of universal element and representable functor:

( [figure: ∗; b^{R}; univ; b; b^{R}]) ( [figure: b; c; ∗; c^{R}; c; •; (iso)]) [figure] [figure] ( [figure: ∗; b^{R}; univ; b; b^{R}])

b^{R} ; (universal ; element)

[figure]

[figure] ( [figure: b; c; ∗; c^{R}; c; •; (iso)])

( [figure: b; c; c; •; c^{R}; (iso)] )

(R is representable and is represented by B)

[figure] [figure] [figure] The Yoneda Lemma (2) We can formalize the previous diagram in type system (or in a programming language — say, ML or Coq). Let’s look at a miniature.

Lemma on preuniversals:

[figure: (; a; b^{R}; b; b^{R}; ); (; b; c; a; c^{R}; c; •; )]

Yoneda Lemma:

[figure: (; ∗; b^{R}; b; b^{R}; ); (; b; c; ∗; c^{R}; c; •; ); (; ∗; b^{R}; b; b^{R}; ); b^{R}; (; b; c; ∗; c^{R}; c; •; ); (; b; c; c; •; c^{R}; )]

[figure]

In the top box: B : B_{0} A : A_{0} R : B → Set a ↦ b^{R} ≡ g : Hom_{A}(A, RB)

( [figure: a; b^{R}; b; b^{R}]) ≡ (A, B, g)

c ⇒ (b ↦ c) ≡ Hom_{B}(B, −) : B → Set c ⇒ (a ↦ c^{R}) ≡ C ↦ Hom_{A}(A, RC) ≡ Hom_{A}(A, R−) : B → Set

( [figure: b; c; a; c^{R}; c; •]) ≡ T : Nat(Hom_{B}(B, −), Hom_{A}(A, R−))

g ↤ T := λT.(T Bid_{B}) g ↦ T := λf.(λC.λg.(f; Rg))

When we move to the bottom box we specialize: 𝔸 := Set A := 1 ≡ {∗}

∗ : 1 Monads A protomonad for a proto-endofunctor T : A → A is a 4-uple:

(A, T, η, μ)

that we draw as:

A [figure: η_{A}] T A [figure: μ_{A}] T T A

A proto-comonad for a proto-endofunctor S : B → B is a 4-uple:

(B, S, ε, δ)

that we draw as:

B [figure: ε_{B}] SB [figure: δ_{B}] SSB

Each proto-adjunction induces both a proto-monad and a proto-comonad. We draw all these together as:

[figure: LRLRB; LRB; \begin{matrix}δ_{B} := \\ Lη_{RB} \end{matrix}; LRB; B; \begin{matrix}ε_{B} := \\ id & RB & ^{♭} \end{matrix}; A; RLA; \begin{matrix}ηA := \\ id & LA & ^{♯} \end{matrix}; RLA; RLRLA; \begin{matrix}μA := \\ Rϵ_{LA} \end{matrix}; LA; A; LA; B; g^{♭}; LA; B; f; A; RB; g; A; RB; f^{♯}; B; RB; B; A; L; B; A; R]

\begin{matrix}{LA \atop ϵ_{LA} : LRLA → LA} & ϵ \\ μ_{A} := Rϵ_{LA} : RLRLA → RLA \end{matrix} R  \begin{matrix}{RB \atop η_{RB} : RB → RLRB} & ♯ \\ δ_{B} := Lη_{RB} : LRB → LRLRB \end{matrix} L

From monads to adjunctions An expensive adjunction comes with a monad. If we erase the ‘♭’, the ‘♯’, etc of this adjunction and leave only the monad, can we reconstruct the original adjunction from that? The answer is no. But we can construct two adjunctions from the monad,

A_{T} [figure: L_{T}; R_{T}] A (Kleisli)

A^{T} [figure: L^{T}; R^{T}] A (Eilenberg-Moore)

that are related to the original adjunction

B [figure: L; R] A

in interesting ways — by comparison functors F_{T} and F^{T}.

[figure: A_{T}; B; F_{T}; B; A^{T}; F^{T}; A_{T}; A; L_{T}; A_{T}; A; R_{T}; B; A; L; B; A; R; A^{T}; A; L^{T}; A^{T}; A; R^{T}]

The Kleisli category of a monad

A_{T} has the same objects as A, but we write them in a funny way — [A [figure] T A] instead of A — because Hom_{A_{T}} ≠ Hom_{A} and ∘_{A_{T}} ≠ ∘_{A}.

[f] : [A [figure] T A] → [C [figure] T C] (in A_{T}) is f : A → T C in A. [f]; [g] := [f; T g; μ_{E}].

[A [figure] T A] [A [figure] T A]_{id_{[A−→T A]:=[η_{A}]}} [figure]  A  T A_{η_{A}} [figure] [figure] [A [figure] T A] [C [figure] T C]_{[f]} [figure] [C [figure] T C] [E [figure] T E]_{[g]} [figure] [A [figure] T A] [E [figure] T E] _{\begin{matrix}[f];[g] := \\ [f;T g;μ_{E}] \end{matrix}} [figure]  A  T C_{f} [figure] [figure] C  T C [figure] [figure] C  T E_{g} [figure] [figure]T C  T T E_{T g} [figure] [figure] E  T E [figure] [figure] T E  T T E [figure]_{μ_{E}}

[A [figure] T A]  A [figure] [A [figure] T A] [A′ [figure] T A′]_{\begin{matrix}L_{T} α := \\ [α;η_{A′}] \end{matrix}} [figure]  A A′_{α} [figure] [A′ [figure] T A′]  A′ [figure] [figure] [C [figure] T C]  T C [figure] [C [figure] T C] [C′ [figure] T C′]_{[γ]} [figure]  T C T C′_{\begin{matrix}R_{T} ([γ]) := \\ T γ;μ_{C′} \end{matrix}} [figure] [C′ [figure] T C′]  T C′ [figure] [figure]

Proving that ∘_{A_{T}} is non-trivial, by the way — but in the syntactical world that doesn’t matter.

The Kleisli adjunction of a monad

[A′ [figure] T A′]  A′ [figure] [A′ [figure] T A′] [A [figure] T A]_{\begin{matrix}L_{T} α := \\ [α;η_{A′}] \end{matrix}} [figure]  A′ A_{α} [figure] [figure] [A [figure] T A]  A [figure] [A [figure] T A] [C [figure] T C]_{f^{♭}:=[f]} [figure] [A [figure] T A] [C [figure] T C]_{[g]} [figure]  A T C_{f} [figure] A T C_{[g]^{♯}:=g} [figure] [figure] [figure] [C [figure] T C]  T C [figure] [C [figure] T C] [C′ [figure] T C′]_{[γ]} [figure]  T C T C′_{\begin{matrix}R_{T} ([γ]) := \\ T γ;μ_{C′} \end{matrix}} [figure] [C′ [figure] T C′] T C′ [figure] [figure] A_{T}  A [figure]_{L_{T}} A_{T}  A_{R_{T}}  [figure] [T T C [figure] T T T C] [T C [figure] T T C] [figure]_{\begin{matrix}δ_{[C−→T C]} := \\ L_{T} (η_{(R_{T} [C−→T C])}) = \\ L_{T} (η_{T C}) = \\ [η_{T C};η_{T T C}] \end{matrix}} [T C [figure] T T C] [C [figure] T C]_{\begin{matrix}ϵ_{[C−→T C]} := \\ [id_{T C}] \end{matrix}} [figure]  A T A_{η_{A}} [figure] T A T T A [figure]_{μ_{A}}

The Eilenberg-Moore category of a monad A proto-algebra for a monad (A, T, η, μ) is a pair (A, α : T A → T). An algebra for a monad (A, T, η, μ) is a proto-algebra (A, α) that obeys T α; α = μ_{A}; α. A proto-morphism f : (A, α) → (C, γ) of (proto-)algebras is just a morphism f : A → C. A morphism of algebras is a proto-morphism f that obeys α; f = T f; γ. The proto-Eilenberg-Moore category of a monad (A, T, η, μ) has the proto-algebras as objects and the proto-morphisms of (proto-)algebras as morphisms. We write it as A^{T}. The Eilenberg-Moore category of a monad (A, T, η, μ), A^{T}, has the algebras as objects and the morphisms of algebras as morphisms. We also write it as A^{T},

Here is the adjunction A^{T} [figure: L^{T}; R^{T}] A:

[T A [figure: μ_{A}] T T A]  A [figure] [T A [figure: μ_{A}] T T A] [C [figure: γ] T C]_{f^{♭}:=T f;γ} [figure] [T A [figure: μ_{A}] T T A] [C [figure: γ] T C]_{g} [figure]  A T C_{f} [figure] A T C_{g^{♯}:=η_{A};g} [figure] [figure] [figure] [C [figure: γ] T C]  T C [figure] A^{T}  A [figure] _{L^{T}} A^{T}  A_{R^{T}}  [figure] [T T C [figure: T T γ] T T T C] [T C [figure: T γ] T T C] [figure]_{δ_{γ}:=T η_{C}?} [T C [figure: T γ] T T C] [C [figure: γ] T C]_{ϵ_{γ}:=γ} [figure]  A T A_{η_{A}} [figure] T A T T A [figure]_{μ_{A}}

The comparison theorem Everything fits in this diagram:

[figure: A_{T}; B; F_{T}; B; A^{T}; F^{T}; A_{T}; A; L_{T}; A_{T}; A; R_{T}; B; A; L; B; A; R; A^{T}; A; L^{T}; A^{T}; A; R^{T}]  [A [figure] RLA] [C [figure] RLC] [RLA [figure: μ_{A}] RLRLA] [RLC [figure: μ_{C}] RLRLC]  A RLC [figure] LA LC [figure]  [A [figure] RLA] [C [figure] RLC] [figure] [RLA [figure: μ_{A}] RLRLA] [RLC [figure: μ_{C}] RLRLC] [figure]  A [figure] [figure] RLC [figure] [figure] LA  A [figure] LC  RLC [figure]A [figure] [figure] RLC [figure] [figure] LA[figure] [figure] LC[figure] [figure] LA  [figure] [figure] LC  [figure] [figure]  [figure] [figure] [figure] [figure] [figure]  [figure][figure] [figure]

\begin{matrix}{[g] : [A [figure] RLA] → [C [figure] RLC] \atop g : A → RLC} & ren \\ F_{T} ([g]) := g^{♭} : LA → LC \end{matrix} ; ♭

\begin{matrix}\begin{matrix}{A \atop LA} & L \\ ϵ_{LA} : LRLA → LA \end{matrix} & ϵ \\ μ_{A} = Rϵ_{LA} : RLRLA → RLA \end{matrix} R  \begin{matrix}{B \atop ϵ_{B} : LRB → B} & ϵ \\ Rϵ_{B} : RLRB → RB \end{matrix} R

Beck’s lemma From Beck’s thesis (1967), reprinted at:

http://www.tac.mta.ca/tac/reprints/articles/2/tr2abs.html

DEFINITION 3. The adjoint pair α : F ⊣ U is tripleable if Φ : B → A^{T} is an equivalence of categories. DEFINITION 3’. A functor U : B → A is tripleable if U has a left adjoint F and the adjoint pair F ⊣ U is tripleable. (...) THEOREM 1. Let α : F ⊣ U be an adjoint pair.

(1) If B has coequalizers, then there exists a left adjoint Φ̂ ⊣ Φ. Assuming the existence of Φ̂:

(2) If U preserves coequalizers, then the unit of Φ̂ ⊣ Φ is an isomor-

phism AT →^{≡} Φ̂Φ.

(3) If U reflects coequalizers, then the counit is an isomorphism

ΦΦ̂ →^{≡} B.

Finally, in the presence of (2), (3) can be replaced by: (3’) If U reflects isomorphisms, then the counit is an isomorphism

ΦΦ̂ →^{≡} B.

I will call item (1) of Theorem 1 “Beck’s Lemma”. In our notation this will be: if in an adjunction B [figure: L; R] A the category B has coequalizers then the comparison functor F^{T} : B → A^{T} has a left adjoint, Λ (i.e. we have an adjunction Λ ⊣ F^{T}). We need to construct Λ_{0}, Λ_{1}, ♭^{T}, ♯^{T}.

Beck’s lemma (2) Sketch of the proof (a construction, actually): Let’s will write Λ as [A [figure: α] T A] ↦ Λ_{α}.

The action of Λ on objects: for each object [A [figure: α] T A] in A^{T} we need to produce an object Λ_{α} in B. We define it as the coequalizer of ϵ_{LA} and Lα.

\begin{matrix}{A \atop LA} & L \\ ϵ_{LA} : LRLA → LA \end{matrix} ϵ \begin{matrix}{[A [figure: α] T A] \atop α : RLA → A} & ren \\ Lα : LRLA → LA \end{matrix} ; L q_{α} : LA↠Λ_{α} coeq

Λ_{α} tgt

The action of Λ on morphisms (Λ_{h} := (Lh; q_{α})/q_{α′}), and the transpositions:

LRLA′  LA′^{ϵ_{LA′}}  [figure] LRLA′  LA′_{Lα′}  [figure] LA′  Λ_{α′}^{q_{α′}}  [figure]  [A′ [figure: α′] RLA′] Λ_{α′} [figure] [figure] LRLA  LA_{ϵ_{LA}}  [figure] LRLA  LA_{Lα}  [figure] LA  Λ_{α}_{q_{α}}  [figure]  [A [figure: α] RLA] Λ_{α} [figure] [figure] LA′ LA_{Lh} [figure] LA′  Λ_{α}_{Lh;q_{α}} [figure]  [figure] [figure]Λ_{α′} Λ_{α}_{Λ_{h}} [figure] [figure] [figure]  [A′ [figure: α′] RLA′] [A [figure: α] RLA]_{h} [figure] [figure] [figure] [figure]_{♭^{T}} [figure]_{♯^{T}} [figure] [figure] LA  B_{\begin{matrix}g^{β}, \\ q_{α};f \end{matrix}}  [figure] [figure]Λ_{α} B_{g^{♭^{T}}} [figure] Λ_{α} B_{f} [figure]  [A [figure: α] RLA] [RB [figure: Rε_{B}] RLRB]_{g} [figure] [A [figure: α] RLA] [RB [figure: Rε_{B}] RLRB]_{f^{♯^{T}}} [figure] B  [RB [figure: Rε_{B}] RLRB] [figure] [figure]

\begin{matrix}\begin{matrix}{[A [figure: α] RLA] \atop q_{α} : LA↠Λ_{α}} & f : Λ_{α} → B \\ q_{α}; f : LA → B \end{matrix} & ; \\ f^{♯^{T}} := (q_{α}; f)^{♯} : A → RB \end{matrix} ; ♯

{[A [figure: α] RLA] \atop q_{α} : LA↠Λ_{α}} {g : [A [figure: α] RLA] → [RB [figure: Rε_{B}] RLRB] \atop g : A → RB} ; g^{♭} : LA → B ; ♭ g^{♭^{T}} := g^{♭}/q_{α} : Λ_{α} → B

fact.through.coeq Monads and cohomology Quoting again from Beck’s thesis (p.12)...

2. Cohomology

Adjoint functors, it is now well known, lead to cohomology ([Eilenberg & Moore (1965a), Godement (1958), Mac Lane (1963)] — or to homotopy [Huber (1961)]). If

\underline{A} →^{F} \underline{B} →^{A} \underline{A} (F ⊣ U)

is an adjoint pair, objects of the form AF ∈ |B| are regarded as “free” relative to the underlying object functor U. The counit

XUF →^{Xϵ} X

is intuitively the first step of a functorial free resolution of any object X ∈ |\underline{B}|. By iterating UF one extends X to a free simplicial resolution of X, and defines derived functors as usual in homological algebra. Here we only consider the simplest case, that of defining cohomology groups

H^{n}(X, Y), n ≥ 0,

of an object X ∈ |\underline{B}| with coefficients in an abelian group object Y ∈ |\underline{B}|, relative to the given underlying object functor U : \underline{B} → A (having a left adjoint). Tripleableness of F ⊣ U will not play any appreciable role until we discuss special properties of the cohomology in §3. We now recall the details of the construction of the cohomology groups. Some of the terms used are clarified in the proof of Theorem 2, which summarizes the main properties the cohomology possesses.

How much of that has nice syntactical proofs? (I don’t know yet!)

Cartesian Closed Categories A Cartesian Closed Category (“CCC”) (C, ×, 1, →) is a category C plus a “cartesian closed structure” (×, 1, →) on it. Again, we will have cheap ways and expensive ways to specify (×, 1, →). The cheap ways (there will be several of them) will appear from formalizing this diagram:

[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; uncur g; A × B; C; f; A; B→C; g; A; B→C; cur f; C; B→C]

Another way — the “adjoint presentation” of a CCC — will be by requiring that the functors A ↦ (A × A), A ↦ •, and A ↦ A × B (note that for each object B of C we have a different A ↦ A × B) all have right adjoints:

[figure: (A, A); A; (A, A); (B, C); (h;π,h;π′); (A, A); (B, C); (f,g); A; B × C; h; A; B × C; ⟨f,g⟩; (B, C); B × C; •; A; •; •; id; •; •; id; A; 1; g; A; 1; !; •; 1; A × B; A; A × B; C; uncur g; A × B; C; f; A; B→C; g; A; B→C; cur f; C; B→C]

The adjoint presentation is quite elegant, but if we expand all the details we see that it is much more expensive than the other ones.

By the way: a (cheap) topos, (C, ×, 1, →, Ω), is a CCC plus a “classifier object”, Ω, where the Ω obeys this magic axiom, that has lots of consequences:

[figure: B′; 1; !; B′; B; 1; Ω; B; Ω; P; ↘]

Cheap and expensive toposes What matters to us is: a CCC is a category in which we can interpret λ-calculus; a topos is a category in which we can interpret (a kind of) set theory; a hyperdoctrine is a category in which we can interpret first-order logic. (I’m simplifying things a little bit, but anyway).

When we buy a cheap topos it takes a lot of work to build the constructions that interpret first-order logic in it... in a hyperdoctrine they sort of come out-of-the-box.

An expensive topos has all the structure and properties of an expensive hyperdoctrine plus a few more.

The category of sets, Set, is a topos, and therefore if you go to the supermarket with the intent of buying the category of sets you will find it there in several different presentations... the more expensive ones have all the hyperdoctrine rules, all the topos rules, plus some. λ-calculus in a CCC: an example We can interpret the λ-construction

\begin{matrix}A & f : B → C \\ λd:(A × B).⟨πd, f(π′d)⟩ : A × B → A × C \end{matrix}

in a Cartesian Closed Category as this diagram:

[figure: A × B; B; π′; A × B; A; π; A × B; A × C; \begin{matrix}λd:(A×B). \\ ⟨πd,f(π′d)⟩ \end{matrix}; A × B; C; B; C; f; A; A × C; A × C; C]

And we can interpret its “internalization”,

\begin{matrix}A & B & C \\ λf:(B→C).λd:(A × B).⟨πd, f(π′d)⟩ : (B → C) → (A × B → A × C) \end{matrix}

using this diagram:

[figure: A × B; (B→C)×(A×B); A × B; A; A × B; B; (B→C)×(A×B); (B→C)×(A×B); (B→C)×(A×B); B; (B→C)×(A×B); (B→C)×B; (B→C)×(A×B); B→C; B; (B→C)×B; (B→C)×B; B→C; (B→C)×B; C; ev; (B→C)×(A×B); A; (B→C)×(A×B); C; (B→C)×(A×B); A × C; A; A × C; A × C; C; (B→C) × (A×B); (B→C); (B→C) × (A×B); A × C; (B→C); (A×B)→(A×C); \begin{matrix}λf:(B→C). \\ λd:(A×B). \\ ⟨πd,f(π′d)⟩ \end{matrix}; A × C; (A×B)→(A×C); cur]

λ-calculus in a CCC: an example (2) ...but in a case like this the diagrams are secondary, and for most λ-terms they are unbearably big... we should focus on the trees.

[figure: A × B; (B→C)×(A×B); A × B; A; A × B; B; (B→C)×(A×B); (B→C)×(A×B); (B→C)×(A×B); B; (B→C)×(A×B); (B→C)×B; (B→C)×(A×B); B→C; B; (B→C)×B; (B→C)×B; B→C; (B→C)×B; C; ev; (B→C)×(A×B); A; (B→C)×(A×B); C; (B→C)×(A×B); A × C; A; A × C; A × C; C; (B→C) × (A×B); (B→C); (B→C) × (A×B); A × C; (B→C); (A×B)→(A×C); \begin{matrix}λf:(B→C). \\ λd:(A×B). \\ ⟨πd,f(π′d)⟩ \end{matrix}; A × C; (A×B)→(A×C); cur]

\begin{matrix}\begin{matrix}(b ↦ c), (a, b) ⊢ a, b & π′ \\ (b ↦ c), (a, b) ⊢ a \end{matrix} ; ; π & \begin{matrix}\begin{matrix}(b ↦ c), (a, b) ⊢ a, b & π′ \\ (b ↦ c), (a, b) ⊢ b \end{matrix} ; ; π′ & (b ↦ c), (a, b) ⊢ b ↦ c π \\ (b ↦ c), (a, b) ⊢ c \end{matrix} ; app \\ (b ↦ c), (a, b) ⊢ a, c \end{matrix} ; ⟨, ⟩ ; b ↦ c ⊢ a, b ↦ a, c ; cur

\begin{matrix}{π′ \atop π′; π} & \begin{matrix}{π′ \atop π′; π′} & π \\ ⟨π, π′; π′⟩; ev \end{matrix} \\ ⟨π′; π, ⟨π, π′; π′⟩; ev⟩ \end{matrix}

cur⟨π′; π, ⟨π, π′; π′⟩; ev⟩ [figure]

[figure]

\begin{matrix}\begin{matrix}(b ↦ c), (a, b) ⊢ a, b & π′ \\ (b ↦ c), (a, b) ⊢ a \end{matrix} ; ; π & \begin{matrix}\begin{matrix}(b ↦ c), (a, b) ⊢ a, b & π′ \\ (b ↦ c), (a, b) ⊢ b \end{matrix} ; ; π′ & (b ↦ c), (a, b) ⊢ b ↦ c π \\ (b ↦ c), (a, b) ⊢ c \end{matrix} ; app \\ (b ↦ c), (a, b) ⊢ a, c \end{matrix} ; ⟨, ⟩ ; b ↦ c ⊢ a, b ↦ a, c ; cur

\begin{matrix}{[d]^{1} \atop πd} & \begin{matrix}{[d]^{1} \atop π′d} & f \\ f(π′d) \end{matrix} \\ ⟨πd, f(π′d)⟩ \end{matrix} ; λd.⟨πd, f(π′d)⟩

[figure]

\begin{matrix}\begin{matrix}(b ↦ c), (a, b) ⊢ a, b & π′ \\ (b ↦ c), (a, b) ⊢ a \end{matrix} ; ; π & \begin{matrix}\begin{matrix}(b ↦ c), (a, b) ⊢ a, b & π′ \\ (b ↦ c), (a, b) ⊢ b \end{matrix} ; ; π′ & (b ↦ c), (a, b) ⊢ b ↦ c π \\ (b ↦ c), (a, b) ⊢ c \end{matrix} ; app \\ (b ↦ c), (a, b) ⊢ a, c \end{matrix} ; ⟨, ⟩ ; b ↦ c ⊢ a, b ↦ a, c ; cur

\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

[figure]

[figure]

The product property

For any diagram of the form B [figure: p] P [figure: p′] C in a category C we have a natural operation,

[figure: (; A; P; h; ); (; A; B; h;p; A; C; h;p′; ); Hom_{C}(A, P); Hom_{C}(A, B) × Hom_{C}(A, C); h; (h; p, h; p′)]

whose action is to compose any given h : A → P with p and p′. Both Hom_{C}(−, P) and Hom_{C}(−, B) × Hom_{C}(−, C) are (contravariant) functors from C^{op} to Set, and the operation above is a natural transformation

prod^{♮} : Hom_{C}(−, P) → Hom_{C}(−, B) × Hom_{C}(−, C)

The product property for a diagram B [figure: p] P [figure: p′] C. is an inverse for the “natural” natural transformation above.

Product diagrams

Whenever we write B [figure: π] B × C [figure: π′] C, using the product symbol in the middle object, it will be implicit that the B × C must “deserve its name”: that is, we must have “projection maps” π and π′ (here they were shown explicitly),

and the diagram B [figure: π] B × C [figure: π′] C must have the product property.

We can draw the two natural transformations together as:

A^{op} [figure: .] (( [figure: A; B × C] ) [figure: ^{prod^{♮}}; prod] ( [figure: A; B; A; C] ))

but note that the projection maps did not appear in the picture... As we can make diagram stand for whatever we want (because diagrams are valid as long names) we will take diagrams of this form as meaning:

[figure: A; B; f; A; B × C; ⟨f,g⟩; A; C; g; B × C; B; π; B × C; C; π′]

a diagram B [figure: π] B × C [figure: π′] C, plus the product property for it, plus a syntactical cue for how to name the results of prod; in this case, this is: :

f : A → B g : A → C
(f, g) : Hom_{C}(A, B) × Hom_{C}(A, C)

⟨f, g⟩ : A → B × C prod^{A}

or, more briefly:

\begin{matrix}f : A → B & g : A × C \\ ⟨f, g⟩ : A → B × C \end{matrix} prod

although this will be an abuse of language, in a sense — Product diagrams (2)

[figure: A; B; f; A; B × C; ⟨f,g⟩; A; C; g; B × C; B; π; B × C; C; π′]

Note that if we write the rule prod as:

{(f : A → B, g : A → C) \atop ⟨f, g⟩ : A → B × C} prod

then it is exactly the inverse of:

{h : A → B × C \atop (h; π : A → B, h; π : A → C)} ^{prod^{♮}} := \begin{matrix}{h : A → B × C \atop h; π : A → B} & {h : A → B × C \atop h; π : A → C} \\ (h; π : A → B, h; π : A → C) \end{matrix}⟨, ⟩

We will repeat this pattern all over the place: for some derived rule, blah^{♮}, an inverse blah.

Note that if you were given just B [figure: π] B × C [figure: π′] C and

A^{op} [figure: .] (( [figure: A; B × C] ) [figure: ^{prod^{♮}}; prod] ( [figure: A; B; A; C] ))

then you would have to figure out the “natural construction” for prod^{♮} yourself; and then prod would be its inverse.

Products as adjunctions If we rewrite the previous NT using the category C × C and we flip the positions of the two vertical arrows it becomes:

A^{op} [figure: .] ( [figure: (A, A); (B, C); A; B × C; _{prod_{♮}}; prod] )

which looks almost like an adjunction... In fact, if for any two objects B and C of C we have a product object B × C (that “deserves its name”, i.e., comes with π, π′, and the product property) then we have this adjunction,

[figure: (A, A); A; Δ; (A, A); (B, C); h^{♭}:=(h;π,h;π′); (A, A); (B, C); (f,g); A; B × C; h; A; B × C; (f,g)^{♯}:=⟨f,g⟩; (B, C); B × C; ×; ♭=prod^{♮}; ♯=prod; (B × C, B × C); (B, C); (π,π′); A; A × A; ⟨id,id⟩; C × C; C; Δ; C × C; C; ×]

where the action of × on a morphism (β, γ) : (B, C) → (B′, C′) of C × C yields β × γ := ⟨π; β, π′; γ⟩:

[figure: B; B × C; π; B × C; C; π′; B; B′; β; B × C; B′; π;β; B × C; B′ × C′; ⟨π;β,π′;γ⟩; B × C; C′; π′;γ; C; C′; β; B′; B′ × C′; π; B′ × C′; C′; π′]

Exponentials In a category with binary products, (C, ×), an object deserves the name B→C if it comes with an evaluation map, ev : (B→C)×B → C, and an inverse, cur, for the “uncurrying” operation:

[figure: A×B; A; A×B; C; \begin{matrix}uncur g := \\ g×B; ev \end{matrix}; A×B; (B→C)×B; g×B; A; B→C; g; (B→C)×B; B→C; (B→C)×B; C; ev]

This, again, looks like an adjunction:

A^{op} [figure: .] ( [figure: A×B; C; A; B→C; uncur; cur] )

where the top functor, A ↦ A × B, is known.

Let’s fix the object B. If we have the action of C ↦ B→C on objects — i.e., for each C we have B→C, ev_{BC} and cur_{BC} — then we can build (B→)_{1}. The trick comes from slide 21 (its bottom rectangle):

[figure: (B→C)×B; B→C; (B→C)×B; C; _{ev_{BC}}; C; C′; γ; (B→C)×B; C′; B→C; B→C′; \begin{matrix}B→γ := \\ cur(ev_{BC};γ) \end{matrix}; C′; B→C′]

We have just built an andjunction (B×) ⊣ (B→) from an operation C ↦ B→C.

Exponentials (2) It turns out that we can also construct a functor (B^{op}, C) ↦ B→C. Its action on objects is obvious; its action on morphisms takes each (β^{op}, γ) : (B^{op}, C) → (B^{′op}, C′) to (β→γ) := (→_{1})(β^{op}, γ) := cur(⟨π, π′; β⟩; ev; γ),

[figure: (B^{op}, C); B→C; (B^{op}, C); (B^{′op}, C′); (β^{op},γ); B→C; B′→C′; \begin{matrix}(β→γ) := \\ (→_{1})(β^{op},γ) := \\ cur(⟨π,π′;β⟩;ev;γ) \end{matrix}; (B^{′op}, C′); B′→C′]

where cur(⟨π, π′; β⟩; ev; γ) is:

\begin{matrix}\begin{matrix}\begin{matrix}B & C \\ B→C \end{matrix} & b′ ⊢ b \\ (b ↦ c), b′ ⊢ (b ↦ c), b \end{matrix} & \begin{matrix}B & C \\ (b ↦ c), b ⊢ c \end{matrix} & c ⊢ c′ \\ (b ↦ c), b′ ⊢ c′ \end{matrix} ; (b ↦ c) ⊢ (b′ ↦ c′)

\begin{matrix}\begin{matrix}\begin{matrix}B & C \\ B→C \end{matrix} & β : B′ → B \\ ⟨π_{(B→C)B′}, π′_{(B→C)B′}; β⟩ \end{matrix} & \begin{matrix}B & C \\ ev & BC \end{matrix} ev & γ : C → C′ \\ ⟨π, π′; β⟩; ev; γ \end{matrix} ; ;
cur(⟨π, π′; β⟩; ev; γ)

cur

But how can we find a definition like the one above for (β→γ) — without using brute force?

Morphisms as sequents We can lift the natural deduction tree

\begin{matrix}\begin{aligned}\begin{aligned}[b′]^{1} & b′ ↦ b \\ & b \end{aligned} & & [b ↦ c]^{2} \\ & c \end{aligned} & c ↦ c′ \\ c′ \end{matrix} ; b′ ↦ c′ ; 1 ; (b ↦ c) ↦ (b′ ↦ c′) 2

to something that looks more like sequent calculus, in the sense that the hypotheses are always listed explicitly before the ‘⊢’, and names with ‘⊢’ stand for morphisms:

\begin{matrix}\begin{matrix}\begin{matrix}\begin{matrix}(b ↦ c), b′ ⊢ b′ π′ & b′ ⊢ b \\ (b ↦ c), b′ ⊢ b \end{matrix} ; & (b ↦ c), b′ ⊢ (b ↦ c) π \\ (b ↦ c), b′ ⊢ c \end{matrix} ; app & c ⊢ c′ \\ (b ↦ c), b′ ⊢ c′ \end{matrix} & ; \\ (b ↦ c) ⊢ (b′ ↦ c′) \end{matrix} ; cur

I don’t want to get into the details of this now...

Hyperdoctrines The following is the precise definition of a hyperdoctrine. It is too technical, so we will spend the next slides dissecting it.

A hyperdoctrine is a (cloven) fibration, p : 𝔼 → 𝔹, plus some extra structure:

• the base category 𝔹 is a CCC (i.e., (𝔹, ×, 1, →) is a CCC))

• each fiber 𝔼_{B} is a CCC (i.e., each (𝔼_{B}, ∧, ⊤, [figure]) is a CCC)

• for each map g : B → C in 𝔹 the change-of-base functor f^{∗} has adjoints ∃_{f} ⊣ f^{∗} ⊣ ∀_{f}

• change-of-base preserves ∧, ⊤, [figure]modulo iso (P∧, P⊤, P [figure])

• the left and right Beck-Chevalley conditions hold (BCCL, BCCR)

• the Frobenius condition holds (Frob)

The precise definition of what a fibration is is quite technical. I will give it in full here — it will take several slides — but if you are a non-specialist you should only pay only attention to the last two operations: change-of-base functors and the isomorphism between two changes of base for the same g : B → C.

Subobjects Our archetypical fibration will be Cod : CanSub(Set) → Set, where the “codomain functor”, Cod, takes each “canonical subobject” P in Set (where P is an inclusion map { b ∈ B | P (b) } ↪ B) and returns its codomain, B.

The categorical way to describe “injective maps” is via the notion of “monic”. The monic arrows of Set are exactly the injective maps. In Set some injective maps are inclusions. Let’s regard Set as category with a (given) distinguished class of monics — the “inclusions”. A subobject of B is a monic A ↣ B with codomain B. A canonical subobject of B is an inclusion B′ ↪ B with codomain B.

Two subobjects of B, B′ ↣ B and B′′ ↣ B are isomorphic when there is an iso B′ ↔ B′′ making the obvious triangle commute:

[figure: B′; B′′; B′; B; B′′; B]

Each subobject f : B′ ↣ B is isomorphic to a unique canonical subobject of B:

[figure: B′; Im(f); B′; B; f; Im(f); B; Im(f); { b ∈ B | f^{−1}(b) ≠ ∅ }]

Subobjects (2) We will use the following notations for canonical subobjects. In the archetypal case,

explicit, long form: shorthand (note the ‘||’!):

( [figure: { a ∈ A | P (a) }; A] )

A

{ a || P (a) }

A

𝔼 = CanSub(Set)

𝔹 = Set

p=Cod

[figure]

and in the generic/abstract case,

[figure: P; A; 𝔼; 𝔹; p]

𝔼 is the “entire category”, 𝔹 is the “base category”, p is the “projection”, P is a “proposition over A”.

Note that instead of drawing a vertical arrow P ↦ pP =A we just draw P over A. (We will do the same for morphisms, by the way).

Subobjects (3) If B is an object of 𝔹, the fiber over B, 𝔼_{B}, is the subcategory of 𝔼 composed of the objects and morphisms of 𝔼 that are taken to B and id_{B} by the projection p.

Being “over B” means “belonging to 𝔼_{B}”. A morphism of 𝔼 is said to be vertical if its image is an identity in 𝔹. We will have a notion of “horizontal morphisms” too, but it will be harder to formalize — it will involve cartesianness. Let’s start with an example.

Every map g : B → C in the base category induces a “change-of-base functor”, g^{∗} : 𝔼_{C} → 𝔼_{B}, and a natural transformation \overline{g} : g^{∗} → id_{𝔼_{C}}, as in the diagram below:

[figure: \{ b || Q(b) \}; \{ b || R(g(b)) \}; \{ b || Q(b) \}; \{ c || R(c) \}; \{ b || R(g(b)) \}; \{ c || R(c) \}; \{ b || R(g(b)) \}; \{ b || S(g(b)) \}; \{ c || R(c) \}; \{ c || S(c) \}; \{ b || S(g(b)) \}; \{ c || S(c) \}; B; C; g; Q; g^{∗}R; k; Q; R; j; g^{∗}R; R; _{\overline{g}_{R}}; g^{∗}R; g^{∗}S; g^{∗}i; R; S; i; g^{∗}S; S; _{\overline{g}_{S}}; B; C; g]

The vertical map i : R → S exists iff { c | R(c) } ⊆ { c | S(c) }, i.e., if ∀c.R(c) [figure]S(c). The diagonal map j : Q → S exists iff its factorization through \overline{g}_{R}, k, exists (because every map in 𝔼 factors as “vertical map followed by an horizontal map”, and we shall see), and: the vertical map k : Q → g^{∗}R exists iff { b | Q(b) } ⊆ { b | R(g(b)) }, i.e., if ∀b.Q(b) [figure]R(g(b)) — so the vertical/horizontal factorization gives us a way to interpret diagonal morphisms “logically”.

Subobjects (4) The horizontal maps of the diagram

[figure: \{ b || Q(b) \}; \{ b || R(g(b)) \}; \{ b || Q(b) \}; \{ c || R(c) \}; \{ b || R(g(b)) \}; \{ c || R(c) \}; \{ b || R(g(b)) \}; \{ b || S(g(b)) \}; \{ c || R(c) \}; \{ c || S(c) \}; \{ b || S(g(b)) \}; \{ c || S(c) \}; B; C; g; Q; g^{∗}R; k; Q; R; j; g^{∗}R; R; _{\overline{g}_{R}}; g^{∗}R; g^{∗}S; g^{∗}i; R; S; i; g^{∗}S; S; _{\overline{g}_{S}}; B; C; g]

are pullbacks in Set:

[figure: { b | R(g(b)) }; { c | R(c) }; { b | R(g(b)) }; B; { c | R(c) }; C; B; C; { b | S(g(b)) }; { c | S(c) }; { b | S(g(b)) }; B; { c | S(c) }; C; B; C]

And so what?...

Cartesianness A vee in a category 𝔼 is a pair of morphisms in 𝔼, (h′ : P → R, g′ : Q → R) with common codomain. A completion for a vee (h′ : P → R, g′ : Q → R) is an arrow f′ : P → Q making the triangle commute. A functor p : 𝔼 → 𝔹 takes completions of (h′, g′) to completions of (ph′, pg′); let’s call this induced map p_{h′g′}^{♮}.

A vee (h′, g′) in 𝔼 has unique liftings (for p : 𝔼 → 𝔹) if the map p_{h′g′} induced by p is a bijection. A map g′ : Q → R in 𝔼 is cartesian if any vee (h′, g′) with g′ as its “lower leg” has unique liftings.

[figure: P; R; h′; P; Q; f′; Q; R; g′; A=pP; C=pR; h=ph′; A=pP; B=pQ; f=pf′; B=pQ; C=pR; g=pg′; p_{h′g′}^{♮}]

To make things more manageable we will use some shorthands: A := pP, B := pQ, C := pR, f := pf′, g := pg′, h := ph′, Invertibility of p_{h′g′}^{♮} means that for any completion f for the vee (h, g) there is exactly one completion f′ : P → Q for (h′, g′) “over f”, i.e., such that f = pf′.

Cartesianness (2) A proto-vee in a category 𝔼 is a pair of morphisms in 𝔼, (h′ : P → R, g′ : Q → R) with common codomain. A proto-completion for a vee (h′ : P → R, g′ : Q → R) is an arrow f′ : P → Q making the triangle commute. A functor p : 𝔼 → 𝔹 takes proto-completions of (h′, g′) to proto-completions of (ph′, pg′); let’s call this induced map p_{h′g′}^{♮}.

Note that this new induced map has a bigger domain... the old one had to act on all completions, the new one has to act on all proto-completions.

A vee with proto-unique liftings is a triple (h′, g′, p_{h′g′}), where p_{h′g′} is a proto-inverse for p_{h′g′}^{♮}.

[figure: P; R; h′; P; Q; f′; Q; R; g′; A=pP; C=pR; h=ph′; A=pP; B=pQ; f=pf′; B=pQ; C=pR; g=pg′; p_{h′g′}^{♮}; p_{h′g′}]

Proto-cartesianness for an arrow g′ is the assurance that any vee (h′, g′) with lower leg g′ has proto-unique liftings. More formally: a proto-cartesian morphism is a pair (g′, cart), where cart ≡ (P, h′ ↦ p_{h′g′}) is an operation that produces all the required proto-inverses.

Pullbacks are cartesian Cartesian maps are not so weird as the preceding definition suggests...

Fact. When p = Cod, “pullback squares are cartesian”. The core of the proof is the following diagram.

[figure: (\begin{matrix}A′′ \\ a↓ \\ A \end{matrix}); _{(\begin{matrix}B ×_{C} C′′ \\ π↓ \\ B \end{matrix})}; f′=( \begin{matrix}⟨a;f, h′′⟩ \\ f \end{matrix} ); _{(\begin{matrix}B ×_{C} C′′ \\ π↓ \\ B \end{matrix})}; _{(\begin{matrix}C′′ \\ c↓ \\ C \end{matrix})}; g′=( \begin{matrix}π′ \\ g \end{matrix} ); (\begin{matrix}A′′ \\ a↓ \\ A \end{matrix}); _{(\begin{matrix}C′′ \\ c↓ \\ C \end{matrix})}; h′=( \begin{matrix}h′′ \\ h \end{matrix} ); A; B; f; B; C; g; A; C; h; A′′; C′′; h′′; A′′; A; a; A′′; B ×_{C} C′′; ⟨a;f, h′′⟩; B ×_{C} C′′; C′′; π′; B ×_{C} C′′; B; π; C′′; C; c; A; B; f; B; C; g]

The arrow g′ = ( \begin{matrix}π′ \\ g \end{matrix} ) is a “pullback square”. Fix any h′ = ( \begin{matrix}h′′ \\ h \end{matrix} ) with the same codomain as g′. For any completion f of the lower vee (h, g),

its lifting is f′ = ( \begin{matrix}⟨a;f, h′′⟩ \\ f \end{matrix} ).

Cleavages Here’s the abstract view of cartesianness & friends — formulated in a way that projects well into the syntactical world. Note that the conditions pR = C, pg′ = g, etc, are always implicit; the conditions h = f; g and h′ = f′; g′ are implicit whenever f, g (resp. f′, g′) are defined and when we are in the real world; in the syntactical world they are irrelevant.

[figure: P; R; h′; P; Q; f′; Q; R; g′; A=pP; C=pR; h=ph′; A=pP; B=pQ; f=pf′; B=pQ; C=pR; g=pg′; p_{h′g′}^{♮}; p_{h′g′}]

Unique liftings for a vee (h′, g′) is an inverse p_{h′g′} for the natural operation p_{h′g′}^{♮}. Cartesianness for an arrow g′ is an operation cart_{g′} ≡ (P, h′ ↦ p_{h′g′}). A cartesian lifting for g : B → C at R is a triple clift_{gR} ≡ (Q, g′, cart_{g′}). A family of cartesian liftings for g : B → C is an operation clifts_{g} ≡ (R ↦ clift_{gR}). A cleavage (for the functor p : 𝔼 → 𝔹) is an operation cleavage ≡ (g ↦ clifts_{g}).

Or all at once: a cleavage (for the functor p : 𝔼 → 𝔹) is an operation cleavage ≡ (g ↦ (R ↦ (Q, g′, (P, h′ ↦ (f ↦ f′))))), or, more detailedly, cleavage ≡ (B, C, g ↦ (R ↦ (Q, g′, (A, P, h, h′ ↦ (f ↦ f′))))).

A cloven fibration is a 4-uple (𝔹, 𝔼, p, cleavage), where p : 𝔼 → 𝔹 and cleavage is a cleavage for p.

One further subtlety is needed to make this work in the syntactical world: as we need a restricted version of equality to be able to say “P is over A”, “f′ is over f”, etc, 𝔼 should be a “category defined over 𝔹”. (Details later!)

Cleavages (2) A cleavage is cleavage ≡ (B, C, g ↦ (R ↦ (Q, g′, (A, P, h, h′ ↦ (f ↦ f′))))), but that specification is too long (for humans). If we underline the letters whose values are subsumed from subsequent ones, we get: cleavage ≡ (\underline{B}, \underline{C}, g ↦ (R ↦ (\underline{Q}, g′, (\underline{A}, \underline{P} , \underline{h}, h′ ↦ (f ↦ f′))))), and if we erase the “redundant” letters, we get: cleavage ≡ g ↦ (R ↦ g′, (h′, f ↦ f′)) which is equivalent to: cleavage ≡ g, R ↦ g′, (f, h′ ↦ f′)

[figure: P; R; h′; P; Q; f′; Q; R; g′; A; C; h; A; B; f; B; C; g]

Let’s call the Q and the g′ produced by the cleavage g^{∗}R and \overline{g}_{R}:

[figure: P; R; h′; P; Q = g^{∗}R; f′; Q = g^{∗}R; R; g′=\overline{g}_{R}; A; C; h; A; B; f; B; C; g]

If we consider cleavage as fixed, we get an operation f, g, h′ ↦ f′ that factors f′ through the cartesian lifting of g at R = tgt f′, and if we make f = id_{B} (and thus A := B), then we get an operation g, h′ ↦ f′ where now f′ is a vertical morphism. It can be simplified. As g := h := ph′, it becomes h′ ↦ f′, the factorization of a “diagonal” morphism in 𝔼, h′, into a vertical morphism, f′, followed by a horizontal one, g′ = \overline{ph′}_{tgt h′}.

This factorization is reversible, in a sense: given f′ vertical and g′ cartesian (horizontal — not necessarily a \overline{g}_{R}), their composite h′ is “diagonal” (“h′ diagonal” means just “h′ ∈ 𝔼”).

Cleavage induces change-of-base A cheap cloven fibration is just a 4-uple (𝔹, 𝔼, p, cleavage); An expensive one also comes with change-of-base functions, factorization through cartesian morphisms, rules that say that the composites of cartesians are cartesian, a family of adjunctions R ↦ (p_{R} ⊣ clift_{R}) [← complete this], isos between different changes of base, etc.

Here’s how to build the action on morphisms of a change-of-base functor g^{∗} ((g^{∗})_{0} comes from cartesian liftings):

[figure: g^{∗}R′; R′; ^{\overline{g}^{R′}}; g^{∗}R′; g^{∗}R; \begin{matrix}g^{∗}r:=f′ \\ :=p_{h′g′} f \end{matrix}; g^{∗}R′; R; h′:=\overline{g}_{R′};r; R′; R; r; g^{∗}R; R; g′:=\overline{g}_{R}; A:=B; B; f:=id_{B}; B; C; g; A:=B; C; h:=g]

Adjoints to change-of-base In the archetypal case, p = Cod : CanSub(Set) → Set, every change-of-base functor f^{∗} has both a left and a right adjoint. In some cases these adjoints have simple forms.

Some terminology... a map π : A × B → A is a “projection”, and the correspondent π^{∗} : 𝔼_{A} → 𝔼_{A×B} is a “weakening functor”; a map π : A × B → A × B × B is a “diagonal”, and the correspondent δ^{∗} : 𝔼_{A×B×B} → 𝔼_{A×B} is a “contraction functor”. A π^{∗} “introduces a dummy variable”, a δ^{∗} “collapses two variables”.

[figure: { a, b || P (a, b) }; { a || ∃b.P (a, b) }; { a, b || P (a, b) }; { a, b || Q(a) }; { a || ∃b.P (a, b) }; { a || Q(a) }; { a, b || Q(a) }; { a || Q(a) }; { a, b || Q(a) }; { a, b || R(a, b) }; { a || Q(a) }; { a || ∀b.P (a, b) }; { a, b || R(a, b) }; { a || ∀b.P (a, b) }; A × B; A; π; P; ∃_{f}P; P; f^{∗}Q; ∃_{f}P; Q; f^{∗}Q; Q; f^{∗}Q; R; Q; ∀_{f}R; R; ∀_{f}R; A; B; f]

P ab  ∃b.P ab [figure] P ab Qa [figure] ∃b.P ab Qa [figure] [figure] [figure] Qa  Qa [figure] Qa Rab [figure]  Qa ∀b.Rab [figure] [figure] [figure] Rab  ∀b.Rab [figure] a, b  a [figure]  P ab  b=b′∧P abb [figure] P ab Qabb [figure] b=b′∧P abb Qabb′ [figure] [figure] [figure] Qabb  Qabb′ [figure] Qabb Rab [figure]  Qabb′ b=b′ [figure]Rab [figure] [figure] [figure] Rab  b=b′ [figure]Rab [figure] a, b  a, b, b′ [figure]  P a  ∃a.a=fb∧P a [figure] P a Qfa [figure]  ∃a.a=fb∧P a Qb [figure] [figure] [figure] Qfa  Qb [figure] Qfa Ra [figure]  Qb ∀a.a=fb [figure]P a [figure] [figure] [figure] Ra  ∀a.a=fb [figure]P a [figure] a  b_{f}  [figure]

Semantics for ND in Pred(Set): quantifiers

[figure: P′xy; ∃y.P′xy; P xy; ∃y.P ab; Qx; Qx; Q′x; Q′x; Rxy; ∀y.Rxy; R′xy; ∀y.R′xy; P′xy; P xy; ∃y.P′xy; ∃y.P ab; ∃_{π}; P xy; ∃y′.P xy′; η_{∃π}; P xy; Qx; ∃y.P ab; Qx; ∃_{π}^{♭}; ∃_{π}^{♯}; ∃y.Qx; Qx; ε_{∃π}; Qx; Q′x; Qx; Q′x; π^{∗}; ∀y′.Rxy′; Rxy; ε_{∀π}; Q′x; Rxy; Q′x; ∀y.Rxy; ∀_{π}^{♭}; ∀_{π}^{♯}; Qx; ∀y.Qx; η_{∀π}; Rxy; R′xy; ∀y.Rxy; ∀y.R′xy; ∀_{π}; x, y; x; π; {0000 \atop 0001}; 0001; {0001 \atop 0011}; 0011; {0111 \atop 0111}; 0111; {0001 \atop 0001}; 0001; {0011 \atop 0111}; 0011; {0111 \atop 1111}; 0111; {0000 \atop 0001}; {0001 \atop 0011}; 0001; 0011; {0001 \atop 0011}; {0011 \atop 0011}; {0001 \atop 0011}; {0111 \atop 0111}; 0011; 0111; 0111; 0111; {0111 \atop 0111}; {0001 \atop 0001}; 0111; 0001; {0011 \atop 0011}; {0011 \atop 0111}; {0001 \atop 0001}; {0011 \atop 0111}; 0001; 0011; 0001; 0001; {0011 \atop 0111}; {0111 \atop 1111}; 0011; 0111; x, y; x; π]

Rules for the quantifiers Now our task is to understand why, and in which sense, the adjoints to change-of-base that were just mentioned are “admissible”.

In Natural Deduction we have six rules: ∃I, ∃E, ∀I, ∀E, =I, =E (a package with all six will be called ‘∃∀=IE’) and some of them only started to make sense to me (years ago!) when I saw how to translate them to a sequent-calculus like form, and how to interpret sequents as inclusions between subsets — so we will see each of them in its ND form, in the corresponding SC form, and in a “set-like” form, involving functions, sets and subsets.

An important idea: any subtree of a derivation in natural deduction “has semantics”, i.e., can be interpreted as an inclusion between subsets.

The rules are:

\begin{matrix}{P aβ \atop ∃b.P ab} ∃I & \begin{matrix}∃b.P ab & [P ab]^{1} Qa ; ⋮ . ; Ra \\ Ra \end{matrix} ; ∃E \\ Qa ; ⋮ . ; Rab ; ∀b.Rab ∀I & \begin{aligned}β & ∀b.Rab \\ & Raβ \end{aligned} ∀E \\ b=b =I & \begin{matrix}b=b′ & P abb \\ P abb′ \end{matrix} =E \end{matrix}

but each of these (apparently) small trees packs a huge amount of information.

Rules for the quantifiers (2) Here are the translations...

\begin{matrix}{P aβ \atop ∃b.P ab} ∃I & \begin{matrix}∃b.P ab & [P ab]^{1} Qa ; ⋮ . ; Ra \\ Ra \end{matrix} ; ∃E \\ \begin{matrix}(a ↦ β) : A → B & \{ a, b || P ab \} \\ \{ a | P aβ \} ↪ \{ a | ∃b.P ab \} \end{matrix} ∃I & {\{ a, b | P ab ∧ Qa \} ↪ \{ a, b | Ra \} \atop \{ a | (∃b.P ab) ∧ Qa \} ↪ \{ a | Ra \}} ∃E \\ \begin{matrix}a ⊢ β & \{ a, b || P ab \} \\ a; P aβ ⊢ ∃b.P ab \end{matrix} ∃I & {a, b; P ab, Qa ⊢ Ra \atop a; ∃b.P ab, Qa ⊢ Ra} ∃E \\ Qa ; ⋮ . ; Rab ; ∀b.Rab ∀I & \begin{aligned}β & ∀b.Rab \\ & Raβ \end{aligned} ∀E \\ {\{ a, b | Qa \} ↪ \{ a, b | Rab \} \atop \{ a | Qa \} ↪ \{ a | ∀b.Rab \}} ∀I & \begin{matrix}(a ↦ β) : A → B & \{ a, b || Rab \} \\ \{ a | ∀b.Rab \} ↪ \{ a | Raβ \} \end{matrix} ∀E \\ {a, b; Qa ⊢ Rab \atop a; Qa ⊢ ∀b.Rab} ∀I & \begin{matrix}a ↦ β & \{ a, b || Rab \} \\ a; ∀b.Rab ⊢ Raβ \end{matrix} ∀E \\ b=b =I & \begin{matrix}b=b′ & P abb \\ P abb′ \end{matrix} =E \\ {B \atop \{ b | ⊤ \} ↪ \{ b | b=b \}} =I & {\{ a, b, b′ || P abb \} \atop \{ a, b, b′ | b=b′ ∧ P abb \} ↪ \{ a, b, b′ | P abb′ \}} =E \\ {B \atop b; ⊤ ⊢ b=b} =I & {\{ a, b, b′ || P abb′ \} \atop a, b, b′; b=b′, P abb ⊢ P abb′} =E \end{matrix}

Rules for equality The three primitive rules for equality in Natural Deduction are:

b=b =I  \begin{matrix}b=b′ & P abb \\ P abb′ \end{matrix} =E  \begin{matrix}P abb & [P abb′]^{1} ; ⋮ . ; Qabb′ \\ Qabb \end{matrix}subst; 1

The four derived rules below deserve proper names. Expensive ND systems come with them built-in, but in cheap ND system we have to build them ourselves.

b=b refl := b=b =I

{b=b′ \atop b′=b} sym := \begin{matrix}b=b′ & b=b =I \\ b′=b \end{matrix} ; =E

\begin{matrix}b=b′ & b′=b′′ \\ b=b′′ \end{matrix} trans := \begin{matrix}b′=b′′ & b=b′ \\ b=b′′ \end{matrix} =E

\begin{matrix}b=b′ & Qabb′ \\ Qabb \end{matrix} =E′ := \begin{aligned}Qabb′ & \begin{matrix}b=b′ & {[Qabb]^{1} \atop Qabb [figure]Qabb} 1 \\ Qabb′ [figure]Qabb \end{matrix} ; =E \\ & Qabb \end{aligned}

Adjoints to change-of-base: quantifiers

[figure: P′ab; ∃b.P′ab; P ab; ∃b.P ab; Qa; Qa; Rab; ∀b.Rab; R′ab; ∀b.R′ab; P′ab; P ab; p; ∃b.P′ab; ∃b.P ab; Σ_{π}p :=; _{(\begin{matrix}∃b.P′ab & {[P′ab]^{1} \atop ⋮ . p} ; P ab ; ∃b.P ab ∃I \\ ∃b.P ab \end{matrix} ; ∃E)}; P ab; Qa; g; P ab; Qa; =: f^{♯}; ∃b.P ab; Qa; g^{♭} :=; ∃b.P ab; Qa; f; _{(\begin{matrix}{P ab \atop ∃b.P ab} & ∃I \\ ⋮ . f \end{matrix} ; Qa)}; _{(\begin{matrix}∃b.P ab & {[P ab]^{1} \atop ⋮ . g} ; Qa \\ Qa \end{matrix} ; ∃E)}; Qa; Rab; =: k^{♭}; Qa; Rab; h; Qa; ∀b.Rab; k; Qa; ∀b.Rab; h^{♯} :=; _{(_{\begin{aligned}b & {Qa \atop ⋮ . k} ; ∀b.Rab \\ & Rab \end{aligned} ∀E})}; _{(_{{Qa \atop ⋮ . h} ; Rab ; ∀b.Rab ∀I})}; Rab; R′ab; r; ∀b.Rab; ∀b.R′ab; Π_{π}r :=; _{(\begin{matrix}\begin{aligned}b & ∀b.Rab \\ & Rab \end{aligned} & ∀E \\ ⋮ . r \end{matrix} ; R′ab ; ∀b.R′ab ; ∀I)}; a, b; a; π]

Adjoints to change-of-base: equality

P′ab  b=b′∧P′ab [figure] P ab  b=b′∧P ab [figure] Qabb  Qabb′ [figure] Rab  b=b′ [figure]Rab [figure] R′ab  b=b′ [figure]R′ab [figure] P′ab P ab_{p} [figure]  b=b′∧P′ab b=b′∧P ab_{Σ_{δ}p :=} [figure] [figure]  _{(\begin{matrix}{b=b′∧P′ab \atop b=b′} & {b=b′∧P′ab \atop P′ab} ; ⋮ . p ; P ab \\ b=b′∧P ab \end{matrix})} P ab Qabb_{g} [figure] P ab Qabb_{=: f^{♯}} [figure]  b=b′∧P ab Qabb′_{g^{♭} :=} [figure] b=b′∧P ab Qabb′_{f} [figure] [figure] [figure]_{(\begin{matrix}b=b∧P ab & {[b=b′∧P ab]^{1} \atop ⋮ . f} ; Qabb′ \\ Qabb \end{matrix} ; subst; 1)}  _{(\begin{matrix}{b=b′∧P ab \atop b=b′} & {b=b′∧P ab \atop P ab} ; ⋮ . g ; Qabb \\ Qabb′ \end{matrix} ; =E)} Qabb Rab_{=: k^{♭}} [figure] Qabb Rab_{h} [figure]  Qabb′ b=b′ [figure]Rab_{k} [figure] Qabb′ b=b′ [figure]Rab_{h^{♯} :=} [figure] [figure] [figure]_{(\begin{matrix}b=b =I & \begin{matrix}Qabb & {[Qabb′]^{1} \atop ⋮ . k} ; b=b′ [figure]Rab \\ b=b [figure]Rab \end{matrix} subst; 1 \\ & Rab \end{matrix})}  _{(\begin{matrix}\begin{matrix}[b=b′]^{1} & Qabb′ \\ Qabb \end{matrix} & =E′ \\ ⋮ . h \end{matrix} ; Rab ; b=b′ [figure]Rab ; 1)} Rab R′ab_{r} [figure]  b=b′ [figure]Rab b=b′ [figure]R′ab_{Π_{δ}r :=} [figure] [figure]  _{(\begin{aligned}[b=b′]^{1} & b=b′ [figure]Rab \\ & Rab \end{aligned} ; ⋮ . r ; R′ab ; b=b′ [figure]R′ab ; 1)} a, b  a, b, b′_{δ}  [figure]

Adjoints to change-of-base: generic

P′x  ∃x.tx=y∧P′x [figure] P x  ∃x.tx=y∧P x [figure] Qtx  Qy [figure] Rx  ∀x.tx=y [figure]Rx [figure] R′x  ∀x.tx=y [figure]R′x [figure] P′x P x_{p} [figure]  ∃x.tx=y∧P′x ∃x.tx=y∧P x_{Σ_{f} p :=} [figure] [figure]  _{(\begin{matrix}tx=y∧P′x & \begin{matrix}{[tx=y∧P′x]^{1} \atop tx=y} & {[tx=y∧P′x]^{1} \atop P′x} ; ⋮ . p ; P x \\ tx=y∧P x \end{matrix} ; ∃x.tx=y∧P x ; ∃I \\ ∃x.tx=y∧P x \end{matrix} ; ∃E)} P x Qtx_{g} [figure] P x Qtx_{=: f^{♯}} [figure]  ∃x.tx=y∧P x Qy_{g^{♭} :=} [figure] ∃x.tx=y∧P x Qy_{f} [figure] [figure] [figure]_{(\begin{matrix}\begin{matrix}{⊤ \atop ⋮ . t^{∗}refl} ; tx=tx & P x \\ tx=tx∧P x \end{matrix} & \begin{matrix}{[tx=y∧P x]^{1} \atop ∃x.tx=y∧P x} & ∃I \\ ⋮ . f \end{matrix} ; Qy \\ Qtx \end{matrix} subst; 1)}  _{(\begin{aligned}∃x.tx=y∧P x & \begin{matrix}{[tx=y∧P x]^{1} \atop tx=y} & {[tx=y∧P x]^{1} \atop P x} ; ⋮ . g ; Qtx \\ Qy \end{matrix} \\ & Qy \end{aligned} ; ∃E; 1)} Qtx Rx_{=: k^{♭}} [figure] Qtx Rx_{h} [figure]  Qy ∀x.tx=y [figure]Rx_{k} [figure] Qy ∀x.tx=y [figure]Rx_{h^{♯} :=} [figure] [figure] [figure]_{(\begin{matrix}{⊤ \atop ⋮ . t^{∗}refl} ; tx=tx & \begin{aligned}x & {Qfx \atop ⋮ . t^{∗}k} ; ∀x′.tx′=tx [figure]Rx \\ & tx=tx [figure]Rx \end{aligned} ∀E \\ & Rx \end{matrix})}  _{(\begin{matrix}\begin{matrix}{[tx=y]^{1} \atop y=tx} sym & Qy \\ Qtx \end{matrix} & ^{sub′} \\ ⋮ . h \end{matrix} ; Rx ; tx=y [figure]Rx ; 1 ; ∀x.tx=y [figure]Rx ; ∀I)} Rx R′x_{r} [figure]  ∀x.tx=y [figure]Rx ∀x.tx=y [figure]R′x_{Π_{f} r :=} [figure] [figure]  _{(\begin{aligned}[tx=y]^{1} & \begin{aligned}x & ∀x.tx=y [figure]Rx \\ & tx=y [figure]Rx \end{aligned} ∀E \\ & Rx \end{aligned} ; ⋮ . r ; R′x ; tx=y [figure]R′x ; 1 ; ∀x.tx=y [figure]R′x ; ∀I)} x  y_{δ}  [figure]

Adjoints to change-of-base: candidates Remember that: Δ_{B} := ⟨id_{B}, id_{B}⟩ : B → B × B, δ_{AB} := ⟨id_{A×B}, π′_{AB}⟩ : A × B → (A × B) × B.

If f : A → B and P ∈ 𝔼_{A} then we can define ∃_{f}P := ∃_{π_{BA}}((id_{B} × f)^{∗} Eq_{Δ_{B}}⊤_{B} ∧ π_{BA}^{′∗}P):

\begin{matrix}\begin{matrix}{A →^{f} B \atop B × A → B × B} & {B \atop \{ b, b′ || b=b′ \}} \\ \{ b, a || b=fa \} \end{matrix} & {\{ a || P a \} \atop \{ b, a || P a \}} \\ \{ b, a || b=fa∧P a \} \end{matrix} \{ b || ∃a.b=fa∧P a \}

{f \atop id_{B} × f} {B \atop Eq_{Δ_{B}}⊤_{B}}
(id_{B} × f)^{∗} Eq_{Δ_{B}}⊤_{B}

{P \atop π_{BA}^{′∗}P}

(id_{B} × f)^{∗} Eq_{Δ_{B}}⊤_{B}∧π_{BA}^{′∗}P
∃_{π_{BA}}((id_{B} × f)^{∗} Eq_{Δ_{B}}⊤_{B}∧π_{BA}^{′∗}P)

If P ∈ 𝔼_{A×B} then we can define Eq_{δ_{AB}} P := (π′_{AB} × id_{B})^{∗} Eq_{Δ_{B}}⊤_{B} ∧ π_{(A×B)B}^{∗}P:

{B \atop \{ b, b′ || b=b′ \}} ; \{ (a, b), b′ || b=b′ \} {\{ a, b || P ab \} \atop \{ (a, b), b′ || P ab \}} \{ (a, b), b′ || b=b′∧P ab \}

{B \atop Eq_{Δ_{B}}⊤_{B}}

(π′_{AB} × id_{B})^{∗} Eq_{Δ_{B}}⊤_{B}

{P \atop π_{(A×B)B}^{∗}P}

(π′_{AB} × id_{B})^{∗} Eq_{Δ_{B}}⊤_{B}∧π_{(A×B)B}^{∗}P Preservation of ‘and’

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

\begin{matrix}\begin{matrix}f & P & Q \\ f^{∗}(P ∧Q) ⊢ f^{∗}P ∧f^{∗}Q \end{matrix} P∧^{♮} & := & \begin{matrix}\begin{matrix}f & \begin{matrix}P & Q \\ P ∧Q ⊢ P \end{matrix} π \\ f^{∗}(P ∧Q) ⊢ f^{∗}P \end{matrix}·^{∗} & \begin{matrix}\begin{matrix}P & Q \\ P ∧Q ⊢ Q \end{matrix} & π′ \\ f^{∗}(P ∧Q) ⊢ f^{∗}Q \end{matrix} ·^{∗} \\ f^{∗}(P ∧Q) ⊢ f^{∗}P ∧f^{∗}Q \end{matrix} ; ⟨, ⟩ \\ \begin{matrix}f & P & Q \\ f^{∗}P ∧f^{∗}Q ⊢ f^{∗}(P ∧Q) \end{matrix} & P∧ \end{matrix}

Preservation of ‘and’ (2) In the archetypal model, CanSub(Set), the arrows P∧^{♮} and P∧ exist for trivial reasons: f^{∗}P ∧ f^{∗}Q = { a || P fa ∧ Qfa } = { a || P (f(a)) ∧ Q(f(a)) } and f^{∗}(P ∧ Q) = { a || P fa ∧ Qfa } = { a || P (f(a)) ∧ Q(f(a)) } are the same subobject.

[figure: { a || P fa }; { b || P b }; { a || P fa }; { a || P fa∧Qfa }; { a || P fa }; { a || P fa∧Qfa }; { b || P b }; { b || P b∧Qb }; { a || P fa∧Qfa }; { a || P fa∧Qfa }; ♮; { a || P fa∧Qfa }; { a || P fa∧Qfa }; P∧; { a || P fa∧Qfa }; { b || P b∧Qb }; { a || P fa∧Qfa }; { a || P fa }; { a || P fa∧Qfa }; { a || P fa }; { b || P b∧Qb }; { b || Qb }; { a || P fa }; { b || Qb }; A; B; f]

The same will happen for P⊤ and P [figure], and for some forms of Frob, BCCL and BCCR (the details for Frob, BCCL and BCCR are in [Seely83])

Preservation of ‘true’

[figure: f^{∗}⊤_{B}; ⊤_{B}; f^{∗}⊤_{B}; ⊤_{A}; P⊤^{♮}; f^{∗}⊤_{B}; ⊤_{A}; P⊤; A; B; f]

\begin{matrix}{f : A → B \atop f^{∗}⊤_{B} ⊢ ⊤_{A}} P⊤^{♮} & := & \begin{matrix}f & {B \atop ⊤_{B}} ⊤ \\ f^{∗}⊤_{B} \end{matrix} ; ·^{∗} ; f^{∗}⊤_{B} ⊢ ⊤_{A} ! \\ {f : A → B \atop ⊤_{A} ⊢ f^{∗}⊤_{B}} & P⊤ \end{matrix}

Preservation of ‘implies’

f^{∗}(Q [figure]R) ∧ f^{∗}Q  f^{∗}((Q [figure]R) ∧ Q) [figure]^{♮} f^{∗}(Q [figure]R) ∧ f^{∗}Q  f^{∗}((Q [figure]R) ∧ Q)_{P∧} [figure] f^{∗}((Q [figure]R) ∧ Q)  (Q [figure]R) ∧ Q [figure] f^{∗}(Q [figure]R) ∧ f^{∗}Q f^{∗}R [figure]  f^{∗}((Q [figure]R) ∧ Q) f^{∗}R [figure] [figure]  (Q [figure]R) ∧ Q R[figure] f^{∗}R  R [figure] f^{∗}(Q [figure]R) ∧ f^{∗}Q  f^{∗}(Q [figure]R) [figure] [figure] f^{∗}R  f^{∗}Q [figure]f^{∗}R [figure] [figure]  (Q [figure]R) ∧ Q  Q [figure]R [figure] [figure] R  Q [figure]R [figure] [figure] f^{∗}(Q [figure]R)  Q [figure]R [figure]  Q [figure]R Q [figure]R_{id} [figure] f^{∗}(Q [figure]R) f^{∗}Q [figure]f^{∗}R_{♮} [figure] f^{∗}(Q [figure]R) f^{∗}Q [figure]f^{∗}R [figure]_{P [figure]} [figure] [figure] [figure]  [figure] [figure] A  B_{f}  [figure]

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

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

f^{∗}(Q [figure]R)∧f^{∗}Q ⊢ f^{∗}R ;

f^{∗}(Q [figure]R) ⊢ f^{∗}Q [figure]f^{∗}R cur

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

Beck-Chevalley for the left adjoint

[figure: f^{′∗}P; P; f^{′∗}P; c^{′∗}f^{∗}∃_{c}P; f^{′∗}P; f^{′∗}c^{∗}∃_{c}P; P; c^{∗}∃_{c}P; c^{′∗}f^{∗}∃_{c}P; f^{′∗}c^{∗}∃_{c}P; f^{′∗}c^{∗}∃_{c}P; c^{∗}∃_{c}P; f^{′∗}P; ∃_{c′}f^{′∗}P; P; ∃_{c}P; c^{′∗}f^{∗}∃_{c}P; f^{∗}∃_{c}P; c^{∗}∃_{c}P; ∃_{c}P; f^{∗}∃_{c}P; ∃_{c}P; ∃_{c}P; ∃_{c}P; id; ∃_{c′}f^{′∗}P; f^{∗}∃_{c}P; ♮; ∃_{c′}f^{′∗}P; f^{∗}∃_{c}P; BCCL; A ×_{B} C; C; f′; A ×_{B} C; A; c′; C; B; c; A; B; f]

\begin{matrix}c & f & c′ & f′ & P \\ ∃_{c′}f^{′∗}P ⊢ f^{∗}∃_{c}P \end{matrix} ^{BCCL^{♮}} := \begin{matrix}\begin{matrix}\begin{matrix}f′ & \begin{matrix}\begin{matrix}\begin{matrix}P & c \\ ∃_{c}P \end{matrix} & ∃_{0} \\ ∃_{c}P ⊢ ∃_{c}P \end{matrix} & id \\ P ⊢ c^{∗}∃_{c}P \end{matrix} ; ∃^{♯} \\ f^{′∗}P ⊢ f^{′∗}c^{∗}∃_{c}P \end{matrix} ; ·^{∗} & \begin{matrix}(f′; c)=(c′; f) & ∃_{c}P \\ f^{′∗}c^{∗}∃_{c}P ⊢ c^{′∗}f^{∗}∃_{c}P \end{matrix} \\ f^{′∗}P ⊢ c^{′∗}f^{∗}∃_{c}P \end{matrix} & ; \\ ∃_{c′}f^{′∗}P ⊢ f^{∗}∃_{c}P \end{matrix} ; ∃^{♭}
\begin{matrix}c & f & c′ & f′ & P \\ f^{∗}∃_{c}P ⊢ ∃_{c′}f^{′∗}P \end{matrix} BCCL

Beck-Chevalley for the right adjoint

[figure: c^{′∗}f^{∗}∀_{c}P; f^{′∗}c^{∗}∀_{c}P; f^{′∗}c^{∗}∀_{c}P; c^{∗}∀_{c}P; c^{′∗}f^{∗}∀_{c}P; f^{′∗}P; f^{′∗}c^{∗}∀_{c}P; f^{′∗}P; c^{∗}∀_{c}P; P; f^{′∗}P; P; c^{′∗}f^{∗}∀_{c}P; f^{∗}∀_{c}P; f^{′∗}P; ∀_{c′}f^{′∗}P; c^{∗}∀_{c}P; ∀_{c}P; P; ∀_{c}P; f^{∗}∀_{c}P; ∀_{c}P; ∀_{c}P; ∀_{c}P; id; f^{∗}∀_{c}P; ∀_{c′}f^{′∗}P; ♮; f^{∗}∀_{c}P; ∀_{c′}f^{′∗}P; BCCR; A ×_{B} C; C; f′; A ×_{B} C; A; c′; C; B; c; A; B; f]

\begin{matrix}c & f & c′ & f′ & P \\ f^{∗}∀_{c}P ⊢ ∀_{c′}f^{′∗}P \end{matrix} ^{BCCR^{♮}} := \begin{matrix}\begin{matrix}(f′; c)=(c′; f) & ∀_{c}P \\ c^{′∗}f^{∗}∀_{c}P ⊢ f^{′∗}c^{∗}∀_{c}P \end{matrix} & \begin{matrix}f′ & \begin{matrix}\begin{matrix}\begin{matrix}P & c \\ ∀_{c}P \end{matrix} & ∀_{0} \\ ∀_{c}P ⊢ ∀_{c}P \end{matrix} & id \\ c^{∗}∀_{c}P ⊢ P \end{matrix} ; ∀^{♭} \\ f^{′∗}c^{∗}∀_{c}P ⊢ f^{′∗}P \end{matrix} ; ·^{∗} \\ c^{′∗}f^{∗}∀_{c}P ⊢ f^{′∗}P \end{matrix} ; ; ; f^{∗}∀_{c}P ⊢ ∀_{c′}f^{′∗}P ; ∀^{♯}
\begin{matrix}c & f & c′ & f′ & P \\ ∀_{c′}f^{′∗}P ⊢ f^{∗}∀_{c}P \end{matrix} BCCR

Frobenius

[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]

\begin{matrix}f & P & Q \\ ∃_{f}(P ∧f^{∗}Q) ⊢ (∃_{f}P)∧Q \end{matrix} ^{Frob^{♮}} := \begin{matrix}\begin{matrix}\begin{matrix}P & \begin{matrix}f & Q \\ f^{∗}Q \end{matrix} ·^{∗} \\ P ∧f^{∗}Q ⊢ P \end{matrix} ; π & f \\ ∃_{f}(P ∧f^{∗}Q) ⊢ ∃_{f}P \end{matrix} ∃_{f} & \begin{matrix}\begin{matrix}P & \begin{matrix}f & Q \\ f^{∗}Q \end{matrix} ·^{∗} \\ P ∧f^{∗}Q ⊢ f^{∗}Q \end{matrix} & π′ \\ ∃_{f}(P ∧f^{∗}Q) ⊢ Q \end{matrix} ; ^{∃_{f}^{♭}} \\ ∃_{f}(P ∧f^{∗}Q) ⊢ (∃_{f}P)∧Q \end{matrix} ; ⟨, ⟩
\begin{matrix}f & P & Q \\ ∃_{f}(P ∧f^{∗}Q) ⊢ (∃_{f}P)∧Q \end{matrix} Frob

Cheap hyperdoctrines A cheap hyperdoctrine is a structure like this:

ℍ = (𝔹, ×, 1, →, 𝔼, ∧, ⊤, [figure], p, cleavage, P∧, P⊤, P [figure], ∃_{π} ⊣ π∗ ⊣ ∀_{p}, Eq_{Δ} ⊣ Δ^{∗}, BCC∃_{π}, BCC∀_{π})

Note that Frob does not appear, and that BCCL and BCCR are stated only for very special cases — BCC∃, BCC∀, BCC= (details soon!)

Pimp implies Frob Fact: we can reconstruct Frob from P [figure]. (Note: this is a yellow-belt categorical proof, but for some reason I find it difficult) First we need a derived rule:

{∃_{f}(P ∧f^{∗}Q) ⊢ R \atop ∃_{f}P ∧Q ⊢ R} P [figure]′ := \begin{matrix}{∃_{f}(P ∧f^{∗}Q) ⊢ R \atop P ∧f^{∗}Q ⊢ f^{∗}R} & ∃^{♯} \\ P ⊢ f^{∗}Q [figure]f^{∗}R \end{matrix} ; [figure: ♯] ; P ⊢ f^{∗}(Q [figure]R) ; ; P [figure] ; ∃_{f}P ⊢ Q [figure]R ; ∃^{♭} ; ∃_{f}P ∧Q ⊢ R ; [figure: ♭]

where ‘; P [figure]’ is composition with ‘P [figure]’, as below. Note that all the bars in the derivation at the right above are bijections; the inverse of ‘; P [figure]’ is ‘; P [figure]^{♮}’.

{P ⊢ f^{∗}Q [figure]f^{∗}R \atop P ⊢ f^{∗}(Q [figure]R)} ; P [figure] := \begin{matrix}P ⊢ f^{∗}Q [figure]f^{∗}R & \begin{matrix}f & Q & R \\ f^{∗}Q [figure]f^{∗}R ⊢ f^{∗}(Q [figure]R) \end{matrix} P [figure] \\ P ⊢ f^{∗}(Q [figure]R) \end{matrix} ; ;

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

Now make R := ∃_{f}(P ∧ f^{∗}Q). We get the tree at the right, below, that becomes our definition of Frob as a derived rule (involving P [figure]).

\begin{matrix}f & P & Q \\ ∃_{f}P ∧Q ⊢ ∃_{f}(P ∧f^{∗}Q) \end{matrix} Frob := \begin{matrix}\begin{matrix}f & P & Q \\ ∃_{f}(P ∧f^{∗}Q) \end{matrix} ; ∃_{f}(P ∧f^{∗}Q) ⊢ ∃_{f}(P ∧f^{∗}Q) & id \\ ∃_{f}P ∧Q ⊢ ∃_{f}(P ∧f^{∗}Q) \end{matrix} ; P [figure]′

Pimp implies Frob (2)

Here is the construction as a diagram. We start with R := ∃_{f}(P ∧ f^{∗}Q) and with the arrow marked ‘(id)’, and we build the arrow ∃_{f}P ∧ Q ⊢ R = ∃_{f}(P ∧ f^{∗}Q), that is ‘Frob’.

∃_{f}P ∧Q  ∃_{f}P [figure] ∃_{f}P ∧Q ∃_{f}(P ∧f^{∗}Q)_{Frob} [figure] ∃_{f}P ∧Q ∃_{f}(P ∧f^{∗}Q) [figure]_{♮} ∃_{f}P ∧Q  R [figure] [figure]  ∃_{f}P  Q [figure]R [figure] [figure] ∃_{f}(P ∧f^{∗}Q)  R_{(id)} [figure] R  Q [figure]R [figure] ∃_{f}(P ∧f^{∗}Q) P ∧f^{∗}Q [figure]  ∃_{f}P P[figure] R f^{∗}R [figure]  Q [figure]R f^{∗}(Q [figure]R) [figure] P ∧f^{∗}Q  P [figure]  P  f^{∗}(Q [figure]R) [figure] P ∧f^{∗}Q  f^{∗}R [figure] [figure]  P  f^{∗}Q [figure]f^{∗}R [figure] [figure] f^{∗}(Q [figure]R) f^{∗}Q [figure]f^{∗}R_{♮} [figure] f^{∗}(Q [figure]R) f^{∗}Q [figure]f^{∗}R [figure]_{P [figure]} f^{∗}R  f^{∗}Q [figure]f^{∗}R [figure] [figure][figure: ♭] [figure: ♯] [figure] [figure]_{∃^{♭}}  _{∃^{♯}} [figure]  [figure]_{∃^{♭}}  _{∃^{♯}} [figure] [figure][figure: ♭] [figure: ♯] [figure]

Pimp implies Frob (3) In the notation of [Lawvere70] (p.6), this is stated and proved as:

Definition-Theorem. In any eed, the following are equivalent:

(1) Frobenius Reciprocity holds,

(2) For any f : X → Y, α, ψ in P (Y) f · (α ⇒ ψ) [figure: ≈] f · α ⇒ f · ψ

(3) For any f : X → Y, ψ ∈ P (X), α ∈ P (Y) ((f · α) ∧ φ)Σf [figure: ≈] α ∧ (φΣf)

Proof. The second conditions means that the diagram of functors (**) commutes up to natural equivalence. Hence replacing each functor by its left adjoint also yields a diagram which commutes up to canonical natural equivalence: (*). But the latter is just the third condition. Conversely if the third condition holds, we can replace the functors in the latter diagram by their right adjoints, yielding the second condition.

α∧φΣf  φΣf [figure] α∧φΣf ((f · α)∧φ)Σf_{Frob} [figure] α∧φΣf ((f · α)∧φ)Σf [figure]_{♮} α∧φΣf  ψ [figure] [figure]  φΣf  α ⇒ ψ [figure] [figure] ((f · α)∧φ)Σf  ψ_{(id)} [figure] ψ  α ⇒ ψ [figure] ((f · α)∧φ)Σf (f · α)∧φ [figure]  φΣf φ[figure] ψ f · ψ [figure]  α ⇒ ψ f · (α ⇒ ψ) [figure] (f · α)∧φ  φ [figure]  φ  f · (α ⇒ ψ) [figure] (f · α)∧φ  f · ψ [figure] [figure]  φ  f · α ⇒ f · ψ [figure] [figure] f · (α ⇒ ψ) f · α ⇒ f · ψ_{♮} [figure] f · (α ⇒ ψ) f · α ⇒ f · ψ [figure]_{P [figure]} f · ψ  f · α ⇒ f · ψ [figure] [figure]_{⇒^{♭}}_{⇒^{♯}} [figure] [figure]_{Σ^{♭}}  _{Σ^{♯}} [figure]  [figure]_{Σ^{♭}}  _{Σ^{♯}} [figure] [figure]_{⇒^{♭}}_{⇒^{♯}} [figure]  [figure: P (Y); P (Y); α∧( ); P (Y); P (X); ( )Σf; P (Y); P (X); ( )Σf; P (X); P (X); (f·α)∧( ); (∗); P (Y); P (Y); α⇒( ); P (Y); P (X); f·( ); P (Y); P (X); f·( ); P (X); P (X); (f·α)⇒( ); (∗∗)]

Note that he only draws the squares (*) and (**), with the categories and the functors; the cube with objects, morphisms, and ‘↦’s for functors is a kind of “internal view” of the categories and functors involved — and such “internal views” are only very rarely drawn in the (standard?) Category Theory literature.

BCCL implies BCCR Also, BCCL implies BCCR (and vice-versa), by an argument similar to the previous one. Here are the diagrams; we won’t get into the details.

[figure: X; Y; a; X; Z; l; Y; W; r; Z; W; b; Q; l^{∗}Q; l^{∗}Q; ∀_{a}l^{∗}Q; Q; ∀_{b}Q; ∀_{b}Q; r^{∗}∀_{b}Q; P; a^{∗}P; a^{∗}P; ∃_{l}a^{∗}P; P; ∃_{r}P; ∃_{r}P; b^{∗}∃_{r}P; a^{∗}P; l^{∗}Q; P; ∀_{a}l^{∗}Q; (id); b^{∗}∃_{r}P; Q; ∃_{r}P; ∀_{b}Q; P; r^{∗}∀_{b}Q; ∃_{l}a^{∗}P; Q; ∃_{l}a^{∗}P; b^{∗}∃_{r}P; ♮; ∃_{l}a^{∗}P; b^{∗}∃_{r}P; BCCL; ∀_{a}l^{∗}Q; r^{∗}∀_{b}Q; BCCR; ∀_{a}l^{∗}Q; r^{∗}∀_{b}Q; ♮; ∀^{♯}; ∀^{♭}; ∃^{♭}; ∃^{♯}; ∃^{♭}; ∃^{♯}; ∀^{♯}; ∀^{♭}]

Lemmas about equality

[figure: P; Σ_{f}P; P ∧ f^{∗}Q; P; Σ_{f}(P ∧ f^{∗}Q); Σ_{f}P; Σ_{f}P ∧ Q; Σ_{f}P; P ∧ f^{∗}Q; Σ_{f}(P ∧ f^{∗}Q); Σ_{f}(P ∧ f^{∗}Q); Σ_{f}P ∧ Q; P ∧ f^{∗}Q; f^{∗}Q; Σ_{f}(P ∧ f^{∗}Q); Q; Σ_{f}P ∧ Q; Q; f^{∗}Q; Q; A; B; f; P; Σ_{f}P; P ∧ R; P; Σ_{f}(P ∧ R); Σ_{f}P; Σ_{f}P ∧ R; Σ_{f}P; P ∧ R; Σ_{f}(P ∧ R); Σ_{f}(P ∧ R); Σ_{f}P ∧ R; P ∧ R; R; Σ_{f}(P ∧ R); g^{∗}R; Σ_{f}P ∧ R; g^{∗}R; R; g^{∗}R; g^{∗}R; R; A; B; f; B; A; g; A; A; id; ⊤; Σ_{f}⊤; f^{∗}Q; ⊤; Σ_{f}f^{∗}Q; Σ_{f}⊤; Σ_{f}⊤ ∧ Q; Σ_{f}⊤; f^{∗}Q; Σ_{f}f^{∗}Q; Σ_{f}f^{∗}Q; Σ_{f}⊤ ∧ Q; f^{∗}Q; f^{∗}Q; Σ_{f}f^{∗}Q; Q; Σ_{f}⊤ ∧ Q; Q; f^{∗}Q; Q; A; B; f; ⊤; Σ_{f}⊤; R; ⊤; Σ_{f}R; Σ_{f}⊤; Σ_{f}⊤ ∧ R; Σ_{f}⊤; R; Σ_{f}R; Σ_{f}R; Σ_{f}⊤ ∧ R; R; R; Σ_{f}R; g^{∗}R; Σ_{f}⊤ ∧ R; g^{∗}R; R; g^{∗}R; g^{∗}R; R; A; B; f; B; A; g; A; A; id; ⊤; Σ_{f}⊤; f^{∗}Q; ⊤; Σ_{f}f^{∗}Q; Σ_{f}⊤; Σ_{f}⊤ ∧ g^{∗}f^{∗}Q; Σ_{f}⊤; f^{∗}Q; Σ_{f}f^{∗}Q; Σ_{f}f^{∗}Q; Σ_{f}⊤ ∧ g^{∗}f^{∗}Q; f^{∗}Q; f^{∗}Q; Σ_{f}f^{∗}Q; g^{∗}f^{∗}Q; Σ_{f}⊤ ∧ g^{∗}f^{∗}Q; g^{∗}f^{∗}Q; f^{∗}Q; g^{∗}f^{∗}Q; g^{∗}f^{∗}Q; f^{∗}Q; A; B; f; B; A; g; A; A; id]

[figure: Frob0; Frob1; \begin{matrix}Q := g^{∗}R \\ f^{∗}g^{∗}R :≅ R \end{matrix}; Frob0; Frob2; \begin{matrix}P := ⊤ \\ ⊤ ∧ f^{∗}Q :≅ f^{∗}Q \end{matrix}; Frob1; Frob3; \begin{matrix}P := ⊤ \\ ⊤ ∧ f^{∗}Q :≅ f^{∗}Q \end{matrix}; Frob2; Frob3; \begin{matrix}Q := g^{∗}R \\ f^{∗}g^{∗}R :≅ R \end{matrix}; Frob3; Frob5; \begin{matrix}R := f^{∗}Q \\ f^{∗}g^{∗}f^{∗}Q :≅ f^{∗}Q \end{matrix}]

λ-calculus in a hyperdoctrine As the base category 𝔹 of a hyperdoctrine is a CCC we can interpret λ-calculus in it. In diagrams:

[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; uncur g; A × B; C; f; A; B→C; g; A; B→C; cur f; C; B→C]

[figure: A; B; a⊢b; A; B×C; a⊢⟨b,c⟩; A; C; a⊢c; B; B×C; p⊢πb; B×C; C; p⊢πb′; 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]

In a sequent-calculus-like form:

\begin{matrix}B & C \\ B × C \end{matrix} ×_{0} \begin{matrix}a ⊢ b & a ⊢ c \\ a ⊢ ⟨b, c⟩ \end{matrix} ⟨, ⟩  \begin{matrix}B & C \\ p ⊢ πp \end{matrix} π  \begin{matrix}B & C \\ p ⊢ π′p \end{matrix} π′

1 1  {A \atop a ⊢ ∗} !

\begin{matrix}B & C \\ B→C \end{matrix} ^{→^{0}}  \begin{matrix}B & C \\ b, f ⊢ fb \end{matrix} app {a, b ⊢ c \atop a ⊢ λb:B.c} cur

In natural deduction form (in downcased notation):

\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

Propositional calculus in a hyperdoctrine As each fiber 𝔼_{B} of a hyperdoctrine is a CCC we can interpret propositional calculus in it. In diagrams:

P Q [figure] [figure]P Q∧R [figure] P  R [figure] [figure] Q  Q∧R [figure] Q∧R  R [figure]  P ⊤_{B} [figure]  P ∧Q  P [figure] P ∧Q R[figure] P ∧Q R[figure]  P Q [figure]R [figure] P Q [figure]R [figure] [figure] [figure] R  Q [figure]R [figure]

In a sequent-calculus-like form:

\begin{matrix}Q & R \\ Q∧R \end{matrix} ∧ \begin{matrix}P ⊢ Q & P ⊢ R \\ P ⊢ Q∧R \end{matrix} ∧I \begin{matrix}Q & R \\ Q∧R ⊢ Q \end{matrix} ∧E_{1} \begin{matrix}Q & R \\ Q∧R ⊢ R \end{matrix} ∧E_{2}

⊤_{B} 1  {P \atop P ⊢ ⊤_{B}} ⊤I

\begin{matrix}Q & R \\ Q [figure]R \end{matrix} [figure] \begin{matrix}Q & R \\ (Q [figure]R)∧Q ⊢ R \end{matrix} ev {P, Q ⊢ R \atop P ⊢ Q [figure]R} [figure]I

In natural deduction form (in downcased notation):

\begin{matrix}P ; .. . ; Q & P ; .. . ; R \\ Q∧R \end{matrix} ∧I  {Q∧R \atop Q} ∧E_{1}  {Q∧R \atop R} ∧E_{2}

{P \atop ⊤_{B}} ⊤I

\begin{aligned}P ; .. . ; Q & P ; .. . ; Q [figure]R \\ & R \end{aligned} [figure]E P [Q]^{1} ; .. . ; R ; Q [figure]R [figure]I; 1

Interpreting ‘∀I’ in a hyperdoctrine

[figure: {π^{∗}Q ⊢ R \atop Q ⊢ ∀_{π}R} ∀I; _{Qa ; .. . ; Rab ; ∀b.Rab ∀I}; _{{a, b; Qa ⊢ Rab \atop a; Qa ⊢ ∀b.Rab} ∀I}; π^{∗}Q; Q; π^{∗}Q; R; Q; ∀_{π}R; R; ∀_{π}R; A×B; A; π; Qa; Qa; Qa; Rab; Qa; ∀b.Rab; Rab; ∀b.Rab; a, b; a; π]

Interpreting ‘∀E’ in a hyperdoctrine

[figure: \begin{matrix}f & Q ⊢ ∀_{π}R \\ Q ⊢ ⟨id, f⟩^{∗}R \end{matrix} ∀E; _{\begin{matrix}a ⊢ b′ & Qa ; .. . ; ∀b.Rab \\ Rab′ \end{matrix} ∀E}; _{\begin{matrix}a ⊢ b′ & a; Qa ⊢ ∀b.Rab \\ a; Qa ⊢ Rab′ \end{matrix} ∀E}; Q; ⟨id, f⟩^{∗}π^{∗}Q; ⟨id, f⟩^{∗}π^{∗}Q; π^{∗}Q; π^{∗}Q; Q; ⟨id, f⟩^{∗}π^{∗}Q; ⟨id, f⟩^{∗}R; π^{∗}Q; R; Q; ∀_{π}R; ⟨id, f⟩^{∗}R; R; R; ∀_{π}R; A; A × B; ⟨id,f⟩; A × B; A; π; A; A; id; Qa; Qa; Qa; Qa; Qa; Qa; Qa; Rab′; Qa; Rab; Qa; ∀b.Rab; Rab′; Rab; Rab; ∀b.Rab; a; a, b; ⟨id,f⟩; a, b; a; π; a; a; id]

Interpreting ‘∃I’ in a hyperdoctrine

[figure: {P ∧π^{∗}Q ⊢ π^{∗}R \atop ∃_{π}P ∧Q ⊢ R} ∃E; _{{P ab′ \atop ∃b.P ab} ∃I}; _{\begin{matrix}a ⊢ b′ & \{ a, b || P ab \} \\ a; P ab′ ⊢ ∃b.P ab \end{matrix} ∃I}; ⟨id, f⟩^{∗}P; P; P; ∃_{π}P; ⟨id, f⟩^{∗}P; ⟨id, f⟩^{∗}π^{∗}∃_{π}P; P; π^{∗}∃_{π}P; ∃_{π}P; ∃_{π}P; id; ⟨id, f⟩^{∗}π^{∗}∃_{π}P; π^{∗}∃_{π}P; π^{∗}∃_{π}P; ∃_{π}P; A; A×B; ⟨id,f⟩; A×B; A; π; A; A; id; P ab′; P ab; P ab; ∃b.P ab; P ab′; ∃b.P ab; P ab; ∃b.P ab; ∃b.P ab; ∃b.P ab; id; ∃b.P ab; ∃b.P ab; ∃b.P ab; ∃b.P ab; a; a, b; ⟨id,f⟩; a, b; a; π; a; a; id]

Interpreting ‘∃E’ in a hyperdoctrine

P ∧π^{∗}Q π^{∗}R [figure]  ∃_{π}P ∧Q R[figure] π^{∗}R  R [figure] P ∧π^{∗}Q  P [figure] [figure] π^{∗}R  π^{∗}Q [figure]π^{∗}R [figure] [figure]  ∃_{π}P ∧Q  ∃_{π}P [figure] [figure] R  Q [figure]R [figure] [figure] P  ∃_{π}P [figure]  ∃_{π}P Q [figure]R [figure] π^{∗}(Q [figure]R)  Q [figure]R [figure] P π^{∗}Q [figure]π^{∗}R [figure] P  π^{∗}(Q [figure]R) [figure] [figure] π^{∗}Q [figure]π^{∗}R  π^{∗}(Q [figure]R) [figure]_{♮} π^{∗}Q [figure]π^{∗}R  π^{∗}(Q [figure]R)_{P [figure]}[figure]  [figure] [figure] [figure]  [figure] [figure] A × B  A_{π}  [figure]

P ab∧Qa Ra [figure]  (∃b.P ab)∧Qa Ra [figure] Ra  Ra [figure] P ab∧Qa  P ab [figure] [figure] Ra  Qa [figure]Ra [figure] [figure]  (∃b.P ab)∧Qa ∃b.P ab [figure] [figure] Ra  Qa [figure]Ra [figure] [figure] P ab  ∃b.P ab [figure]  ∃b.P ab Qa [figure]Ra [figure] Qa [figure]Ra  Qa [figure]Ra [figure] P ab Qa [figure]Ra [figure] P ab  Qa [figure]Ra [figure] [figure] Qa [figure]Ra  Qa [figure]Ra [figure] _{♮} Qa [figure]Ra  Qa [figure]Ra_{P [figure]} [figure]  [figure] [figure] [figure]  [figure] [figure] a, b  a [figure]

\begin{matrix}{P ∧π^{∗}Q ⊢ π^{∗}R \atop ∃_{π}P ∧Q ⊢ R} & ∃E \\ \begin{matrix}∃b.P ab & [P ab]^{1} Qa ; .. . ; Ra \\ Ra \end{matrix} ; ∃E; 1 & {a, b; P ab, Qa ⊢ Ra \atop a; ∃b.P ab, Qa ⊢ Ra} ∃E \end{matrix}

Equality types: Hofmann 1995 A diagram for the rules Id-Intro and Id-Elim-J as they appear in Martin Hofmann’s PhD thesis (p.21): (Note: my the diagram is for a slightly weaker Id-Elim-J... in the rule the type τ may depend on the value of p)

[figure: 1; Id_{σ}(x, y); 1; τ[y : =x]; a⃗,x,y;p⊢M; Id_{σ}(x, y); τ; a⃗,x,y;p⊢J_{σ,τ} (M,x,y,p); τ[y : =x]; τ; Σ^{♭}; Id_{σ}(N_{1}, N_{2}); Id_{σ}(x, y); Id_{σ}(N_{1}, N_{2}); τ[x := N1][y := N2][p := P]; (Id-Elim-J) a⃗⊢J_{σ,τ} (M,N_{1},N_{2},P); Id_{σ}(x, y); τ; Id_{σ}(x, y); τ; a⃗,x,y;p⊢J_{σ,τ} (M,x,y,p); τ[x := N1][y := N2][p := P]; τ; ∗; 1; 1; 1; Id_{σ}(x, y); 1; Id_{σ}(M, M); (Id-Intro) a⃗⊢Refl_{σ}(M); 1; Id_{σ}(x, x); Id_{σ}(x, y); Id_{σ}(x, y); a⃗,x,y;p⊢p; Id_{σ}(M, M); Id_{σ}(x, x); Id_{σ}(x, x); Id_{σ}(x, y); ∗; Σ^{♯}; (a⃗:Γ, x:σ); (a⃗:Γ, x:σ, y:σ); y:=x; (a⃗:Γ); (a⃗:Γ, x:σ, y:σ); x:=N_{1},y:=N_{2}; (a⃗:Γ); (a⃗:Γ, x:σ); x:=M; (a⃗:Γ, x:σ); (a⃗:Γ, x:σ, y:σ); y:=x]

PL categories The paper [Seely87] (“Categorical Semantics for Higher Order Polymorphic Lambda Calculus”), shows how to interpret polymorphic λ-calculus in a hyperdoctrine with a universal object. Its rules (ΣI), (ΣE), (ΠI), (ΠE) correspond (very roughly) to our (∀I), (∀E), (∃I), (∃E), and are stated as this in the paper (in the section (1.1.4)):

(ΣI) If α is an indeterminate of order A, σ ∈ Ω, τ ∈ A, then I_{Σα·σ,τ} ∈ σ[τ/α] [figure]Σα ∈ A · σ. When clear from the context, we shall denote this term by I_{τ}, or even by I; in particular, if b ∈ σ[τ/α], then I(b) ∈ Σα ∈ A · σ.

(ΣE) If a ∈ σ [figure]ρ, α an indeterminate of order A which is not free in ρ nor in the type of any free variable in a, then Vα ∈ A · a ∈ (Σα ∈ A · σ) [figure]ρ.

(ΠI) If a ∈ σ, α an indeterminate of order A which is not free in the type of any free variable in a, then Λα ∈ A · a ∈ Πα ∈ A · σ.

(ΠE) If a ∈ Πα ∈ A · a, τ ∈ A, then a{τ} ∈ σ[τ/α], where σ[τ/aa is σ with τ replacing α.

In a diagram:

[figure: σ; Σα∈A.σ; σ; ρ; a; Σα∈A.σ; ρ; Vα∈A.a (ΣE); ρ; ρ; Σ^{♭}; σ[τ/α]; σ; σ; Σα∈A.σ; σ[τ/α]; Σα∈A.σ; (ΣI) I_{Σα.σ,τ}; σ; Σα∈A.σ; Σα∈A.σ; Σα∈A.σ; id; Σα∈A.σ; Σα∈A.σ; Σα∈A.σ; Σα∈A.σ; Σ^{♯}; ρ; ρ; ρ; ρ; ρ; σ[τ/α]; (ΠE) α{τ}; ρ; σ; a; ρ; Πα∈A.σ; a; ρ; Πα∈A.σ; Λα∈A.a (ΠI); σ[τ/α]; σ; σ; Πα∈A.σ; Π^{♭}; Π^{♯}; B; B×A; b ⊢⟨b,τ⟩; B×A; B; π]

PL categories (2) Here is a Rosetta stone for translating between the paper’s notation and the (“standard”) notation for hyperdoctrines that we use here. In the middle rectangle the iso ⟨id, τ⟩^{∗}π^{∗}∃_{π}P ↔ ∃_{π}P has been collapsed — we show only the object ∃_{π}P.

[figure: σ; Σα∈A.σ; σ; ρ; a; Σα∈A.σ; ρ; Vα∈A.a (ΣE); ρ; ρ; Σ^{♭}; σ[τ/α]; σ; σ; Σα∈A.σ; σ[τ/α]; Σα∈A.σ; (ΣI) I_{Σα.σ,τ}; σ; Σα∈A.σ; Σα∈A.σ; Σα∈A.σ; id; Σα∈A.σ; Σα∈A.σ; Σα∈A.σ; Σα∈A.σ; Σ^{♯}; ρ; ρ; ρ; ρ; ρ; σ[τ/α]; (ΠE) α{τ}; ρ; σ; a; ρ; Πα∈A.σ; a; ρ; Πα∈A.σ; Λα∈A.a (ΠI); σ[τ/α]; σ; σ; Πα∈A.σ; Π^{♭}; Π^{♯}; B; B×A; b ⊢⟨b,τ⟩; B×A; B; π]

[figure: P; ∃_{π}P; P; π^{∗}Q; g; ∃_{π}P; Q; g^{♭}; π^{∗}Q; Q; ∃_{π}^{♭}; ⟨id, τ⟩^{∗}P; P; P; ∃_{π}P; ⟨id, τ⟩^{∗}P; ∃_{π}P; ⟨id,τ⟩^{∗}η_{P}; P; π^{∗}∃_{π}P; η_{P}; ∃_{π}P; ∃_{π}P; id; ∃_{π}P; π^{∗}∃_{π}P; π^{∗}∃_{π}P; ∃_{π}P; ∃^{♯}; Q; π^{∗}Q; π^{∗}Q; Q; Q; ⟨id, τ⟩^{∗}R; ⟨id,τ⟩^{∗}k^{♭}; π^{∗}Q; R; k^{♭}; π^{∗}Q; R; h; Q; ∀_{π}R; k; Q; ∀_{π}R; h^{♯}; ⟨id, τ⟩^{∗}R; R; R; ∀_{π}R; Π^{♭}; Π^{♯}; B; B×A; ⟨id,τ⟩; B×A; B; π]

Uppercasing names When I defined a (proto-)cleavage, several slides ago, I said that it was:

[figure: P; R; h′; P; Q; f′; Q; R; g′; A; C; h; A; B; f; B; C; g; p]

cleavage ≡ B, C, R, g ↦ Q, g′, (A, P, f ↦ f′)

Let’s formalize this.

A (proto-)cleavage (for a projection functor p : 𝔼 → 𝔹) is anything that “deserves the name” B, C, R, g ↦ Q, g′, (A, P, f ↦ f′) that is, a cleavage for p : 𝔼 → 𝔹 is any object of a certain type — where that type is the uppercasing of B, C, R, g ↦ Q, g′, (A, P, f ↦ f′).

How do we uppercase names as complex as that? How do we extract the necessary “hints” from the accompanying diagrams? Can this always be done unambiguosly?

Uppercasing names (2) Let’s start with a simpler problem. We have a set A and families of sets

a:A ⊢ B_{a}
a:A, b:B_{a} ⊢ C_{ab}
a:A, b:B_{a}, c:C_{ab} ⊢ D_{abc}

a:A, b:B_{a}, c:C_{ab}, d:D_{abc} ⊢ E_{abcd}

and we want to find the type — written in standard notation for λ-calculus with dependent types (i.e., with ‘Σ’s and ‘Π’s) — of:

a, b, c ⊢ d, e.

A convention: ‘E[α]’ will mean “the space of ‘α’s”. We will add lots of ‘E[…]’ entries to our dictionary to keep track of the types.

Remember:

\begin{matrix}(a, b) : Σa:A.B_{a} \\ (a ↦ b) : Πa:A.B_{a} \end{matrix}

So:

E[a] ≡ A
E[b] ≡ B_{a}  (← which depends on a)
E[a, b] ≡ Σa:E[a].E[b] ≡ Σa:A.B_{a}
E[a ↦ b] ≡ Πa:E[a].E[b] ≡ Πa:A.B_{a}

Uppercasing names (3) We want to uppercase

a, b, c ↦ d, e.

We start by adding the missing parentheses:

(a, (b, c)) ↦ (d, e)

Then:

E[a, (b, c)] ≡ Σa:E[a].(Σb:E[b].E[c])
≡ Σa:A.(Σb:B_{a}.C_{ab})
≡ Σa:A.Σb:B_{a}.C_{ab}
E[d, e] ≡ Σd:E[d].E[e]
≡ Σd:D_{abc}.E_{abcd}
E[(a, (b, c)) ↦ (d, e)] ≡ Π(a, (b, c)):E[a, (b, c)].E[d, e]
≡ Π(a, (b, c)):(Σa:A.Σb:B_{a}.C_{ab}).(Σd:D_{abc}.E_{abcd})
≡ Πt:(Σa:A.Σb:B_{a}.C_{ab}).((Σd:D_{abc}.E_{abcd}) [ \begin{matrix}a:=πt, \\ b:=ππ′t, \\ c:=π′π′t \end{matrix} ])

where the ‘[…]’ on the last line is a substitution box, and:

(Σd:D_{abc}.E_{abcd}) [ \begin{matrix}a:=πt, \\ b:=ππ′t, \\ c:=π′π′t \end{matrix} ] = Σd:D_{(πt)(ππ′t)(π′π′t)}.E_{(πt)(ππ′t)(π′π′t)d}

when we use then name ‘a, (b, c)’ for ‘t’ then it is obvious that:

\begin{aligned}⟨⟨a⟩⟩ & := & π⟨⟨a, (b, c)⟩⟩ \\ ⟨⟨b, c⟩⟩ & := & π′⟨⟨a, (b, c)⟩⟩ \\ ⟨⟨b⟩⟩ & := & π⟨⟨b, c⟩⟩ \\ ⟨⟨c⟩⟩ & := & π′⟨⟨b, c⟩⟩ \end{aligned}

and so we can avoid choosing a name for the t ≡ a, (b, c), and we can omit the substitution box... Long names save the day! 8-)

Uppercasing names (4) To summarize:

⟨⟨E[a]⟩⟩ := A
⟨⟨E[b]⟩⟩ := B_{a}
⟨⟨E[c]⟩⟩ := C_{ab}
⟨⟨E[d]⟩⟩ := D_{abc}
⟨⟨E[e]⟩⟩ := E_{abcd}
⟨⟨a, (b, c)⟩⟩ := t
⟨⟨E[b, c]⟩⟩ := Σb:⟨⟨E[b]⟩⟩.⟨⟨E[c]⟩⟩
⟨⟨E[a, (b, c)]⟩⟩ := Σa:⟨⟨E[a]⟩⟩.⟨⟨E[b, c]⟩⟩
⟨⟨a⟩⟩ := π⟨⟨a, (b, c)⟩⟩
⟨⟨b, c⟩⟩ := π′⟨⟨a, (b, c)⟩⟩
⟨⟨b⟩⟩ := π⟨⟨b, c⟩⟩
⟨⟨c⟩⟩ := π′⟨⟨b, c⟩⟩
⟨⟨E[d, e]⟩⟩ := Σd:⟨⟨E[d]⟩⟩.⟨⟨E[e]⟩⟩
⟨⟨E[(a, (b, c)) ↦ (d, e)]⟩⟩ := Π⟨⟨a, (b, c)⟩⟩:⟨⟨E[a, (b, c)]⟩⟩.(⟨⟨E[d, e]⟩⟩ [ \begin{matrix}a:=⟨⟨a⟩⟩, \\ b:=⟨⟨b⟩⟩, \\ c:=⟨⟨c⟩⟩ \end{matrix} ])

New terminology: a thing like ⟨⟨a, b⟩⟩ — a long name within double angle brackets — is bracketed long name, or, for short, a blong name.

The dictionary treats blong names as macros. The dictionary above has two parts. In the top part we have the “terminals”. In the bottom part we have “(real) macros” (non-terminals).

The definition for ⟨⟨a, (b, c)⟩⟩ could have been omitted — the preprocessor would then substitute ⟨⟨a, (b, c)⟩⟩ by dnc006, which would be a perfectly acceptable name for a variable (in, say, Coq).

Currying long names There are natural bijections

[figure: (a, (b, c)) ↦ (d, e); f_{1}; a ↦ ((b, c) ↦ (d, e)); f_{2}; a ↦ (b ↦ (c ↦ (d, e))); f_{3}; (a, b) ↦ (c ↦ (d, e)); f_{4}; ((a, b), c) ↦ (d, e); f_{5}; (a, (b, c)) ↦ (d, e); a ↦ ((b, c) ↦ (d, e)); a ↦ ((b, c) ↦ (d, e)); a ↦ (b ↦ (c ↦ (d, e))); a ↦ (b ↦ (c ↦ (d, e))); (a, b) ↦ (c ↦ (d, e)); (a, b) ↦ (c ↦ (d, e)); ((a, b), c) ↦ (d, e)]

and usually when we are speaking with humans we can gloss over the details, and say just:

\begin{aligned}a & b & c & f \\ & d, e \end{aligned} apps

For f being any of the ‘f_{i}’s above.

f_{3} — the “totally curried” version of f — has the simplest type:

f_{3} : Πa:A_{a}.Πb:B_{a}.Πc:C_{ab}.Σd:D_{abc}.E_{abcd}

and the way to obtain d, e from a, b, c, f_{3} is the shortest:

\begin{aligned}(d, e) & = & f_{1} ⟨a, ⟨b, c⟩⟩ \\ (d, e) & = & f_{2} a ⟨b, c⟩ \\ (d, e) & = & f_{3} a b c \\ (d, e) & = & f_{4} ⟨a, b⟩ c \\ (d, e) & = & f_{5} ⟨⟨a, b⟩, c⟩ \end{aligned}

so the “totally curried versions” are usually preferred in implementations (where we cannot gloss over those details)...

Usually in mathematical practice we say Hom_{C}(A, B) (= Hom_{C}⟨A, B⟩) but in our implementation of (proto-)CT in type theory we will use Hom_{C} A B.

Typing proto-categories It should be possible to type

C ≡ (C_{0}, Hom_{C}, id_{C}, ∘_{C})

from the equations:

A, B, C : C_{0}
A → A := Hom_{C} A A : Sets
A → B := Hom_{C} A B : Sets
B → C := Hom_{C} B C
A → C := Hom_{C} A C
Hom_{C} : E[λA.λB. Hom_{C} A B]
id_{A} := id_{C}A : A → A
id_{C} : E[λA.id_{A}]
g ∘ f := ∘_{C} A B C g f : A → C
∘_{C} : E[λA.λB.λCλg.λf.(g ∘ f)]

And it should be possible to extract some of them from this diagram:

[figure: A; B; f; B; C; g; A; C; g∘f; A; ^{id^{A}}]

(Note: I’m ignoring all questions of size, and I’m not saying where C_{0} lives).

After that we should have a constant, E[C], that we can use to declare arbitrary (proto-)categories: a proto-category is an element of E[C].

The result should be something like:

E[C_{0}] := Classes
E[Hom_{C}] := C_{0} → (C_{0} → Sets)
E[id_{C}] := ΠA:C_{0}. Hom_{C} A A
E[∘_{C}] := ΠA:C_{0}.ΠB:C_{0}.ΠC:C_{0}.

(Hom_{C} B C → (Hom_{C} A B → Hom_{C} A C))

E[C] := E[C_{0}, Hom_{C}, id_{C}, ∘_{C}]

Introduction to Heyting Algebras Let’s identify ‘true’ with with 1 and with the singleton set, and ‘false’ with 0 and with the empty set. Now all our truth-values (i.e., 0 and 1) are subsets of a “top” set, ⊤, and we have an arrow 0 → 1, but there’s no arrow 1 → 0. The arrows are “non-decreasing”. In the category Set^{•••} we have 8 truth-values, and in the category Set^{𝕍} just five:

[figure: 0; 1; 000; 001; 000; 010; 000; 100; 001; 011; 001; 101; 010; 011; 010; 110; 100; 101; 100; 110; 011; 111; 101; 111; 110; 111; _{0 0 0}; _{0 0 1}; _{0 0 1}; _{1 0 1}; _{0 0 1}; _{0 1 1}; _{1 0 1}; 1 1 1; _{0 1 1}; 1 1 1; Set; _{Set_{•••}}; _{Set_{𝕍}}]

𝕍 is the DAG

𝕍 := (W, R) := ({ α, β, γ }, { α → γ, β → γ })

regarded as a category:

𝕍 ≡ [figure: α; γ; β; γ]

In each category Set^{𝔻}, where 𝔻 is a DAG, the structure (Sub(1_{𝔻}), ∧, ⊤, [figure]) is a CCC, and even more: (Sub(1_{𝔻}), ∧, ⊤, [figure], ∨, ⊥) a (bi-)Heyting Algebra. Its objects behave as intuitionistic truth-values... In Set^{𝕍}, if we take P =^{0}^{0} 1 we have ¬¬P = (P [figure]⊥) [figure]⊥ =^{1}^{1} 1 = ⊤, so P ≠ ¬¬P.

Introduction to Lawvere-Tierney Topologies The operation P ↦ P^{∗} := ¬¬P on a HA obeys these three rules:

⊢ ⊤^{∗}  {P ⊢ Q \atop P^{∗} ⊢ Q^{∗}}  P^{∗∗} ⊢ P^{∗}

Anything obeying these three rules [in the HA of a topos] is called a Lawvere-Tierney topology. These three rules are the cheap presentation, of course. The nicer equivalent expensive presentations for LT-topologies include how the ‘^{∗}’ interacts with ∧, ⊤, [figure], ∨, ⊥,

[figure: P ∧Q; P^{∗}∧Q; P ∧Q; P ∧Q^{∗}; P^{∗}∧Q; P^{∗}∧Q^{∗}; P ∧Q^{∗}; P^{∗}∧Q^{∗}; (P ∧Q)^{∗}; (P^{∗}∧Q)^{∗}; (P ∧Q)^{∗}; (P ∧Q^{∗})^{∗}; (P^{∗}∧Q)^{∗}; (P^{∗}∧Q^{∗})^{∗}; (P ∧Q^{∗})^{∗}; (P^{∗}∧Q^{∗})^{∗}; P ∧Q; (P ∧Q)^{∗}; P^{∗}∧Q; (P^{∗}∧Q)^{∗}; P ∧Q^{∗}; (P ∧Q^{∗})^{∗}; P^{∗}∧Q^{∗}; (P^{∗}∧Q^{∗})^{∗}; 0 0 1; _{1 0 1}; 0 0 1; 0 1 1; _{1 0 1}; _{1 1 1}; 0 1 1; _{1 1 1}; _{1 1 1}; _{1 1 1}; _{1 1 1}; _{1 1 1}; _{1 1 1}; _{1 1 1}; _{1 1 1}; _{1 1 1}; 0 0 1; _{1 1 1}; _{1 0 1}; _{1 1 1}; 0 1 1; _{1 1 1}; _{1 1 1}; _{1 1 1}]

[figure: P ∨ Q; P^{∗} ∨ Q; P ∨ Q; P ∨ Q^{∗}; P^{∗} ∨ Q; P^{∗} ∨ Q^{∗}; P ∨ Q^{∗}; P^{∗} ∨ Q^{∗}; (P ∨ Q)^{∗}; (P^{∗} ∨ Q)^{∗}; (P ∨ Q)^{∗}; (P ∨ Q^{∗})^{∗}; (P^{∗} ∨ Q)^{∗}; (P^{∗} ∨ Q^{∗})^{∗}; (P ∨ Q^{∗})^{∗}; (P^{∗} ∨ Q^{∗})^{∗}; P ∨ Q; (P ∨ Q)^{∗}; P^{∗} ∨ Q; (P^{∗} ∨ Q)^{∗}; P ∨ Q^{∗}; (P ∨ Q^{∗})^{∗}; P^{∗} ∨ Q^{∗}; (P^{∗} ∨ Q^{∗})^{∗}; 0 0 0 1 1; _{0 0 1 1 1}; 0 0 0 1 1; 0 1 0 1 1; _{0 0 1 1 1}; _{0 1 1 1 1}; 0 1 0 1 1; _{0 1 1 1 1}; _{1 1 1 1 1}; _{1 1 1 1 1}; _{1 1 1 1 1}; _{1 1 1 1 1}; _{1 1 1 1 1}; _{1 1 1 1 1}; _{1 1 1 1 1}; _{1 1 1 1 1}; 0 0 0 1 1; _{1 1 1 1 1}; _{0 0 1 1 1}; _{1 1 1 1 1}; 0 1 0 1 1; _{1 1 1 1 1}; _{0 1 1 1 1}; _{1 1 1 1 1}]

P [figure]Q P^{∗} [figure]Q [figure] P [figure]Q  P [figure]Q^{∗} [figure] P^{∗} [figure]Q  P^{∗} [figure]Q^{∗} [figure]P [figure]Q^{∗} P^{∗} [figure]Q^{∗} (P [figure]Q)^{∗} (P^{∗} [figure]Q)^{∗} [figure] (P [figure]Q)^{∗}  (P [figure]Q^{∗})^{∗} [figure] (P^{∗} [figure]Q)^{∗}  (P^{∗} [figure]Q^{∗})^{∗} [figure](P [figure]Q^{∗})^{∗} (P^{∗} [figure]Q^{∗})^{∗} P [figure]Q (P [figure]Q)^{∗} [figure] [figure] P^{∗} [figure]Q(P^{∗} [figure]Q)^{∗} [figure] [figure]  P [figure]Q^{∗}(P [figure]Q^{∗})^{∗} [figure] P^{∗} [figure]Q^{∗} (P^{∗} [figure]Q^{∗})^{∗} [figure]  ^{0}^{1}_{0}_{1}_{0 0 0 0} [figure]^{0}^{1}_{0}_{1}  ^{1}^{1}_{1}_{1} [figure]_{0 0 0 0}  _{1 1 1 1} [figure]^{1}^{1}_{1}_{1}_{1 1 1 1}_{0 1 1 1}_{0 0 1 1} [figure]_{0 1 1 1}  _{1 1 1 1} [figure]_{0 0 1 1}  _{1 1 1 1} [figure]_{1 1 1 1}_{1 1 1 1}^{0}^{1}_{0}_{1}  _{0 1 1 1} [figure] [figure]_{0 0 0 0}  _{0 0 1 1} [figure] [figure]  ^{1}^{1}_{1}_{1}  _{1 1 1 1} [figure]_{1 1 1 1}  _{1 1 1 1} [figure]

Introduction to Lawvere-Tierney Topologies (2) ...plus how the ‘^{∗}’ interacts with ∀ and ∃, plus the notions of ^{∗}-sheaf and sheafification, among lots of other things. With just a little bit more we get forcing and geometric maps between toposes.

This all looks very technical, and it is. However toposes of the form Set^{𝔻}, where 𝔻 is a small DAG, seem to be archetypal, in a sense...

Map of the world This is the map of the “obvious” places where my work can be presented.

CT journals CompSci journals Alg journals

Logic journals

{CT \atop books} CS/TT books Alg books

Logic books

international conferences (papers)

national conferences (papers)

international conferences (tutorial) national conferences (tutorial)

proof assistants

math seminars PUC/IMPA/ UFRJ/etc math seminars at UFF

local comspci seminars local CT seminars local algebra seminars

local logic seminars

local CompScis local categor- ists local algebra- ists local logic- ians

local topolog- ists

grad students iniciação científica undergrads

However it makes more sense to use it to connect these “places” than to think of it as belonging to one or a few of them in particular... For example, it can be used to discuss, in local seminar with non-CT-ists, how CT and Type Theory texts are written, and how to approach them.

There are no (new) theorems in these slides ...because the things that we usually call “theorems” in Category Theory belong to the real world — they are a construction plus something more.

Take for example the Yoneda Lemma. It says that given a functor R : B → Set and an object B of B we have a bijection between the set RB and the set of natural transformations C →^{.} ((B → C) → RC). Here we are working in the syntactical world only

— we mention liftings to the real world, but we don’t do any such liftings explicitly, and so what we get is just the projection of that bijection, which is a proto-iso between RB and the set of proto-NTs C →^{.} ((B → C) → RC). Usually a “theorem” involving a such construction would have to either show that it is always a bijection, or to show a case where it is not a bijection.

What we do have here is the definition of the two worlds (mostly via examples, but whatever...), of the projections, of the liftings, some ideas of how to work with this splitting of worlds, and examples.

This is not the kind of work that usually gets published.

Typing proto-adjunctions Hom_{C} : =A, B ↦ (A → B) id_{C} : =A ↦ id_{A} ∘_{C} : =A, B, C, f, g ↦ h C : =(C_{0}, Hom_{C}, id_{C}, ∘_{C}) F_{0} : =A ↦ F A F_{1} : =A, B, f ↦ F f F : =(F_{0}, F_{1}) T_{0} : =A ↦ T_{A} T : =(T_{0}) ♭_{AB} : =g ↦ f ♯_{AB} : =f ↦ g ♭ : =A, B ↦ ♭_{AB} ♯ : =A, B ↦ ♯_{AB} η : =A ↦ η_{A} ϵ : =B ↦ ϵ_{B} (L ⊣ R) : =(♭, ♯, η, ϵ)

Typing proto-CCCs

prod^{♮} : =A, h ⊢ f, g prod : =A, f, g ↦ h B × C : =(P, π, π′, prod) ×_{0} : =B, C ↦ B × C ×_{1} : =B, C, B′, C′, β, γ ↦ β × γ × : =(×_{0}, ×_{1})

! : =A ↦ t 1 : =(T,!)

uncur_{BC} : =A, g ↦ f cur_{BC} : =A, f ↦ g B→C : =E, ev_{BC}, cur_{BC} →_{0}: =B, C ↦ B→C

(×B)_{0} : =A ↦ A × B (×B)_{1} : =A′, A, α ↦ α × B (B→)_{0} : =C ↦ (B→C) (B→)_{1} : =C, C′, γ ↦ (B→γ) uncur_{B} : =A, C, g ↦ f cur_{B} : =A, C, f ↦ g (×B) : =((×B)_{0}, (×B)_{1}) (B→) : =((B→)_{0}, (B→)_{1}) η_{B} : =A ↦ coev_{AB} ϵ_{B} : =C ↦ ev_{BC} ((×B) ⊣ (B→)) : =(uncur_{B}, cur_{B}, η_{B}, ϵ_{B}) → : =B ↦ (B→), ((×B) ⊣ (B→))

(C, ×, 1, →)

Typing proto-fibrations

𝔹 : =(𝔹_{0}, Hom_{𝔹}, id_{𝔹}, ∘_{𝔹}) 𝔼_{0} : =B ↦ 𝔼_{B0} Hom_{𝔼} : =A, B, f, P, Q ↦ Hom_{𝔼}(P, Q, f) id_{𝔼} : =A, P ↦ id_{P} ∘_{𝔼} : =A, B, C, f, g, P, Q, R, f′, g′ ↦ h′ 𝔼 : =(𝔼_{0}, Hom_{𝔼}, id_{𝔼}, ∘_{𝔼})

ulift_{h′g′} : =f ↦ f′ cart_{g′} : =A, h, P, h′ ↦ ulift_{h′g′} \overline{g}_{0} : =R ↦ Q, g′, cart_{g′} cleavage : =B, C, g ↦ \overline{g}_{0}