This is a companion discussion topic for the original entry at https://forest.localcharts.org/ocl-001x.xml

This is a companion discussion topic for the original entry at https://forest.localcharts.org/ocl-001x.xml

The \alpha in the second diagram should be pointing in the opposite direction, I changed it and it displays that way locally, but seems to not be updating even though the build workedâ€¦ Someone should tell the sysadmin

Nice construction! As you know, weâ€™ve used both of these categories (the â€śchartsâ€ť and the â€ślensesâ€ť) in the papers on diagrammatic equations (1, 2), but not both together in the form of a double category. I wonder if the double category could be used to frame in any interesting constructions. Beyond that, I wonder if using the intuitions from â€śchartsâ€ť and â€ślensesâ€ť is helpful here. I havenâ€™t thought about diagrammatic equations in those termsâ€”but then again, Iâ€™m not in the habit of thinking about lenses, so it might well be a natural perspective.

One fun thing about these â€śdiagram charts/lensesâ€ť is that they take part in a sort of microcosm principle for the Grothendieck (aka chart/lens) construction. Namely, if E : B^{\mathsf{op}} \to \mathsf{Cat} is an indexed category and \mathsf{Chart}(E) is its Grothendieck construction and \mathsf{Lens}(E) the Grothendieck construction of the pointwise opposite, then E lifts against the forgetful functor \mathsf{Diag}^{\to}(\mathsf{Chart}(E)) \to \mathsf{Cat} and \mathsf{Diag}^{\leftarrow}(\mathsf{Lens}(E)) \to \mathsf{Cat}, in each case by equipping E(b) with the functor interpreting it as a vertical chart or lens. Even more, \mathsf{Chart}(E) and \mathsf{Lens}(E) are determined as the initial lifts of E through \mathsf{Diag}^{\to} or \mathsf{Diag}^{\leftarrow}. This is just another way of saying that the Grothendieck construction is the (op)lax colimit of the diagram of categories E.

What is a â€śmicrocosm principleâ€ť? And what does it meant to lift against a forgetful functor?

The microcosm principle is a Baez-Dolan coinage remarking on how you need to be in a monoidal category to define a monoid, and in a monoidal 2-category to define a monoidal category, and in a monoidal 3-category to define a monoidal 2-categoryâ€¦

By saying that E : B^{\mathsf{op}} \to \mathsf{Cat} lifts against f : \mathsf{Diag}^{\to}(\mathsf{Chart}(E)) \to \mathsf{Cat} I mean there is a functor \hat{E} : B^{\mathsf{op}} \to \mathsf{Diag}^{\to}(\mathsf{Chart}(E)) so that f \circ \hat{E} = E. By the initial lift I mean that if L : B^{\mathsf{op}} \to \mathsf{Diag}^{\to}(C) is any other lift (f \circ L = E), then there is a unique functor \ell : \mathsf{Chart}(E) \to C so that \mathsf{Diag}^{\to}(\ell) \circ \hat{E} = L.