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.
Consider either the category of sheaves over the big zariski site, or some setting for Lawvere’s synthetic differential geometry.
What does the category of objects with a fixed reduction look like. The morphisms are morphisms such that is an isomorphism.
These are like the fibers of where consists of the reduced objects of , under modal homotopy type theory.
In the geometric setting, we should get some kind of linear category, like the category of quasicoherent sheaves. But I can’t find a place where this is discussed.
It’s a bit like how is like a -fibration, and the fiber of a scheme is its category of quasicoherent sheaves.
Or the “2-fibration” of a tangent category over a given category, possibly adjoint to a certain -context extension.
One thing to note is that all of these fibers of categories are settings for some linear type theory (possibly without objects being dualizable).
This is discussed in Section 2.3.4 (p. 35) of arXiv:1402.7041.
The algebras for the maybe monad canonically have a monoidal structure. I can’t figure out why this extends to a monoidal structure on all of the infinitesimal extensions. Particularly, how to get the monoidal structure of jets, or a monoidal closed structure. Is there a way to get that canonically?
I’m slowly learning the theory here. Thanks for the excellent reference. I think in a few months I might approach the problem you mentioned earlier, to see if I can make use of myself. Thanks for all of your help, Urs.
1 to 3 of 3