7
$\begingroup$

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.)
$\endgroup$
2
  • 2
    $\begingroup$ The Set category can be replaced by an elementary topos. Once you get rid of Russel's paradox related issues you can pretty much do anything. If not, then add a couple of ETCS axioms. $\endgroup$
    – Trebor
    Jul 11, 2022 at 13:13
  • 1
    $\begingroup$ IIRC there's some weird tricks that use set theory more explicitly but the vast majority of category theory just doesn't care. ncatlab.org/nlab/show/Scott%27s+trick Probably wrong here. $\endgroup$ Jul 11, 2022 at 15:25

3 Answers 3

6
$\begingroup$

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.

$\endgroup$
5
  • 1
    $\begingroup$ Here you're using excluded middle to mean: “for every type X, X + (X → ⊥)”, which is really a form of global choice. It might be worth pointing out that there's a more sensitive version stating “for every proposition P, P + (P → ⊥)”, where a proposition is a type any two of whose elements can be identified, aka h-propositions, homotopy propositions, or (-1)-types. This version doesn't entail axiom K. $\endgroup$ Jul 11, 2022 at 10:26
  • 1
    $\begingroup$ Thanks, fixed. Would it it possible to develop here the custom of daring to edit other people's answers? Probably not, academics are a jealous kind. $\endgroup$ Jul 11, 2022 at 15:32
  • 2
    $\begingroup$ You didn't mention setoids! (-:O $\endgroup$ Jul 12, 2022 at 5:10
  • 1
    $\begingroup$ Lean is 2. right? In which way is it achieved? $\endgroup$ Jul 12, 2022 at 5:21
  • $\begingroup$ Lean does something like the last bullet: it assumes strong principles that are enough to obtain Axiom K, and thus kill all the higher structure and ensure every type behaves as a 0-set from the homotopic viewpoint. More precisely, Axiom K is a form of proof irrelevance (in the particular case where the proposition to be proven is an equality), so the strong form of proof irrelevance available in Lean is enough to obtain it. I guess the axiom of choice would be enough on its own to get it as well through excluded middle. $\endgroup$ Jul 12, 2022 at 14:31
3
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

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.

$\endgroup$
6
  • 1
    $\begingroup$ The category formerly known as Set is defined in category_theory.types and the surrounding file. $\endgroup$ Jul 11, 2022 at 2:31
  • $\begingroup$ Small correction: Classical logic does not contradict univalence nor does it by itself imply that all types are (h-)sets, as indeed homotopy type theory is fully compatible with classical logic and the axiom of choice. Rather, Lean more directly just builds in that all identity types are propositions in a very strict sense, and it's this (rather than LEM or AC) that makes its types behave like sets. $\endgroup$ Jul 11, 2022 at 10:17
  • $\begingroup$ @UlrikBuchholtz I edited the answer so hopefully it is better now. However, even without UIP being baked into Lean's definitional equality, I think Axiom-K/UIP would follow from Lean's axiom of choice (which is more like AC_infinity in the HoTT book that AC_0 which is what I think you are referring to), right? (I don't know however how the axiom of choice is normally written in Coq when using classical logic and if the situation is the same there.) $\endgroup$
    – Jason Rute
    Jul 11, 2022 at 12:55
  • $\begingroup$ @UlrikBuchholtz Also, good point about classical logic and Univalence being compatible. Any interest in answering this question? 😊 proofassistants.stackexchange.com/questions/794/… $\endgroup$
    – Jason Rute
    Jul 11, 2022 at 12:58
  • $\begingroup$ Small mistake, you said that equality is decidable in the Hom set A -> B but I guess you meant something to do with contractibility not decidability. $\endgroup$ Jul 11, 2022 at 14:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.