I do formal category theory

• A kind of 2-dimensional category theory
• finds categorical patterns inside category theory

«The purpose of category theory is to try to describe certain general aspects of the structure of mathematics. Since category theory is also part of mathematics, this categorical type of description should apply to it as well as to other parts of mathematics.

[O]ne should attempt to identify those properties that enable one to do the "structural parts of category theory".» – [Gra74]

Euclid theorem

FCT : CT = CT : MATH

(and perhaps \(\text{FCT} = \frac{\text{CT}^2}{\text{MATH}}\))

• CT = Mathematics of Mathematics
• FCT = category theory of category theory.

Commandments

1. Thou shalt not look inside objects of \(\cal K\)
2. Thou shalt define properties internally
   1. via Kan extensions/lifts
   2. via weighted/pseudo-limits
3. category theory \(=\) corollaries of the Yoneda lemma [SW78]
4. algebra \(=\) theory of monads and their algebras [BK89]

We shall take commandment 3 very seriously…

Yoneda structure on \(\mathcal{K}\):

1. a class of 0-cells \(\mathcal{K}_s\) of "small" objects

2. a class of 1-cells \(y_A : A \to \boldsymbol{P}\! A\), one for each small \(A\)

   • Each \((y_A, f : A \to B)\) determines a left extension

   \[\text{Lan}_fy_A : B \to \boldsymbol{P}\! A\]

   • Each \(y_A\) is fully faithful and dense (an "arity");
   • The correspondence \(A\mapsto \boldsymbol{P}\! A\) is a

   pseudofunctor \(\mathcal{K}_s^\text{coop} \to \mathcal{K}\).

… But there are other choices

Proarrow equipment on \(\mathcal K\):

a locally fully faithful 2-functor \(\iota : \mathcal{K} \to \overline{\mathcal{K}}\)

• it is the identity on objects
• for each \(f\in \mathcal{K}(A,B)\), \(\iota(f)\) has a left adjoint \(\iota_! f\) in \(\overline{\mathcal{K}}(A,B)\).

An equipment is

• Modeled on the embedding of categories in the bicategory of profunctors (bimodules? distributors?)
• an old idea, settled in [Woo82, Woo85] with obscure notation; nobody developed it
• a mysterious structure: axioms were later extended to six in [RW88]: do we really need them all? Why?

Today, it's way better to employ (hyper)virtual double categories and virtual equipments.

Mid-term goals

1. Relate these two apparently disconnected paradigms
2. Find applications to category theory:
   • Done in arXiv1804.08710; def. of a locally presentable object in a 2-category w/ a YS; unifies all instances of such.
   • Work in progress: the formal theory of Isbell duality;
   • Work in progress: unified approach to syntax-semantics dualities through Yoneda structures;
   • Work in progress: find Yoneda structures on the 2-category of (pre)derivators.

Strategy for Goal 1

• Study good categories: \(\mathcal{K}\) is co/complete, cartesian closed and strongly enriched over CAT;
• Study good Yoneda structures where \(\boldsymbol{P}\) is representable: such \(\boldsymbol{P}\) all have left adjoints \(\boldsymbol{P}^!\);
• Treat \(\boldsymbol{P}\) as a relative pseudomonad (like a monad, but not an endofunctor):
  • the Yoneda embedding is a unit \(\eta_A : A \to \boldsymbol{P}\! A\);
  • there is a skew-multiplication \(\mu_A : \boldsymbol{P}\! A \to \text{Lan}_J \boldsymbol{P} (\boldsymbol{P}\! A)\).

Strategy for Goal 1

The relative pseudomonad P = [ _ °, Set ] has a Kleisli bicategory Kl(P) which is a proarrow equipment. – [FGHW16]

This is a particular instance of

The relative pseudomonad P of a Yoneda structure has a Kleisli virtual double category.

• If P is good, Kl(P) is a virtual equipment
• If P is very good, Kl(P) is an equipment

Thanks!

References

• [BK89] R. Blackwell, G.M. Kelly, and A.J. Power. " Two-dimensional monad theory." Journal of pure and applied algebra 59.1 (1989): 1-41.
• [FGWH16] Fiore, M., et al., " Relative pseudomonads" Selecta Mathematica 24.3 (2018): 2791-2830.
• [Gra74] Gray, J.W., Formal category theory: adjointness for 2-categories. Vol. 391. Springer, 2006.

References

• [RW88] Rosebrugh, R., and R.J. Wood., " Proarrows and cofibrations." Journal of Pure and Applied Algebra 53.3 (1988): 271-296.
• [SW78] Street, R., and Walters, R,. " Yoneda structures on 2-categories." Journal of Algebra 50.2 (1978): 350-379.
• [Woo82] Wood, R.J., " Abstract pro arrows I." Cahiers de topologie et géometrie différentielle categoriques 23.3 (1982): 279-290.