Category Theory

[fredrik-bakke]

This issue outlines formalization goals for the category-theory module.

Formalization targets

The following list outlines missing formalizations that should be part of any standard library on category theory:

• [ ] Extensionality of
  • [ ] Small precategories
  • [ ] Large precategories
  • [ ] Small categories
  • [ ] Large categories
• [x] (large) Functor categories
• [ ] Rezk completion
  • [ ] Large Rezk completion of small precategory
  • [ ] Small Rezk completion of small precategory
  • [ ] Large Rezk completion of large precategory
• [ ] The (large) (pre)groupoid core of a (large) (pre)category
  • [X] The pregroupoid core of a precategory
  • [x] The groupoid core of a category
  • [ ] The large pregroupoid core of a large precategory
  • [ ] The large groupoid core of a large category
  • [ ] the (large) (pre)groupoidal completion
  • [ ] their adjunctions
• [x] The Yoneda lemma for (large) (pre)categories
  • [ ] Naturality of the Yoneda lemma
  • [ ] The Yoneda embedding is an embedding
• [ ] Colimits and limits in (large) (pre)categories Equivalence of
  • [ ] Definition as adjoint to constant functor
  • [ ] Definition as terminal object in cone category
  • [ ] Object with universal property
• [x] Dependent products of (pre)categories
  • [x] Dependent products of large (pre)categories
• [ ] Fully-faithful+essentially surjective factorization
• [ ] (large) Sub(pre)categories
  • [x] Full (large) Sub(pre)categories
  • [ ] Wide (large) Sub(pre)categories
• [ ] (large) Quotient (pre)categories
• [ ] (Co)cartesian families/fibrations
• [ ] The adjoint functor theorem
• [ ] Equivalence of transposing adjunctions and diagrammatic adjunctions
• [ ] Adjoint equivalences of (pre)categories (i.e. what is named "equivalences" in HoTT-UF)
• [x] Presheaf categories
  • [ ] Presheaf categories are free cocompletions
  • [ ] Representable presheaves

It would also be nice to have

• [ ] A basic treatment of wild categories
  • [ ] The homotopy precategory of a wild category
• [x] A basic treatment of strict categories
  • [ ] "Adjoint equivalences are equivalences" is equivalent to choice
• [ ] Left/right fibrations

[EgbertRijke]

Fibrations will be very nice to have, for instance if we want to make our extensionality proofs even more slick. We should follow the example of the 1lab on this front.

[fredrik-bakke]

Feel free to edit the main comment btw!

[fredrik-bakke]

#765 resolves item 7 :)

[EgbertRijke]

I think we should try to make more concrete goals that clearly focus the efforts of the person working on them. Goals of the form "formalize the theory of ..." are not attainable. An example of a concrete goal would be "Show that right adjoints preserve limits", or "Prove Beck's monadicity theorem". Notice how different those sound than "formalize category theory".

[EgbertRijke]

Btw this issue seems well organized and does try to focus the efforts of a contributor. So I don’t want to change this issue. But I wouldn’t like to see many future issues of the form “Formalize the theory of…” because in general I don’t think they’re so inspiring

[fredrik-bakke]

I think we should try to make more concrete goals that clearly focus the efforts of the person working on them. Goals of the form "formalize the theory of ..." are not attainable. An example of a concrete goal would be "Show that right adjoints preserve limits", or "Prove Beck's monadicity theorem". Notice how different those sound than "formalize category theory".

Please do! I posted this issue in hopes of getting help shaping more concrete goals. I'm not planning to implement everything in this issue myself, but I'll see if I can phrase some more concrete goals as well. I feel somewhat inspired to do fibrations, so I'll try to do that soon. But otherwise, everything is up for grabs, including developing the issue body.

[EgbertRijke]

Awesome! I think fibrations will be really nice to have