How are the parts of category theory which make explicit reference to Set different when formalized in a proof assistant that is based on type theory

Question

In category theory a presheaf is defined as a functor whose target is $\mathrm{Set}$, and the concept is used to state the Yoneda lemma. The appearance of $\mathrm{Set}$ in the definition comes from the assumption that hom-sets are sets.

But proof languages that are based on type theory don't necessarily have any built-in definition of what a set is (in the sense of sets in a specific foundation like ZFC, for example, which comes with all sorts of theorems about sets like the fact that uncountable sets exist, which may be false about types or not even possible to state in type theory).

So how, then, are these types of theorems such as the Yoneda lemma formalized in a type theory based proof assistant, in practice, if they can't make reference to $\mathrm{Set}$?

• Is the category of sets simply replaced by some category of types? If so does this create any significant difference between how category theory in a proof assistant works compared to how category theory normally works?
• Is set theory formulated in the proof assistant and then the definitions of stuff in category theory can refer to it?
• Is some kind of type theory magic used to do category theory in the "internal logic" of a category of categories or whatever? (I don't know what "internal logic" means, I just know that it is a thing that exists and it seems like it might apply here.)

Answer 1

The question is not limited to category theory. We can ask more generally how to formalize in type theory those parts of mathematics where it matters that we use sets. To give an example, one can do a lot of basic group theory without really worrying whether the carrier is a set, a topological space, or a sheaf.

The most naive approach to formalization of mathematics is simply to use types as if they were sets, which often works well. When it does break down, the trouble can almost always be traced to the fact that types have a more intricate notion of equality than sets: equality on a set $S$ is a relation, whreas equality on a type $T$ is a structure, called the identity type on $T$. Therefore, when sets are really required, we can:

1. Restrict only to those types for which the identity type is a relation. These types go under different names: sets, h-sets, homotopy sets, 0-types. I prefer “sets”.

2. Use a type theory in which all types are sets. There are again several ways to achieve this:

   • use extensional type theory whose equality reflection rule forces all identity types to be relations
   • use intensional type theory with the axiom K, which has the same effect on identity types
   • postulate the global axiom of choice, which entails axiom K, as well as excluded middle.

The first option is more refined but technically more complicated, as one has to navigate the intricacies of homotopy type theory. The second one, especially assuming axiom K or choice, is like killing a fly with a nuclear bomb. You get a wasteland without any flies.

Answer 2

You can work through all the proofs referring to $\mathsf{Set}$ and see what assumptions they made. For example, if you're simply trying to define a presheaf, then any category will do, because a $\mathcal C$-valued presheaf is nothing but a (contravariant) functor with codomain in $\mathcal C$.

Now the presheaf category inherits a lot of properties from the original category. For example, if $\mathcal C$ is complete, then so is $\mathsf{Psh}_{\mathcal C}(\mathcal D)$. Since $\mathsf{Set}$ is complete, you can regard this as the general version of the statement "Presheaf categories are complete." Of course you need to pay some attention when you define completeness. Because when you define a limit, you need a diagram, which is a small category. So it depends on how you define small categories.

Take another example, when you need to prove the Yoneda lemma, the actual dependency on $\mathsf{Set}$ is that $\mathrm{hom}$ takes values in $\mathsf{Set}$. In other words, the Yoneda lemma works in a $\mathsf{Set}$-enriched category. Therefore, a $\mathcal{C}$-valued $\mathcal{C}$-enriched presheaf will satisfy the Yoneda lemma.

Answer 3

Here is a partial answer for how Lean 3 handles it, but you probably want to wait for a person in Lean with more knowledge of the category theory library to confirm that my understanding is fully accurate.

Here is the Yoneda lemma in Lean's mathlib. In particular the documenation says

The Yoneda lemma asserts that that the Yoneda pairing (X : Cᵒᵖ, F : Cᵒᵖ ⥤ Type) ↦ (yoneda.obj (unop X) ⟶ F) is naturally isomorphic to the evaluation (X, F) ↦ F.obj X.

As you can see (if I understand correctly), the type Type is used in place of the category Set to refer to the presheafs Cᵒᵖ ⥤ Type. This might seem weird (and I'm not an expert), but let me explain.

The first thing to keep in mind is that in Lean types behave as sets. Informally, I mean that equality of objects in a Lean type is nothing special. If a=b then there is only one way for them to be equal. This can be made formal with homotopy type theory, via a formal definition of what it means for a type to be a "set" (or h-set ). So from a category theory standpoint, in Lean, the type Type plays the same role as the category Set of small sets.

Second, Type is not technically a category, but it is a Type universe which is itself a type in the universe Type 1. This is a common situation in Lean, just as the type real of real numbers is not a topological space, but just a type. So how do we give Type it's canonical categorical structure (just like we give Real its canonical topological space structure)? We do this through type classes. So when Lean sees Cᵒᵖ ⥤ Type (the functors from Cᵒᵖ to Type) it looks up the instance of the category typeclass for Type to turn Type into a category. I didn't trace though exact the route it does this, but I'm sure it is the usual category structure of Set, i.e. the morphisms from A: Type to B: Type are exactly the elements of the "hom" type A -> B in Lean (which again is an element of Type in Lean, and that is the requirement of the Yoneda lemma as stated in Trebor’s answer).

Third, you asked about internal logic. I'm not great with this either, but my loose intuition is that the logic of Lean when restricted to types in Type is the internal logic of the category Set (and when you add the sort Prop of propositions then you get the internal logic of the topos Set). So normal math in Lean uses category theoretical ideas implicitly and internally. But since Lean has universes, you can explicitly refer to Type externally as an object of a higher universe Type 1, and you can explicitly talk about the categorical structure of Type as well. That is exactly what the mathlib category theory library does, especially its formulation of the Yoneda lemma.

Last, I've only talked about Lean which has built in that all types are sets. I imagine if working in HoTT or cubical type theory in Adga, Coq, or Arend, that you can do the same thing, but in that case, one doesn't use the type Type of all small types, but instead the type of all small h-sets (or maybe its truncation to an h-set to prevent it from becoming a higher category). Indeed in the HoTT book there is a type Set of small sets and it plays the same role as the category of Set. The HoTT version of the Yoneda lemma is Theorem 9.5.4 in the book (and I don't think it requires that Set satisfies the axiom of choice). Also, here is the Agda Yoneda lemma which appears to use the category of setoids.

For higher order logic, which is another type theoretic foundation used in HOL Light and Isabelle/HOL, there are not universes, so I think one can't show the category Set exists. Anyway, here is the Yoneda Lemma in Isabelle's Archive of Formal Proofs, but I'll leave it up to someone else to explain how it works.

You can find more about the Lean category theory library by reading the documentation for the Lean category theory library, watching the videos for Lean for the Curious Mathematician 2020 (or LFTCM 2022 coming this week!) which cover category theory, or doing the category theory exercises for LFTCM 2020. Note that Lean moves quickly (and breaks things) so some of these references may be out of date.