David Corfield Ox Notes

Categorical logic built up over more than 50 years. Many moments when.

Computer science. Mundane things like database queries.

HoTT is a sweet spot.

Type, dependent type, homotopy type, and a modal variety.

If you don’t understand adjunctions, you don’t understand logic.

Type formation. Modalities.

Propositional, First-order logic, modal logic: But why?

Useful way to understand the perspective via judgement structure. First-order logic can be specified in this way, and when you do so.

A mathematical example of intricate dependency.

$k:Field, V:FinVec(k), f: Endo_k(V) \vdash Ev(f,V,k) : SubVec_k(V)$

$p: Person, c: Child(m), s: PoliteSpeak(c,p) \vdash Praise(p,c,s): Type$ $p: Person, c: Child(m), s: PoliteSpeak(c,p) \vdash f(p,c,s): Praise(p,c,s)$

Anyone whose child speaks politely to them praises them for it. If someone’s child speaks politely to them, they praise them for it.

Foundations, justification, organisation basic ideas.

Sets as set theory, and as category of structureless structure.

Vast field of categorical logic which flourishes in computer science departments.

Philosophical logic – mathematical logic (set theory, proof theory) – categorical logic – category theory.

• Only allow one mode, so no modality (DTT);
• Only allow one level of dependency (FOL)
• Allow no dependency (Simple) (or dependency on singleton)
• Only allow one premise (Unary)
• Force dependent types to be propositions
• Force all types to be propositions
• Only allow one non-dependent type

So ordinary FOL is a restriction to a system which is uni-moded, one non-dependent type forced to be set, and dependent types which are forced to be propositions.

No variables for P(x).

Type formation all given by adjoints.

• Product of types – tuples of domain, conjunction
• Constant (variable) element of type – constant (variable) in domain
• Element of function type – n-ary function on domain.
• Dependent type–proposition and relations
• Dependent product - universal quantification
• Dependent sum - subset of domain, truncates to existential quantification
• Identity type - equality relation
• Object classifier - proposition classifier HOL

Standard modal logic is based on one mode. Just see endomap on single node.

Mathematics, homotopification.

HoTT - term model as initial elementary $\infty$-topos. Synthetic homotopy theory is unthinkable via ZFC.

Philosophy training, propositional logic, untyped FOL, modal logic, perhaps set theory (if interested in philosophy of maths).

Untyped FOL is a restricted kind of logic.

Set theory

If you start out with DTT, and limit it.

Someone driving a car with a speed-inhibitor fitted who’d like to go faster, so straps on an external engine.

Just use the car.

Perhaps you want a limited system for a reason.

soundness and completeness theorem is proved for DFOL.

Euclidean Riemannian Cartan geometry.

Dependent product as adjoint

Hom_{\mathcal{C}}(A, \prod_{x:B} C(x)) \equiv Hom_{\mathcal{C}/A}(A \times B, C(x))

One person’s generalisation is another person’s lack of imposed conditions.

There’s a logical system which when dramatically restricted yields the standard first-order logic that we teach our philosophy students.

Because of these restrictions expressive power is restored by .

This system blurs the distinction between logic and mathematics.

Sets and propositions are treated even-handedly. Applied mathematics is no more and no less mysterious than applied logic.

The system has types. Dependent types. Judgement structure.

Type constructors by adjoints.

Group of people as domain. Someone loves everyone, everyone is loved by someone.

List of people of at least seniority X, with training in Y and Z.

Modal HoTT.

Some of us call ourselves algebraic topologists, but this has the unhelpful effect of making the subject appear to be an area of topology, which I think is profoundly inaccurate. It so happens that one way (and historically the first way) to model homotopical thinking is to employ a very particular class of topological spaces. Today, the praxis of homotopy theory interacts with topology no more often than it does with arithmetic geometry and category theory, and the interactions with areas like representation theory are growing rapidly. Homotopy theory is not a branch of topology.

I think of homotopy theory as an enrichment of the notion of equality, dedicated to the primacy of structure over properties. Simplistic and abstract though this idea is, it leads rapidly to a whole universe of nontrivial structures.

Do we see homotopy in the world? Set and equivalence relation. Books and position.

Problem: ML didn’t devise TT with the real world in mind. No more difficulty than applying first-order logic to the world. Database theorists suggest this.

If HoTT is a logic, then applied mathematics becomes the same problem as applied propositional or first-order logic.

Illustrate with states of affairs.

As soon as we start working in an untyped universe, we begin to organize it in different ways for different purposes. Types arise informally in any domain to categorize objects according to their usage and behavior. The classification of objects in terms of the purposes for which they are used eventually results in a more or less well-defined type system. Types arise naturally, even starting from untyped universes. Cardelli Wegner 1985, On Understanding Types, Data Abstraction, and Polymorphism 473

I have never seen any serious proposals for a vernacular based on set theory. Or to put it another way, as soon as we start expanding and transforming set theory to fit the requirements for V, we end up with a theoretical framework that looks a lot like type theory