Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
How should one complete the analogy
hyperdoctrine : topos :: *** : -topos ?
From hyperdoctrine
The notion of a hyperdoctrine is essentially an axiomatization of the collection of slices of a locally cartesian closed category (or something similar)
So what is
essentially an axiomatization of the collection of slices of a locally cartesian closed -category (or something similar)?
Presumably syntactically we need a base category of contexts, then fibred above the possible expressions in the variables of the context types.
There are clearly more canonically expert people here than me, but let me say something anyway:
Iād think this is pretty obvious: a hyperdoctrine ā contrary to what the name might suggest ā is a rather simplistic concept: a functor to a 2-category such that each morphism in the image has left and right adjoint. Add extra conditions as need be, but this is the basic idea.
And this has the evident homotopy-theoretic refinement: an -functor to an -category landing in morphisms that have left and right -adjoint.
And as in the 1-categorical case, the self-indexing of any locally cartesian closed -category is an example.
What Urs said.
Thanks. Great. I was wondering about this in a talk by Yoshihiro Maruyama on Monad-Relativized Hyperdoctrines. So maybe there could be a parallel route to the one to modal hyperdoctrines to one to modal homotopy type theory.
But I must dash.
1 to 4 of 4