There is a lot of modalities seen in action at *Proper Orbifold Cohomology*, proceeding, essentially, from the example of “smooth sets”.

As Dmitry notes elsewhere, this article doesn’t give details on how to construct the models for the axioms (we hope to be writing these up, soon), but it does spell out loads of elementary proofs using the axioms.

]]>Dmitri: Thank you for writing it up! I feel comfortable with this.

How, then, would this help HoTT discuss richer (synthetic?) mathematics, which is the main reason I wish to approach cohesion. I’m comfortable with the notion of geometry+of+physics+–+smooth+sets, but hope to see what can get from it. To be more specific, what should I read after geometry+of+physics+–+smooth+sets? I feel I’m stuck there for a while..

Also, how much (homotopy) type theory one is advised to be familiar with before jumping into works of Shulman and Schreiber? The book [1] is standard but huge. I’m not sure if one should go through all of it..

[1] Homotopy Type Theory: Univalent Foundations of Mathematics-[TUFP IAS]

]]>All examples of such (cohesive, say, but also elastic, solid, etc.) modalities arise from adjunctions between sites. (In fact, given an adjoint quadruple as below, we can extract a (nonunique) adjunction of sites as indicated.)

Specifically, suppose we have an adjoint pair L⊣R, where L:S_1→S_2 and R:S_2→S_1 are functors between sites S_1 and S_2. Without loss of generality, assume that S_1 and S_2 have finite limits (or ∞-limits) and L preserves finite limits and coverings.

Both L and R induce adjoint triples given by Kan extensions: L_! ⊣ L^* ⊣ L_* and R_! ⊣ R^* ⊣ R_*, where L^*: PreSh(S_2) → PreSh(S_1) is precomposition with L and R^*: PreSh(S_1) → PreSh(S_2) is precomposition with R. By the above properties, these adjunctions between categories of presheaves restrict to categories of sheaves (for left adjoints, also apply sheafification).

We have L_* = R^* and L^* = R_!, so the above adjoint triples merge together in an adjoint quadruple: L_! ⊣ L^* ⊣ R^* ⊣ R_*.

Any such adjoint quadruple induces an adjoint triple of induced modalities: L^* L_! ⊣ L^* R^* ⊣ R_* R^*.

A typical example of L⊣R is the pair L:Cart→1 and R:1→Cart, where Cart denotes the cartesian site and 1 denotes the terminal category. The functor L is unique, the functor R pick the terminal object in R, i.e., the point.

Using the definition of L and R together with pointwise formulas for Kan extensions, we can easily compute the adjoint quadruple: L^* X = (S ↦ X), R^* F = F(pt), L_! F = colim(F), R_* X = (S ↦ X^{U(S)}), where U(S) denotes the underlying set of a manifold S.

From here, we can immediately compute the corresponding modalities.

]]>[First time posting here.. please correct me kindly if I have not followed any explicit or implicit rules. And please excuse my question if it’s vague.]

It’s exciting to see that HoTT can prove concrete homotopical results, like $\pi_1(S^1) \simeq \mathbb{Z}$. It seems that to go further into other subfields, we need modality and cohesion in the theory to “buff up” the local structures – be it topological, smooth, or super-smooth..

However, I had a hard time tapping into modality and cohesion. First of, I’ve tried to understand what a cohesive topos means. As a first example of a cohesive topos, I’ve read through geometry+of+physics+–+smooth+sets and found it exciting. However, it remains unclear how to build up a theory with local model “X” from scratch by myself.

To do that, I planned to read Shulman’s proof on Brouwer’s fixed point.. hoping to understand the process by looking at a classical theorem in topology. But it is unfortunately too advanced for me, I’m not even sure where to start asking if there’s someone to help. Not being too familiar with type theory, I reckon there must be something missing.

What would you suggest if I want to quickly tap into these kind of modalic math, understand at least the proof for Brouwer fixed point, and hopefully be able to understand Schreiber’s foundation of geometry and physics?

4th year math PhD student. I’m not afraid of reading formal papers.. as long as it’s as much self-sufficient as possible. In fact, I find there’s “too much” motivation out there.. I hope to get serious, and even start to think/research in this language. Put in another way using an analogy in the world of programming: I regard Def/Thm/Proof as the source code of a program, and a regular math paper as the literate code or the manual/documentation of the source code. Sometimes it’s nice to have docs to read.. but sometimes you’d rather dive into the source code to see what *it is*. My mood is at the latter stage.

I’m willing to provide more details if it’d be helpful. Thank you very much!

]]>