Finn Lawler empty 5 (changes)

Redirected from "Heyting categories".

Showing changes from revision #3 to #4: Added | Removed | Changed

There are three notions of equipment in the literature:

  • Wood’s: an identity-on-objects, locally fully faithful pseudofunctor KMK \to M, written ff *f \mapsto f_*, where each f *f_* has a right adjoint f *f^* in MM.

  • Shulman’s: a framed bicategory, that is, a pseudo double category MM whose source and target functors (s,t):M 1M 0×M 0(s,t) \colon M_1 \to M_0 \times M_0 form a bifibration.

  • that of Carboni–Kelly–Verity–Wood: a (normal) pseudofunctor M:K op×KCatM \colon K^{op} \times K \to Cat, where KK is a 1-category.

The last is strictly more general than the others, as are even their starred pointed equipments, i.e. those equipped with a transformation hom KM\hom_K \Rightarrow M, where the left and right actions of KK have suitable adjoints. These CKVW equipments should be equivalent to the others if we ask for a transformation M 2MM^2 \Rightarrow M making MM a (pseudo)monad in a suitable bi- or tricategory of ‘biprofunctors’.

  • There is also the related notion of a connection on a double category — an equipment is a (pseudo) double category with both a connection and an ‘op-connection’, the latter giving e.g. the right adjoints f *f^* in Wood’s definition.

Question: Why are these all equivalent?

Let’s forget about the ‘op-connections’ for the moment.

A pseudofunctor KMK \to M that is the identity on objects and locally fully faithful is the same as an identity-on-objects pseudofunctor KMK' \to M out of the locally discrete bicategory given by simply throwing away the 2-cells of KK.

An identity-on-objects pseudofunctor KMK \to M exhibits MM as the Kleisli object of a monad on KK in the 2-category of biprofunctors (q.v.). This will be the associated CKVW equipment.

Last revised on January 13, 2014 at 13:03:38. See the history of this page for a list of all contributions to it.