HoTT Cohesion -- Exercise II | The n-Category Café

November 9, 2011

HoTT Cohesion – Exercise II

Posted by Urs Schreiber

$MathML-enabled post (click for more details).$

Following “exercise I” on Axiomatic Cohesion in Homotopy Type Theory, where we saw (thanks to Guillaume Brunerie!) the HoTT-Coq code incantation of the Maurer-Cartan form on cohesive ∞-groups, it should now be a small step to conjure up something rather interesting: the definition of differential cohomology and the proof of its characteristic curvature exact sequence.

A writeup of this in the pseudocode formerly known as traditional mathematics is in section 2.3.14, p. 147 of Differential Cohomology in a Cohesive ∞-Topos. The following “exercises a) – d)” try to extract from this a core statement that should have a fairly straightforward implementation in HoTT-Coq (I hope!).

As before, this “exercise” is an exercise that I am posing myself. But also as before, it is more than likely that HoTT experts can solve this many orders of magnitudes quicker than I will. Don’t hesitate, there are plenty of further “exercises” along these lines waiting to get attention.

Exercise II a) In exericse I you found HoTT encoding of the fiber sequence

$G \stackrel{\theta}{\to} \flat_{dR}\mathbf{B}G \to \flat \mathbf{B}G \to \mathbf{B}G$

exhibiting the Maurer-Cartan form with values in de Rham coefficients inside the moduli ∞-stack of flat ∞-connections for a cohesive ∞-group $G$ .

Take now $G = \mathbf{B}^n A$ to be an Eilenberg-MacLane object. Then, as before, the fiber sequence continues further to the left to yield

$\Omega \flat \mathbf{B}^{n+1} A \to \mathbf{B}^n A \stackrel{\theta}{\to} \flat_{dR} \mathbf{B}^{n+1}A \to \cdots \,.$

Show that $\flat$ – being a right adjoint – commutes with forming loop space objects and thus deduce the fiber sequence

$\flat \mathbf{B}^{n} A \to \mathbf{B}^{n} A \stackrel{\theta}{\to} \flat_{dR} \mathbf{B}^{n+1}A \,.$

Exercise II b) Consider a morphism into $\flat_{dR} \mathbf{B}^{n+1}A$ out of a 0-truncated object, to be denoted

$\Omega^{n+1}_{cl}(-,A) \to \flat_{dR} \mathbf{B}^{n+1} A \,.$

For later exercises we will demand the morphism thus denoted to be an effective epimorphism. But describing effective epiness will require more work than fits into the present exercise. Since the following parts c) and d) do not yet depend on this morphism being effective epi, we can ignore it for the moment and just assume some morphism out of a 0-truncated object. Extra credit, of course, if you manage to code effective epiness nevertheless!

Exercise II c) Define the type $\mathbf{B}^n A_{conn}$ – to be called the moduli ∞-stack of A-principal n-connections – as the ∞-pullback

$\array{ \mathbf{B}^n A_{conn} &\stackrel{F}{\to}& \Omega^{n+1}_{cl}(-,A) \\ \downarrow && \downarrow \\ \mathbf{B}^n A &\stackrel{\theta}{\to}& \mathbf{\flat}_{dR} \mathbf{B}^{n+1} A } \,.$

Exercise II d) Prove that the type thus defined fits into a fiber sequence of the form

$\flat \mathbf{B}^n A \to \mathbf{B}^n A_{conn} \stackrel{F}{\to} \Omega^{n+1}_{cl}(-,A)$

to be called the $\infty$ -stack refinement of the curvature exact sequence.

Remark. The meat is in a). The rest should be straightforward consequences whose main point is to amplify the relevance of a).

Posted at November 9, 2011 9:29 PM UTC

TrackBack URL for this Entry: https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2458

59 Comments & 3 Trackbacks

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

the pseudocode formerly known as traditional mathematics

I am unutterably amused by that remark. (-:

I wish I could be doing these exercises myself, but I just don’t have the time this month. )-: But I’m excited that they’re happening!

Posted by: Mike Shulman on November 10, 2011 3:40 AM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Cool, another exercise!

I think there are two ${}_{\mathrm{dR}}$ missing in the two last fiber sequences in a).

I’m trying to prove the a), but I’m stuck proving that the loop space of a discrete object is discrete. Is this true? How can I prove it?

I have tried to do it by hand using only what is formalized in HoTT, but it seems I really need an operation loop_disc taking a discrete object to a discrete object and having properties of a loop space, and I do not see which axioms imply that the category of discrete objects has loop spaces. If the usual (in the ambient topos $H$ ) loop space takes discrete objects to discrete objects, this will work, or if $\Pi$ commutes with loop spaces this will work too (but $\Pi$ does not seem to be supposed to commute with loop spaces), but I do not see how to prove it.

Posted by: Guillaume Brunerie on November 13, 2011 2:04 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

I think there are two ${}_{dR}$ missing in the two last fiber sequences in a).

Thanks for catching this. Sorry for the typo. I have fixed it now.

Posted by: Urs Schreiber on November 13, 2011 2:21 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

I’m trying to prove the a), but I’m stuck proving that the loop space of a discrete object is discrete. Is this true? How can I prove it?

The pseudocode proof is straightforward:

a) $\flat$ is a right adjoint (its left adjoint is $\mathbf{\Pi}$ ),

b) the loop space object of ${\ast} \to X$ is a pullback

$\Omega X \simeq \ast \times_X \ast$

and

c) since right adjoints preserve pullbacks and the terminal object

we have

$\begin{aligned} \flat \Omega X & \simeq \flat ( \ast \times_X \ast) \\ & \simeq (\flat \ast) \times_{\flat X} (\flat \ast) \\ & \simeq \ast \times_{\flat X} \ast \\ & \simeq \Omega \flat X \,. \end{aligned}$

So it would be sufficient to formalize the proof that right adjoints preserve pullbacks.

Thinking along these lines I just wondered here if we coded the right adjointness of $\flat$ correctly.

Posted by: Urs Schreiber on November 13, 2011 2:28 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

I do not see which axioms imply that the category of discrete objects has loop spaces.

Maybe the missing information was that forming loop spaces is forming a (homotopy) limit? Or with “axioms” you are distinguishing the pseudocode axioms for cohesive $(\infty,1)$ -toposes from the formal axioms in HoTT (and we might not have formulated the latter properly yet)?

Just for completeness, let me say that in the pseudocode context of higher topos theory any $\infty$ -category $\mathbf{B}$ that is both reflectively as well as coreflectively emdedded

$\mathbf{H} \stackrel{\overset{\Pi}{\to}}{\stackrel{\overset{Disc}{\hookleftarrow}}{\underset{\Gamma}{\to}}} \mathbf{B}$

has all limits and colimits: by the adjunction relations they are computed by computing them in $\mathbf{H}$ and then applying $\Pi$ for colimits and $\Gamma$ for limits. Because for any diagram $X : I \to \mathbf{B}$ we have

$\begin{aligned} \Gamma \lim_{\leftarrow_i} Disc X_i & \simeq \lim_{\leftarrow_i} \Gamma Disc X_i \\ & \simeq \lim_{\leftarrow_i} X_i \end{aligned}$

and

$\begin{aligned} \Pi \lim_{\to_i} Disc X_i & \simeq \lim_{\to_i} \Pi Disc X_i \\ & \simeq \lim_{\to_i} X_i \end{aligned} \,.$

Moreover, the functor $Disc$ , being both a left and a right adjoint, preserves all limits and colimits.

Therefore, in terms of our internal formulation this means that limits and colimits of discrete objects are computed in $\mathbf{H}$ and end up being themselves discrete again.

Posted by: Urs Schreiber on November 13, 2011 4:02 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

a) ♭ is a right adjoint (its left adjoint is Π),

I think you mean that its left adjoint is the inclusion of discrete objects.

Maybe the missing information was that forming loop spaces is forming a (homotopy) limit?

No, no problem with this, we know that loop spaces are homotopy pullbacks (even if we do not have a general notion of homotopy limit).

Just for completeness, let me say that in the pseudocode context of higher topos theory any ∞-category B that is both reflectively as well as coreflectively embedded has all limits and colimits: by the adjunction relations they are computed by computing them in H and then applying Π for colimits and Γ for limits.

Thanks, that’s what I wanted to know, the loop space in $\mathbf{B}$ is $\flat$ of the loop space in $\mathbf{H}$ . I don’t now why I just tried to apply $\Pi$ and not $\flat$ .

Now this seems to be enough to finish the proof that $\flat$ commutes with loop spaces (at least I have now maps in both directions, I haven’t proved that they are inverse to each other yet), but I guess I should wait for new axioms that do not imply that every object is discrete :-)

Posted by: Guillaume Brunerie on November 14, 2011 5:33 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

a) $\flat$ is a right adjoint (its left adjoint is $\mathbf{\Pi}$ ),

I think you mean that its left adjoint is the inclusion of discrete objects.

No, that would be $\Gamma$ . Let me try to clarify: we have an adjoint quadruple, which I like to write as

$(\Pi \dashv Disc \dashv \Gamma \dashv coDisc) : \mathbf{H} \stackrel{\stackrel{\Pi}{\to}}{\stackrel{\overset{Disc}{\hookleftarrow}}{\stackrel{\overset{\Gamma}{\to}}{\underset{coDisc}{\hookleftarrow}}}} \mathbf{B}$

and induced by this an adjoint triple, which we have come to write as

$(\mathbf{\Pi} \dashv \flat \dashv #) : \mathbf{H} \stackrel{\overset{\Pi}{\to}}{\stackrel{\overset{Disc}{\leftarrow}}{\underset{\Gamma}{\to}}} \mathbf{B} \stackrel{\overset{Disc}{\to}}{\stackrel{\overset{\Gamma}{\leftarrow}}{\underset{coDisc}{\to}}} \mathbf{H} \,.$

Here, notice, the first $\Pi : \mathbf{H} \to \mathbf{B}$ is not boldface, but the second $\mathbf{\Pi} : \mathbf{H} \to \mathbf{H}$ is. (I once thought that was a great idea, but it has its pitfalls, evidently.)

So indeed the left adjoint of

$\flat := Disc \Gamma$

$\mathbf{\Pi} := Disc \Pi \,.$

Now this seems to be enough to finish the proof that $\flat$ commutes with loop spaces

Okay, good!

(at least I have now maps in both directions, I haven’t proved that they are inverse to each other yet),

I would think one will have to use some right-adjointness property of $\flat$ for this. But maybe I am missing a shortcut.

but I guess I should wait for new axioms that do not imply that every object is discrete :-)

Yeah, sorry for that. Maybe we are about to have fixed it, but maybe there are other pitfalls to be aware of.

Anyway, thanks for looking into this!

Posted by: Urs Schreiber on November 14, 2011 6:31 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Last night I started proving that any internally reflective subcategory is closed under terminal objects and loop spaces, so I went ahead and finished it this morning just to reassure myself I still remember how to Coq. It’s here. I’m sure the same approach would work for arbitrary homotopy pullbacks.

I’m fairly certain this applies to codiscrete objects; I think our current axiomatization of those is fine. For discrete ones, as you say, we need to fix up the axioms first.

Posted by: Mike Shulman on November 14, 2011 8:33 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

I manage to prove (same link) that every internally-reflective subcategory (expressed in the naive way) is an exponential ideal, and even a “local exponential ideal” (closed under arbitrary dependent products). This should imply in the usual way that the reflector preserves finite products, but I haven’t finished that proof.

Actually, I wouldn’t be surprised if the reflector automatically preserved all finite limits, but I haven’t managed to prove that yet. One thing that’s standing in my way is that I don’t know whether if X is in the subcategory, and P : X -> Type is a family such that each P x is in the subcategory, then the total space { x:X & P x } is in the subcategory.

Posted by: Mike Shulman on November 15, 2011 11:57 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

This should imply in the usual way that the reflector preserves finite products,

That would be nice. It would in particular mean that in the internal formulation the axioms of cohesion simplify, because the need for the asymmetric extra condition that $\Pi$ preserves finite products would disappear.

I keep thinking that, simple as it is, the usual formulation of the axioms for cohesion does not quite look as nice as the role the axioms play suggests that it should.

But then, when you say next…

I wouldn’t be surprised if the reflector automatically preserved all finite limits,

this worries me. If that’s true, then this internal formulation would not help with cohesion. There $\Pi$ cannot generally be assumed to be left exact, I think.

But maybe I am misunderstanding some of what you said. I shouldn’t be posting, but should go to bed instead… But it a joy to see you write all this code.

Posted by: Urs Schreiber on November 16, 2011 12:36 AM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Ah, I think I’ve figured out what is going on. Everything I say below is known to be true for 1-categories, but I expect it to also be true for $(\infty,1)$ -categories.

I think that to give an internally-reflective subcategory, axiomatized in the way that we’ve been doing, is equivalent semantically to giving a reflective subfibration of the codomain fibration. (It’s certainly at least that.) That means we have a reflective subcategory of each slice category $\mathbf{H}/X$ , and pullback preserves the subcategories and commutes with the reflectors. This is more data than we want: we want all of this to be determined by just an ordinary reflective subcategory of $\mathbf{H}$ itself.

However, it is almost true that every reflective subcategory gives rise to a reflective subfibration, by a two-step process. First we define a factorization system $(E,M)$ where $E$ is the class of morphisms inverted by the reflector. (Size considerations come into play when showing that $(E,M)$ -factorizations exist.) The factorization systems which arise from reflective subcategories in this way are called reflective factorization systems; they are exactly those for which $E$ satisfies 2-out-of-3 (two-thirds of which is true for any factorization system).

Then we observe that given any factorization system on $\mathbf{H}$ , the factorizations give a reflection of $\mathbf{H}/X$ into $M/X$ , and the subcategories $M/X$ are preserved by pullback since $M$ is. And if $M$ is a pullback-stable class of morphisms for which each $M/X$ is reflective in $\mathbf{H}/X$ , then it is part of a factorization system exactly when it is closed under composition.

In our case, $M$ is the class of morphisms such that “each fiber of $f$ lies in the subcategory” is internally valid. Asserting this class to be closed under composition ought to be equivalent, working internally in the type theory, to the point that was confusing me: whether total spaces lie in the subcategory if their base and fibers do. Thus, taking this as an additional axiom, we should obtain a factorization system $(E,M)$ .

But we then furthermore need the missing third of 2-out-of-3 for $E$ in order to ensure that our factorization system comes from a reflective subcategory. I think that internally, this assertion ought to be equivalent to saying that if $X$ and $Y$ both reflect to the terminal object, then so does any fiber of any map between them – a very restricted sort of pullback-preservation for the reflector. Probably this will need to be asserted as an additional axiom too.

Finally, there is the additional condition (again, automatic when working internally) that pullback commutes with the reflectors. This is equivalent to saying that the factorization system is stable, which in turn is equivalent to saying that the corresponding reflector preserves finite limits. This is what I was getting at before — making everything “internal” in the type theory forces us to only be able to talk about lex-reflective subcategories. Thus, as you say, we won’t be able to axiomatize $\Pi$ in this way. Currently I’m thinking we’ll have to fall back to the suggestion I made here: first axiomatize the codiscrete objects, which are lex-reflective so that this works, then axiomatize the discrete objects using sharp Type.

Posted by: Mike Shulman on November 16, 2011 8:00 AM | Permalink | PGP Sig | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

And now I’ve implemented the first half of this in Coq, again here. With the reflective subcategory defined “internally” as we have been doing, and with the additional axiom that it is closed under dependent sums (which, as I said, is what the category theory says should be necessary to get a factorization system), I was able to define the two classes $M$ and $E$ . Internally speaking, $M$ is the class of morphisms all of whose fibers are in the subcategory, while $E$ is the class of morphisms all of whose fibers become contractible after applying the reflector. I was also able to prove that these two classes are orthogonal to each other (well, not quite—I didn’t check homotopy uniqueness of the lifting) and that every morphism factors into an $E$ followed by an $M$ .

The code doesn’t quite compile in vanilla Coq 8.3; it gives a universe inconsistency. For any readers not familiar with this phenomenon, it’s basically an artifact of the fact that Coq is not as clever about manipulating universes as it might be, and when doing things univalently we often exceed its capacity to determine that what we’re doing is okay. Hopefully at some point in the future, Coq will support true universe polymorphism, which ought to solve this problem. Until then, the stopgap solution is to use a patched version of Coq which turns off all universe consistency checking (patch available from Hugo Herbelin’s web page here). This technically makes Coq inconsistent (you could reproduce the Burali-Forti paradox if you tried hard enough), but as long as you don’t do anything so deliberately perverse, it’s fine.

I haven’t done anything yet with the last condition, the missing third of 2-out-of-3 for $E$ . I’m not sure yet what the best way is to phrase that condition internally. Once we include that axiom, it should be possible to prove that the reflector preserves all finite limits—perhaps by way of proving that $E$ is stable under pullback, or perhaps more directly. But I don’t know when I’ll have a chance to do that; I’ve spent far more time on this already than I should have. (-:

For purposes of the internal development of cohesion, it’s not clear that the factorization system itself is particularly important. However, working all of this out in Coq has reassured me that my intuition is more or less correct now. I also had to prove a lot of useful things about internally reflective subcategories along the way, like dependent functoriality and factorization. This might make it feasible to start talking about flat : sharp Type -> sharp Type, if anyone has the energy. (-:

Posted by: Mike Shulman on November 16, 2011 11:32 PM | Permalink | PGP Sig | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Thanks, Mike!

I was all busy with something else the last days, and so I need to catch up with all the things you write here.

One quick thought concerning this one here:

we’ll have to fall back to the suggestion I made here: first axiomatize the codiscrete objects, which are lex-reflective so that this works, then axiomatize the discrete objects using sharp Type.

First a question: I understand that a term of Type -> Type induces pullback-stable systems of subcategories, due to the pasting law

$\array{ g^* f^* j^* \hat Type &\to& f^* j^* \hat Type &\to& j^* \hat Type &\to& \hat Type \\ \downarrow && \downarrow && \downarrow && \downarrow \\ Y &\stackrel{g}{\to} & X &\stackrel{f}{\to}& Type &\stackrel{j}{\to}& Type }$

which says that if $f$ classifies a system of types in $j^* \hat Type$ , then so does $f g$ (just to make that explicit once).

I understand that replacing $Type$ here with $# Type$ evades the direct conclusion that we have defined a pull-back stable subfibration of the codomain fibration. But how do you have this under enough control to know that this would be the right thing to do instead?

Then another thought: I was wondering if we could assert the existence of $\flat$ more implicitly, without actually defining it as a term sharp Type -> sharp Type. If we had an internal adjoint functor theorem, it might be sufficient to assert that $#$ preserves internal limits (not just finite ones) in a suitable way.

Posted by: Urs Schreiber on November 17, 2011 7:57 AM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

how do you have this under enough control to know that this would be the right thing to do instead?

I don’t know for sure. But what I’m thinking is, since the codiscrete objects are a full subcategory equivalent to $\infty Gpd$ , and under this identification $\sharp$ is $\Gamma$ (assuming we’ve axiomatized $\sharp$ correctly, which I’m pretty confident about), when we consider $\sharp Type$ as an $\infty$ -groupoid it is exactly the core of (the small objects in) $\mathbf{H}$ . So since the codiscrete objects are a full subcategory, a morphism $\sharp Type \to \sharp Type$ is exactly an endomorphism of that core, which is something that we do have for any endofunctor of $\mathbf{H}$ .

The problem with this approach, as I see it right now, is figuring out how to state the reflectivity property, since terms in $\sharp Type$ are not “types,” and as such we don’t have “elements” or “functions” between them.

If we had an internal adjoint functor theorem, it might be sufficient to assert that $\sharp$ preserves internal limits (not just finite ones) in a suitable way.

That’s an interesting idea. I expect the closest thing we have to an adjoint functor theorem is to mimic the “large limit” construction, which will then give us something living in the next universe up. We could then use a “resizing axiom” to make it live in the universe where we started (or use the type-in-type patch).

However, I’m not confident that $\sharp$ does preserve internal limits in the model. I think that would be equivalent to $\Gamma$ being a locally cartesian closed functor, which doesn’t seem to be the case — does it? Anyway, if it did, then the indexed adjoint functor theorem would apply to show that it has an indexed left adjoint, which is exactly what we don’t have.

Posted by: Mike Shulman on November 17, 2011 5:52 PM | Permalink | PGP Sig | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

If we had an internal adjoint functor theorem, it might be sufficient to assert that ♯ preserves internal limits (not just finite ones) in a suitable way.

[…] Anyway, if it did, then the indexed adjoint functor theorem would apply to show that it has an indexed left adjoint, which is exactly what we don’t have.

Ah, I see. Right, if the internal formulation of “co/reflective subcategory” does not come out as we need it, then any equivalent formulation internalized will neither.

Of help would be the $\infty$ -analog of the internal characterization of local reflections.

Posted by: Urs Schreiber on November 18, 2011 9:49 AM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Of help would be the ∞-analog of the internal characterization of local reflections.

Hmm. I feel like that characterization relies on the fact that everything can be reduced to monomorphisms in a 1-topos. (For instance, subtoposes can be characterized in terms of monics.) For an $(\infty,1)$ -topos I would not expect that to be true. But maybe you were thinking of something more general?

Anyway, that characterization doesn’t internalize either, since the least dense subobjects are also not stable under pullback.

Posted by: Mike Shulman on November 18, 2011 4:52 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Anyway, that characterization doesn’t internalize either, since the least dense subobjects are also not stable under pullback.

I thought it would help that the least dense subobjects are only characterized separately over each $X$ as values of a functor $Sub(X) \to Sub(X)$ left adjoint to $\sharp_X : Sub(X) \to Sub(X)$ .

Posted by: Urs Schreiber on November 18, 2011 6:21 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

The point is that you can’t say anything internally and have it mean something “separately over each $X$ ”. Everything you say internally is stable under pullback. In fancy language, this is because pullback functors in a topos are logical.

Posted by: Mike Shulman on November 18, 2011 10:33 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

terms in $\sharp Type$ are not “types,” and as such we don’t have “elements” or “functions” between them.

Hmm. I’d been thinking that there’s no way of “escaping” from $\sharp Type$ , but that doesn’t seem to be the case.

Definition unsharpify : sharp Type -> Type :=
  fun sA => { A : Type & { x:A  &  map_to_sharp Type A ~~> sA } }.

Semantically, this is the map $\sharp Type \to Type$ which classifies the composite $\widehat{Type} \to Type \to \sharp Type$ . What does this map do in a cohesive $(\infty,1)$ -topos? What are the composites $Type \to \sharp Type \to Type$ and $\sharp Type \to Type \to \sharp Type$ ?

Of course there is also the map

Definition sharp_unsharpify : sharp Type -> Type :=
  fun sA => { Ax : sharp { A:Type & A } & sharp_functor pr1 Ax ~~> sA }.

which classifies $\sharp \widehat{Type} \to \sharp Type$ , about which we could ask the same questions.

Posted by: Mike Shulman on November 17, 2011 8:17 PM | Permalink | PGP Sig | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Thanks for all this input, Mike! And sorry for my slow reactions recently. The last days I had only time for HoTT cohesion a little bit over breakfast and after dinner.

I need to think about all the questions you ask about general abstract properties of cohesive $\infty$ -toposes. Certainly I don’t know off the top of my head. But I can try to think about it.

But two facts are slowing me down (apart from a general lack of time). The first is easily fixed: I don’t understand some of your code (see below).

The second is: I am getting worried that we are not going in the right direction. While in itself all the discussion of internal formulations of external-sub categories that you give is most interesting, I would be unpleasantly surprised if the complexity of the formulation is necessary for a good internal formulation of cohesion. Part of the charm of the external axioms of cohesion is that they are so very simple and natural. I feel they shouldn’t become so considerably involved after internalization. Maybe I am wrong, but that’s how I feel currently.

Here is a thought: for everything in the previous “Exercise I” and this “Exercise II” it is in fact sufficient to assume just a local $\infty$ -topos. (The extra left adjoint $\mathbf{\Pi}$ is not strictly needed yet.)

So: should we (or somebody) maybe first concentrate on HoTT-ing Awodey-Birkedal completely? I have this vague idea that one could just literally translate their axioms into HoTT-Coq code, and it would give us $\flat$ from $#$ not as a term $Type \to Type$ but more indirectly: “there exists a universal $#$ -equivalence over each $X$ , to be denoted $\flat X \to X$ ”.

(You must have thought of this before.)

Finally a stupid question about your code (I feel that I am slowing us down, but I can’t help it):

Definition unsharpify : sharp Type -> Type :=
   fun sA => { A : Type & { x:A  &  map_to_sharp Type A ~~> sA } }.

I can’t parse the piece

map_to_sharp Type A ~~> sA.

Is there a

map

missing?

Posted by: Urs Schreiber on November 18, 2011 1:37 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Don’t worry about slowing us down! I’m spending more time on this than I really should right now, so maybe it would be better to put it on a back burner for a little while.

I can’t parse the piece map_to_sharp Type A ~~> sA.

For any type X, we have a function term map_to_sharp X : X -> sharp X. We can then apply this to any term x of type X to obtain a term of type sharp X. Here, the type X is Type and the term x is A (which is a type, hence a term of type Type). So map_to_sharp Type A is a term of type sharp Type, and since so is sA, we can ask for the type of paths between them. Does that help?

I am getting worried that we are not going in the right direction… I would be unpleasantly surprised if the complexity of the formulation is necessary for a good internal formulation of cohesion.

I’ve been simultaneously proposing two different approaches: the one involving the factorization systems, and the other involving $\sharp Type$ . So far, I think the one involving factorization systems is not more complicated than what we had before: it would involve adding a few new axioms which, I think, look very natural (sum_codiscrete, codiscrete_reflective_fs, and an analogous sum_discrete), but in exchange we would get for free the facts that $\sharp$ is left exact and $\Pi$ preserves finite products. It’s not necessary to talk about factorization systems in order to state the axioms.

The approach involving $\sharp Type$ may look more complicated at the moment, and that might turn out to be intrinsically the case. Some things just are complicated and there’s no way around it. But I’ve also found that sometimes, in figuring something out, I have to go through a stage of seeing it in a complicated way, before it resolves later on into a simpler notion. All the complexity is still there, hidden in the background, and not everyone has to think about it, but understanding all the complexity at first is often helpful for me when trying to find the simple notion that underlies it.

By the way, I am also thinking that perhaps the two approaches are not that different. Since we have unsharpify, giving pi : sharp Type -> sharp Type will nevertheless induce a morphism

unsharpify o pi o (map_to_sharp Type) : Type -> Type

which is, of necessity, stable under pullback. So perhaps, if the localization+stabilization approach doesn’t work, then we just need to look for a different non-reflective stable factorization system with $M/1$ the category of discrete objects — the one induced by the above morphism.

there exists a universal $\sharp$ -equivalence over each $X$ , to be denoted $\flat X\to X$

As I said above, I don’t think this will help; the reflection will still end up having to be pullback-stable.

Posted by: Mike Shulman on November 18, 2011 5:27 PM | Permalink | PGP Sig | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Does that help?

Yes, thanks. I kept reading invisible brackets as in

map_to_sharp Type ( A ~~> sA )

but of course I should have seen from the context what was meant.

Posted by: Urs Schreiber on November 18, 2011 7:21 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

So far, I think the one involving factorization systems is not more complicated than what we had before: it would involve adding a few new axioms which, I think, look very natural […] but in exchange we would get for free the facts that ♯ is left exact and $\Pi$ preserves finite products. It’s not necessary to talk about factorization systems in order to state the axioms.

Ah, okay, now I get it!

I’ll go through the exercise of compiling all this (pseudocode and and code) into the $n$ Lab entry, to check if I am following all the details. I’ll get back to you when I am done with that.

Posted by: Urs Schreiber on November 18, 2011 6:37 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

I have been thinking about the $\sharp Type$ approach some more (largely because I haven’t found any reason yet to believe that the localization-stabilization factorization system exists for $\Pi$ ), and I think that it’s actually the second way of escaping that we want to use:

Definition escape (sA : sharp Type) : Type :=
  { Ax : sharp {A:Type & A} & sharp_functor pr1 Ax == sA }.

Partly, this is because I was thinking about the other one in models (and its dual, which I didn’t write down here), and they look pretty weird. This one, on the other hand, has the pleasing property that the composite

$Type \to \sharp Type \xrightarrow{escape} Type$

is equivalent to $\sharp \colon Type \to Type$ ! A proof of this is here; it’s quite simple once you know that $\sharp$ preserves pullbacks. This then implies that the other composite

$\sharp Type \xrightarrow{escape} Type \to \sharp Type$

must be “ $\sharp(\sharp)$ ”. (That’s something that’s surely going to give a universe inconsistency in an unpatched Coq.)

That means that if we work with $\sharp Type$ , then applying escape is a sort of “externalization”. For instance, suppose we postulate $\Pi\colon \sharp Type\to \sharp Type$ . Since $\sharp$ is a product-preserving functor, the “exponential” map $Type\times Type \to Type$ induces a map $\sharp Type \times \sharp Type \to \sharp Type$ , and if we compose one of those with $\Pi$ , we get a map $\sharp Type \times \sharp Type \to \sharp Type$ that takes types $A$ and $B$ (regarded as objects of the external core of the category) to the internal-hom $[\Pi A,B]$ (also so regarded). Finally, composing with $Type\to\sharp Type$ on the inputs and escape on the output, we obtain an operation $Type\times Type\to Type$ which takes types $A$ and $B$ and produces the external-hom $\mathbf{H}(\Pi A,B)$ (regarded as a codiscrete object of $\mathbf{H}$ ).

It should then be possible to axiomatize all the universal properties of $\Pi$ and $\flat$ in this way, speaking only about the external-homs.

Posted by: Mike Shulman on November 21, 2011 11:08 PM | Permalink | PGP Sig | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Hi Mike,

I was looking at all that you wrote over breakfast (but it will take me much more time to reasonably absorb your Coq code), and I am getting the idea, but I am not certain yet that I see where exactly you are headed.

Can you maybe give a concise outline of the steps that you are proposing? Assume that I understand the business about reflective factorization systems and just concisely list the strategy now.

For instance your file still starts out with reflect : Type -> Type and hence descusses lex reflective subcategories, as you have explained.

But at some point in your above messages I was getting the impression that you are proposing to instead axiomatize reflective subcategories entirely via their reflective factorization systems, thus circumventing the need to write a reflector of the form reflect : Type -> Type that makes thigs left exact.

Wouldn’t that then also help give the non-exact reflective subcategory of discrete objects? Instead of postulating explicitly a term flat : Type -> Type we’d postulate a factorization system with certain properties.

If this is not what you are imagining, then why bother with the factorization systems here at all and not just go via sharp : Type -> Type and then flat : sharp Type -> sharp Type?

You see, maybe I have not fully understood what you are doing now, or proposing to do. If you could just restate it concisely, that might be helpful.

Posted by: Urs Schreiber on November 17, 2011 9:47 AM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Ah, sorry; I guess I wasn’t very clear. The point that I was making is that the naive internal definition that we’ve been using, which looks like it is talking only about a reflective subcategory, is actually talking about a pullback-stable system of reflective subcategories of slice categories (since everything that is said “internally” happens automatically in every slice). If we wanted to actually be talking about merely a plain reflective subcategory, then we should add the two axioms

Axiom sum_codiscrete : forall X (P : X -> Type),
  is_codiscrete X -> (forall x, is_codiscrete (P x)) -> is_codiscrete {x:X & P x}.

which ensures that the stable system of reflective subcategories arises from a (necessarily stable) factorization system $(E,M)$ , and

Axiom codiscrete_reflective_fs : forall X Y (f : X -> Y) (y : Y),
  is_contr (sharp X) -> is_contr (sharp Y) -> is_contr (sharp {x:X & f x ~~> y}).

which ensures that that factorization system $(E,M)$ is a reflective factorization system, hence uniquely determined by the ordinary reflective subcategory $M/1$ . Such a subcategory will then automatically be lex-reflective, since the corresponding reflective factorization system is stable.

However, a reflective subcategory whose reflector is not lex can still occur as $M/1$ for a stable factorization system $(E,M)$ , if the factorization system is not reflective. So my proposal was to axiomatize $\Pi$ in the naive way plus the corresponding axiom above, which gives us a factorization system, but leave out the second axiom above; this should prevent our being able to prove that $\Pi$ is lex. (I haven’t really thought much yet about $\flat$ , or about the equivalence between the subcategories of discrete and codiscrete objects.)

If this factorization system were moreover the “localization/stabilization” of the reflective one corresponding to the subcategory of discrete objects, then not only would we be guaranteed that it is stable, but we would have the nice property that the morphisms in $M$ are those which are “locally discrete” or “locally constant”. In other words, a locally constant family over a type A would be a family P : A -> Type such that internally we can say forall x:A, is_discrete (P x).

However, right now I’m worried that this localization/stabilization factorization system may not exist in the models. In fact, two of the counterexamples in the paper I linked above are in categories of sheaves, with the reflective subcategory of discrete objects! The first one is sheaves over a connected, locally connected, but not locally-simply-connected space, which is not our situation (we have everything locally $\infty$ -connected). But the second is sheaves over a very nice space (a disc).

Here’s a concrete question about cohesive $(\infty,1)$ -toposes. Suppose we say a “weak equivalence” is a map which is inverted by $\Pi$ . To what extent are weak equivalences stable under pullback?

In particular, for the machinery of the Carboni-Janelidze-Kelly-Paré paper I linked to, the important case would be the following. Given a morphism $f\colon X\to Y$ , consider the following factorization through a pullback square:

$\array{ X & \xrightarrow{e} & P & \to & \Pi X\\ & _f\searrow & \downarrow^m & & \downarrow^{\Pi f}\\ & & Y & \to & \Pi Y}$

Assuming that $\Pi$ has stable units, it preserves this pullback square, and so the morphism $e$ is always a weak equivalence. Are there any hypotheses under which we can say that it is a pullback-stable weak equivalence?

Posted by: Mike Shulman on November 17, 2011 6:18 PM | Permalink | PGP Sig | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Here is finally a reply to an older comment, which I never reacted to. Now I realize that I still need to sort this out for myself.

You (Mike) wrote:

So my proposal was to axiomatize $\Pi$ in the naive way plus the corresponding axiom above, which gives us a factorization system, but leave out the second axiom above;

This may be obsolete by now, but I need to ask for again for clarification: is this proposal still viable?

Why do we need a factorization system for $\mathbf{\Pi}$ at all? Would it not be sufficient to show that morphisms all whose (homotopy) fibers are discrete form a reflective subfibration of the codomain fibration?

Since the internal axioms would be so much neater if this were the case, I am wondering about the following: even if the external axioms of cohesion don’t imply that discrete objects form a reflective subfibration, maybe all the models that I care about do?! In that case I would say: forget the external axioms and adopt the simple internal ones.

But I don’t know yet.

Are there any hypotheses under which we can say that it is a pullback-stable weak equivalence?

In the models for homotopy cohesion which I considered, I find that $\Pi$ preserves certain homotopy fibers (discussed here). This is of crucial importance for the applications, so I was rather happy about the fact. But my proof is very much taking place in the model. I always wanted to see to which generality I can lift it, but I never got around to.

Posted by: Urs Schreiber on November 22, 2011 10:40 AM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Would it not be sufficient to show that morphisms all whose (homotopy) fibers are discrete form a reflective subfibration of the codomain fibration?

Yesterday I would have agreed with this: I was hoping for the additional axiom of a factorization system, but I thought we could do without it. Today, however, I tried to finish the proof that the reflector preserves finite products, and I wasn’t able to do it without the sum axiom (the one that makes a factorization system). The proof is now here.

It’s possible that I just wasn’t sufficiently clever, but I suspect something extra is required. In retrospect, it reminds me of the fact that inductive types with simple eliminators are only weakly initial objects; to prove uniqueness of recursively defined functions you need a dependent eliminator.

Of course, we could just add the axiom that $\Pi$ preserves finite products separately, if it were true in models that the reflector on each slice category preserves finite products. I do definitely agree that we shouldn’t restrict ourselves to the external axioms of cohesion in their current form, but we should look at the models we care about. (But that way we’d lose the nice fact that we get product-preservation for free.)

Something else to keep in mind, which I just realized, is that not only is everything we say internally pullback-stable, it must also be local, in the sense that it descends along effective epis and (finite, and even indexed) coproducts. I wrote out a quick internal proof of this here. I think that stability and locality should be sufficient, however, since by HTT 6.1.6.3 they guarantee that such a class has a classifying object, which is what the internal axiomatization works with. (Of course, it has yet to be proven that HoTT has models in any $(\infty,1)$ -topos other than $\infty Gpd$ , but we’re sort of tacitly assuming through all of this that it eventually will be.)

Posted by: Mike Shulman on November 22, 2011 3:41 PM | Permalink | PGP Sig | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

it descends along effective epis and (finite, and even indexed) coproducts. I wrote out a quick internal proof of this here.

Thanks, good to know.

In there you define effective epis internally to be the maps with all homotopy fibers inhabited. Is that equivalent to the standard definition of “homotopy effective” epis?

I was wondering if this characterization would be useful for a HoTT formulation: a morphism in an $\infty$ -topos is (homotopy-)effective precisely if it induces by pullback an injective map on subobjects (i.e. on -1-truncated morphisms).

Of course, we could just add the axiom that $\Pi$ preserves finite products separately

Sure. And I appreciate the fact that with the remarkable work that you have done the last days on the internal formulation of factorization systems and of the externalization via sharp-escape, it seems clear that one can obtain some axiomatization of what we want.

But I keep being haunted by that hope that internally the situation becomes more “natural”, rather than less so. When internal reflective subcategories turned out to be automatically product-preserving, one part of myself took that as a hint: internally one of the external axioms disappears and becomes automatic!

Maybe I am seeing ghosts. I’ll try to find some time to think about whether the motivating models for homotopy cohesion happen to secretly exhibit more $\Pi$ -pullback stability.

Posted by: Urs Schreiber on November 22, 2011 5:15 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Is that equivalent to the standard definition of “homotopy effective” epis?

I presume you mean this one. We can’t formalize that in HoTT yet, of course; we still need a workable notion of “simplicial object”. But I fully expect them to be equivalent. I think we can even deduce that model-wise from what we know now, since both notions of “effective epi” form the left class of a factorization system whose right class is the monomorphisms ((-1)-truncated morphisms).

a morphism in an ∞-topos is (homotopy-)effective precisely if it induces by pullback an injective map on subobjects

I would expect we could prove that in HoTT. I don’t immediately see a use for it, but it’ll be good to keep in mind in case it does turn out useful.

But I keep being haunted by that hope that internally the situation becomes more “natural”, rather than less so.

Sure, I understand. I think it would be great if the other approach turned out to work! I’m just currently skeptical, but I’m not saying you shouldn’t work on it.

After thinking about it a lot the past few days, I don’t find the sharp-escape approach any less natural than the external formulation (though it is admittedly not any more natural). It basically amounts to first saying “we have a subtopos (the codiscretes) that we’re going to call the ‘external world’” and then copying the external formulation in terms of that ‘external world’.

From another point of view, the lack of any added “naturalness” for the sharp-escape version is a virtue, because it means the framework is more flexible. Sharp by itself axiomatizes any geometric subtopos. (As a way of putting off my job applications even further, this morning I proved that any open subtopos satisfies the axioms of sharp. I want to do closed subtoposes too, but that requires some setup of homotopy pushouts first.) Adding flat then axiomatizes any local geometric morphism. We can then add $\Pi$ and properties of $\Pi$ to make it locally connected, strongly connected, totally connected, etc.

I think we can even talk about any geometric morphism $E\to S$ , not necessarily local, with the following trick. First construct the scone $scn_S(E)$ , which is a local $S$ -topos in which the codiscrete objects are a closed subtopos, whose complementary open subtopos is equivalent to $E$ . Thus, the internal logic of the single category $scn_S(E)$ allows us to talk about both $E$ and $S$ and the geometric morphism between them.

As an example of where this extra generality might be useful, the effective topos comes with a geometric embedding from $Set$ as “codiscrete objects”, but the embedding is not essential, so there is no $\flat$ (and certainly no $\Pi$ ).

Posted by: Mike Shulman on November 22, 2011 9:25 PM | Permalink | PGP Sig | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

I wrote:

I’ll try to find some time to think about whether the motivating models for homotopy cohesion happen to secretly exhibit more $\Pi$ -pullback stability.

Okay, here are some first observations on models of homotopy cohesion presented by ∞-cohesive sites.

First I consider the fibered reflector that was mentioned in a previous comment here.

Let $C$ be an $\infty$ -cohesive site and consider the Cech-localized projective model structure on simplicial presheaves over it, $[C^{op}, sSet]_{proj,loc}$ . This presents a cohesive $\infty$ -topos $\mathbf{H}$ .

Since the left Bousfield localization from the global to the local structure presevers weak equivalences, cofibrations, homotopy colimits and finite homotopy limits, it is sufficient for the following to argue in $[C^{op}, sSet]_{proj}$ .

Now I make heavy use of Dugger’s cofibrant replacement theory in the projective structure (summarized here).

This says that for $X$ any simplicial presheaf, a projectively cofibrant replacement is given by

$Q X : [k] \mapsto \coprod_{U_0 \to U_1 \to \cdots \to U_k \to X_k} U_0 \,,$

where the coproduct is over sequences of representables $U_i \in C \hookrightarrow [C^{op}, sSet]$ as indicated. The face and degeneracy maps are the obvious ones.

By the discussion of ∞-cohesive sites, we have that $\mathbf{\Pi}$ is given by the left derived functor of the colimit functor $\lim_\to : [C^{op}, sSet] \to sSet$ postcomposed with the injection $const : sSet \hookrightarrow [C^{op}, sSet]$ . So on the cofibrant replacements from above it is just given by degreewise colimits. Moreover, since the colimit over a representable Set-valued functor (such as the $U$ s above) is the point, we have that the reflector

$(X \to \mathbf{\Pi}(X)) \in \mathbf{H}$

is presented by the morphism of simplicial presheaves which in degree $k$ is the evident map of sets

$\left( \coprod_{U_0 \to U_1 \to \cdots \to U_k \to X_k} U_0 \right) \to \left( \coprod_{U_0 \to U_1 \to \cdots \to U_k \to X_k} * \right)$

that summand-wise is the terminal $U_i \to *$ .

So given a morphism $f : Y \to X$ , we can present the canonical diagram

$\array{ Y &\to & \mathbf{\Pi}Y \\ \downarrow && \downarrow \\ X &\to& \mathbf{\Pi}X } \;\;\;\;\; \in \mathbf{H}$

by the diagram of simplicial presheaves

$\array{ (\coprod_{U_0 \to U_1 \to \cdots \to U_\bullet \to Y_\bullet} U_0) &\to& (\coprod_{U_0 \to U_1 \to \cdots \to U_\bullet \to Y_\bullet} *) \\ \downarrow && \downarrow \\ (\coprod_{U_0 \to U_1 \to \cdots \to U_\bullet \to X_\bullet} U_0) &\to& (\coprod_{U_0 \to U_1 \to \cdots \to U_\bullet \to X_\bullet} *) } \,.$

Since $[C^{op}, sSet]$ is a right proper model category, for computing the homotopy pullback of the bottom right cospan it is sufficient to factor the morphism on the right through a fibration

$(\coprod_{U_0 \to U_1 \to \cdots \to U_\bullet \to Y_\bullet} *) \stackrel{\simeq}{\hookrightarrow} K \stackrel{fib}{\to} (\coprod_{U_0 \to U_1 \to \cdots \to U_\bullet \to X_\bullet} *)$

and then take the ordinary pullback of

$\array{ && K_\bullet \\ && \downarrow \\ (\coprod_{U_0 \to U_1 \to \cdots \to U_\bullet \to X_\bullet} U_0) &\to& (\coprod_{U_0 \to U_1 \to \cdots \to U_\bullet \to X_\bullet} *) } \,.$

Here $K$ can be chosen to be discrete in that it is degreewise a constant presheaf. The universal morphism in the homotopy pullback thus presented is then

$(\coprod_{U_0 \to U_1 \to \cdots \to U_\bullet \to Y_\bullet} U_0) \;\; \to \;\; \left(\coprod_{U_0 \to U_1 \to \cdots \to U_\bullet \to Y_\bullet} ( U_0 \times K_{U_0 \to \cdots \to U_\bullet \to X_\bullet} ) \right) \,,$

which is degreewise and componentwise the pairing of the identity with the component induced by the above factorization.

Since all components of $K$ are discrete, the object on the right is still cofibrant, by Dugger. Therefore the value of $\mathbf{\Pi}$ on this universal morphism is still given by applying the ordinary colimit degreewise. This again simply contracts all the $U_0$ s to points. The result is the first morphism

$(\coprod_{U_0 \to U_1 \to \cdots \to U_\bullet \to Y_\bullet} *) \stackrel{\simeq}{\hookrightarrow} K$

from the above factorization, hence a weak equivalence.

In conclusion, this establishes over $\infty$ -cohesive sites a factorization of $f : Y \to X$ as

$Y \to reflect(f) \to X$

where the first morphism is a $\mathbf{\Pi}$ -equivalence and the second has discrete homotopy fibers.

Next I should try to see if

$\array{ Y &&\to&& reflect(f) \\ & {}_{\mathllap{f}}\searrow && \swarrow \\ && X }$

has the universal property of a reflection on $\mathbf{H}/X$ . But I am not sure yet about that.

Posted by: Urs Schreiber on November 22, 2011 11:14 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

I wrote:

Next I should try to see if […]

Wait, no. The above argument is proof that this cannot work, that what I was hoping for fails in the models of homotopy cohesion that I care about:

By the discussion below (2.8) in Carboni-Janelidze-Kelly-Paré what I showed implies that if the system were fiberwise reflective, then it would be a factorization system. By the remark above (2.8) it would furthermore be stable. Hence discrete objects would be lex-reflective, which they aren’t.

Okay. That heals me from seeing the ghosts that I was seeing. I’ll follow you through the sharp-escape route now.

Posted by: Urs Schreiber on November 23, 2011 12:36 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Of course, it has yet to be proven that HoTT has models in any (∞,1)-topos other than ∞Gpd, but we’re sort of tacitly assuming through all of this that it eventually will be.)

What is lacking with the Awodey-Warren result that intensional ML type theory with identity types has a sound model in any simplicial model category with cofibrations the monos, so in particular in the Joyal- and the Jardine model structure presentations of hypercomplete $\infty$ -toposes?

Posted by: Urs Schreiber on November 23, 2011 12:36 AM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

What is lacking

Ah, univalence?

Posted by: Urs Schreiber on November 23, 2011 12:45 AM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Ah, univalence?

Indeed! Of course, morally univalence is there in the object classifiers, but the problem is that type theory is stricter than $(\infty,1)$ -categories. No one has yet managed to find sufficiently strict models for object classifiers to satisfy univalence (except Voevodsky’s model in simplicial sets, which uses very special features of simplicial sets). But I have faith that we will succeed eventually….

Posted by: Mike Shulman on November 23, 2011 5:04 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Ah, univalence?

Indeed!

Okay, thanks. I have edited the Idea-section and the References section at nLab:homtopy type theory to make this clearer (for people like me, that is). Also created nLab:univalence in the process.

No one has yet managed to find sufficiently strict models for object classifiers to satisfy univalence

So it’s already hard for just the global model structure on simplicial presheaves? (I haven’t really thought about object classifiers outside of $\infty Grpd$ at all, yet.)

Posted by: Urs Schreiber on November 23, 2011 11:06 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Perhaps someone like Peter Lumsdaine who understands the type theory better will step in, but here’s the deal as I understand it. Firstly, types have to be represented by fibrant objects, and dependent types by fibrations. So we need to pick a fibration $\widehat{Type}\;\twoheadrightarrow \; Type$ between fibrant objects that represents the object classifier. Okay, no problem — every morphism in an $(\infty,1)$ -category is represented by some fibration between fibrant objects.

But now, at least in the only way we currently know how to model type theory categorically, the dependent type over $A$ that is classified by a morphism $A\to Type$ must be the strict (1-categorical) pullback of the fibration $\widehat{Type}\to Type$ to $A$ . Such a pullback is always a homotopy pullback, so it represents the $(\infty,1)$ -pullback and thus classifies the same object of $\mathbf{H}/A$ (up to equivalence). Moreover, any object of the $(\infty,1)$ -overcategory $\mathbf{H}/A$ which is classified by the object classifier $Type$ should be equivalent to some fibration over $A$ which is such a strict pullback.

The problem is that the types living in any given universe need to be closed under all the other structure in type theory, like dependent products (including function spaces) and (higher) inductive types, and currently we also only know how to model that structure using strict 1-categorical structure. The objects classified by the $(\infty,1)$ -categorical object classifier are closed under all the corresponding $(\infty,1)$ -categorical constructions, but that doesn’t imply that the fibrations strictly classified by maps into the chosen fibrant object $Type$ are closed under the strict 1-categorical versions of these constructions.

I think that ideally, what we’d like is a univalent fibration which (strictly) classifies all fibrations whose fibers are “bounded in cardinality” by some inaccessible. That should imply closure under all the relevant operations as well as all future ones that get dreamed up. But as yet, I don’t think we know how to obtain such a thing.

Posted by: Mike Shulman on November 24, 2011 8:39 PM | Permalink | PGP Sig | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

[…] must be the strict (1-categorical) pullback of the fibration […]

Yes, this I understand. It is therefore that I was wondering if the model already constructed in $sSet_{Quillen}$ would not directly generalize to a model in a global projective model structure on simplicial presheaves $[C^{op}, sSet_{Quillen}]_{proj}$ over any $C$ , since all these fibrations and pullbacks simply happen objectwise there.

But probably this argument breaks in that there is a little bit of colimits (inductive types) that needs to be taken care of, too, and that does not easily lift from the point to a generic $C$ ?

Posted by: Urs Schreiber on November 24, 2011 10:04 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

since all these fibrations and pullbacks simply happen objectwise there

But the object classifier does not happen objectwise, does it?

Posted by: Mike Shulman on November 25, 2011 8:36 AM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Belated reply to this exchange:

since all these fibrations and pullbacks simply happen objectwise there

But the object classifier does not happen objectwise, does it?

What is the $\kappa$ -compact object classifier in a presheaf $\infty$ -topos $PSh_\infty(C)$ ?

I’d think it is the presheaf that assigns to any object $U \in C$ the full sub- $\infty$ -groupoid of $Core(PSh_\infty(C)_{/U})$ on the relatively $\kappa$ -compact morphisms.

Posted by: Urs Schreiber on December 6, 2011 8:16 AM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Yes, by the Yoneda lemma, that’s basically what it’s got to be, right?

Posted by: Mike Shulman on December 6, 2011 7:47 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Yes, by the Yoneda lemma, that’s basically what it’s got to be, right?

Yes. And that’s what I would call “the object classifier happens objectwise” in the above words.

Now with $\widehat {\Type} \to Type$ a projective fibration presenting the universal fibration, we have that it is objectwise a Kan fibration and that its 1-categrical pullbacks are homotopy pullbacks and are objectwise 1-categorical pullbacks which are homotopy pullbacks.

Therefore it looks to me as if much of what goes through for Voevodsky’s univalent model in $\mathrm{sSet}_{Quillen}$ ought to go through for any $[C^{op}, sSet_{Quillen}]_{proj}$ , too, at least as long as we are not talking about colimits.

But I haven’t really thought about it, I should study Voevodsky’s model in detail. I was just wondering if somebody considered this obvious “objectwise generalization” . I won’t be shocked if you tell me that this is too naive and runs into problems at some point. I’d just like to know which point that is :-)

Posted by: Urs Schreiber on December 7, 2011 8:18 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Ah. To me “objectwise object classifier” would mean the functor constant at the object classifier of sSet.

a projective fibration presenting the universal fibration, we have that it is objectwise a Kan fibration and that its 1-categorical pullbacks are homotopy pullbacks and are objectwise 1-categorical pullbacks which are homotopy pullbacks.

How does that deal with the problem I mentioned here?

Posted by: Mike Shulman on December 7, 2011 10:16 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Today, however, I tried to finish the proof that the reflector preserves finite products, and I wasn’t able to do it without the sum axiom

So you can show that a reflective subfibration gives an exponential ideal, but not that the reflector preserves products? What’s going on? Shouldn’t one imply the other?

Posted by: Urs Schreiber on November 23, 2011 12:53 AM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

So you can show that a reflective subfibration gives an exponential ideal, but not that the reflector preserves products?

That does seem wrong, doesn’t it? I should try mimicking the classical proof of that direction more closely.

By the way, I have now completed the proof here that with all the axioms included, the reflector preserves homotopy pullbacks.

Posted by: Mike Shulman on November 23, 2011 5:07 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Whew! Yes, being an exponential ideal does imply that the reflector preserves finite products, as it should. But formalizing that was pretty tricky! The standard proof goes by a longish sequence of bijections/equivalences, where $C$ is in the subcategory and $A$ and $B$ are arbitrary: $\array{ A \times B & \to & C \\ A & \to & C^B\\ L A & \to & C^B\\ L A \times B & \to & C\\ B & \to & C^{L A}\\ L B & \to & C^{L A}\\ L A \times L B & \to & C }$ using the fact that $C^B$ and $C^{L A}$ are in the subcategory by assumption. Thus, $L A\times L B$ has the same universal property as $L(A\times B)$ , so they are isomorphic. However, that casual appeal to the Yoneda lemma requires knowing that the composite equivalence is natural, which is easy at each step but difficult to prove all at once. I ended up manually putting together all the naturalities at each step, but clearly we need to set up some better technology for talking about universal properties and natural equivalences. However, that’s for another day….

Posted by: Mike Shulman on November 23, 2011 9:24 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

I am wondering, in light of the formulation using factorization systems, whether we might be able to escape from the problem of pullback-stability for $\Pi$ . In particular, I wonder whether not asserting the final 2-out-of-3 axiom in that case, thus not demanding that the factorization system be reflective, would be enough. I believe that there can exist stable non-reflective factorization systems $(E,M)$ for which the reflector onto the subcategory $M/1$ is not left exact.

In order to tell whether this is possible, I need to know more about cohesive $(\infty,1)$ -toposes. In particular, I want to know whether $\Pi$ , while not left exact in general, may satisfy some left-exactness conditions beyond preservation of finite products. For instance:

Does it preserve monomorphisms?
Is it semi-left exact? (This would mean that it preserves the pullback of $\eta_X \colon X\to \Pi X$ along any map $A\to \Pi X$ for which $A$ is discrete.)
Does it have stable units? (This would mean that it preserves the pullback of $\eta_X \colon X\to \Pi X$ along any map $A\to \Pi X$ for any $A$ at all, or equivalently that it preserves all pullbacks over discrete objects.)

In particular, I am contemplating the notion of localization and stabilization for factorization systems as discussed in this paper. There, given a factorization system $(E,M)$ (for which I am thinking of the reflective factorization system associated to the subcategory of discrete objects), one constructs (in good cases) a new stable factorization system $(E', M^\ast)$ , where $E'$ is the class of maps all pullbacks of which are in $E$ , and $M^\ast$ is the class of maps which can be pulled back along an effective descent map to become in $M$ .

Of course, $(E', M^\ast)$ will no longer be reflective, but it might still be the case that $M^\ast /1 \simeq M/1$ . I think that this will be the case if $\Pi$ has stable units, at least. If we were in this good case, then we might still be able to use the internal formulation of $\Pi$ , interpreting it with $(E', M^\ast)$ rather than $(E,M)$ .

Posted by: Mike Shulman on November 17, 2011 12:45 AM | Permalink | PGP Sig | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Here’s an attempt at an argument for why $\Pi$ might have stable units. If $A$ is an $\infty$ -groupoid, then $\mathbf{H}/Disc A \simeq \mathbf{H}^A$ , with the subcategory of discrete objects over $Disc A$ identified with $\infty Gpd / A \simeq \infty Gpd^A$ . The reflector $\Pi/Disc A$ of $\mathbf{H}/Disc A$ into these subcategories, then, is identified with the reflector $\Pi^A \colon \mathbf{H}^A \to \infty Gpd^A$ . But products in functor categories are calculated pointwise, so since $\Pi$ preserves finite products, so does $\Pi^A$ , and hence so does $\Pi/Disc A$ . But the latter assertion says exactly that $\Pi$ preserves pullbacks over $Disc A$ .

In fancier language, this means that $\Pi$ having stable units is the “indexed” version of its preserving finite products—indexing being automatic when the base $(\infty,1)$ -topos is $\infty Gpd$ .

Posted by: Mike Shulman on November 17, 2011 1:09 AM | Permalink | PGP Sig | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

If A is an $\infty$ -groupoid, then $\mathbf{H}/Disc A \simeq \mathbf{H}^A$

I have convinced myself of this now for the case that $\mathbf{H}$ has an $\infty$ -cohesive site of definition. I have written that into the $n$ Lab here.

Probably I am missing a more general simple argument?

Posted by: Urs Schreiber on November 23, 2011 7:24 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

I was thinking of it as the $\infty$ -version of extensivity. It seems like it should be true for any $(\infty,1)$ -topos. Can we say something like the following? Modulo size considerations, the object classifier should be the object-of-objects of an internal category $T$ in $\mathbf{H}$ that represents entire slice categories: $\mathbf{H}/X \simeq \mathbf{H}(X,T)$ Probably $T$ is officially a simplicial object in $\mathbf{H}$ satisfying complete Segal conditions, and so $\mathbf{H}(X,T)$ is a complete Segal space. Then by adjointness, we have $\mathbf{H}/Disc A \simeq \mathbf{H}(Disc A,T) \simeq \infty Gpd(A, \Gamma T) \simeq \mathbf{H}^A$ since $\Gamma T \simeq \mathbf{H}$ .

Posted by: Mike Shulman on November 23, 2011 9:37 PM | Permalink | PGP Sig | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

I have (only) now installed Coq, created a GitHub account, forked off Mike’s repository and started to play around (I haven’t yet managed to “patch the Universe inconsistency”, though).

One question: I’d like to break up the code that we have into smaller pieces and then “load” these under generic names. How does one do this?

I am looking for something a bit more sophisticated than the Require Import-line (or at least the use of it that I have seen so far). It should be possible to load, for instance, the file that defines reflective subcategories and then say “let A, B and C be three reflective subcategories”, so that then three copies of the respective lists of axioms are instantiated. Is that possible? What’s the code for it?

While playing around wth the Coq code, I already learned something about cohesion whose relevance, obvious as it is, I didn’t fully appreciate before: namely that it is interesting to consider the fact (and its models) to be proven in the above exercise II not for flat, but for pi in the internal homs, namely the fiber sequence of internal homs

$[X, \Omega A] \to [\mathbf{\Pi}_{dR} X, A] \to [\mathbf{\Pi}X , A] \to [X,A]$

as before. This is useful. For instance $[\mathbf{\Pi}_{dR}X, A]$ is the correct moduli $\infty$ -stack of flat $A$ -valued differential forms on $X$ , while $[X, \flat A]$ is so only after “concretification”.

But $[X, -]$ preserves homotopy pullbacks, so that this slight variant of the above exercise should be solvable just with $\mathbf{\Pi}$ , even.

Lastly, I looked around a bit for existing discussion of internal subcategories, if only to know what to cite in the $n$ Lab entry. Not sure if I was looking in the right places, though (also different concepts go by the name “internal subcategory”). But I notice that on p. 5 of a recent note Eugenio Moggi mentions in passing the fact that internally formulated subcategories of cartesian closed categories preserve products.

Posted by: Urs Schreiber on November 21, 2011 3:00 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

It should be possible to load, for instance, the file that defines reflective subcategories and then say “let A, B and C be three reflective subcategories”, so that then three copies of the respective lists of axioms are instantiated.

Indeed! This was possible with the old file, but it was a little annoying. The way I originally coded that file was with all the “axioms” of a reflective subcategory as “hypotheses” in a “section”. When the section is over, all those hypotheses are automatically “generalized”, so that all the axioms become parameters to all the objects defined in the section.

Thus, to do what you suggest, you would have had to write out separate copies of all the axioms for A, B, and C, and then pass all the relevant axioms to whichever function or theorem you wanted to invoke for A, B, or C respectively.

As of just now, I have pushed a new version of the code which improves on this by using Coq’s “type classes”. Now you can say

Axiom is_codiscrete : Type -> Type.
Axiom codiscrete_is_rsf : rsf is_codiscrete.
Existing Instance codiscrete_is_rsf.

The type class ‘rsf’ (for reflective subfibration) incorporates all the additional data, and moreover makes it automatically available to all the functions that need it, without it having to be passed as an explicit argument.

This update also makes the following changes:

I moved all the code about reflective subcategories into the subdirectory “Subcategories”, here. I also split it into three separate files, one for reflective subfibrations, one which adds the axiom for a stable factorization system, and another which adds the final axiom for a lex-reflective subcategory. (Unfortunately, that means you need three separate axioms, as at the top of this file, but at least they’re all still passed around automatically.)
I finished a proof that in the third case, the reflector preserves homotopy fibers. I think this should be a good step towards proving that it preserves all pullbacks as well, but now I really need to do some other work for a while. Along the way I had to prove the unstable 3x3 lemma and “octahedral axiom”, now in the file “FiberSequences” here.
Following discussion on the HoTT mailing list, I have changed the notation a bit. In particular, it now uses == for paths (instead of ~~>), and <~> for equivalences.
Finally, I added a file proving that with the HIT is_inhab, we obtain a stable factorization system whose right class are the monomorphisms. Since the reflective subcategory of h-propositions is certainly not lex-reflective, this means that the axioms up through a stable factorization system don’t imply that the reflector is lex.

Posted by: Mike Shulman on November 21, 2011 10:56 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Here is a simple idea for how to define cohesion. Whether or not it works out, first of all I am annoyed with myself that I fail to be able to code it in Coq. Help!

So after defining two reflective subcategories of discrete and codiscrete objects as we have discussed, I thought it might be a good idea to first set

Definition DiscType : Type := 
 { A : Type & is_discrete A }.

Definition coDiscType : Type := 
  { A : Type & is_codiscrete A }.

and then impose the axiom that the restriction of sharp to DiscType -> coDiscType exhibits an equivalence. The inverse of that equivalence precomposed with sharp would be a way to talk about flat.

Whether or not that is a good idea: how do I code that term sharpRestr : DiscType -> coDiscType?? After looking at the Coq documentation, I am trying

Definition f : DiscType -> coDiscType :=
(fun f =>  
  existT
   is_codiscrete
   ( sharp (projT1 f) )  
   ( sharp_is_codiscrete ( (projT1 f) ) ) 
).

but Coq does not like that.

Posted by: Urs Schreiber on November 21, 2011 8:15 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Ah, I have found the solution by more trial-and-error. Instead of the curly-bracket notation I have to use sigT.

Definition DiscType : Type := 
  sigT is_discrete.

Definition coDiscType : Type := 
  sigT is_codiscrete.

Why is that?

Posted by: Urs Schreiber on November 21, 2011 8:35 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Instead of the curly-bracket notation I have to use sigT… Why is that?

Ah, you have run up against the dreaded eta-equivalence. (-: The curly-bracket notation

{x:A & P x}

actually translates inside Coq to

sigT (fun x:A => P x)

rather than to sigT P. This is logical, and indeed necessary, since if you wrote something wackier like

{x:A & f (Q x y) (z x) }

then there is no P for Coq to translate it as sigT P, but it works fine to translate it as

sigT (fun x:A => f (Q x y) (z x))

Unfortunately, this causes some problems, as you have seen, because P is not identical with fun x => P x; they are “eta-equivalent” but not the same. In Coq 8.4, eta-equivalence will be built into the system, so that this problem will go away; for now you can patch your Coq by hand, or just learn to work around the issue.

Posted by: Mike Shulman on November 21, 2011 10:55 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

I have uploaded a file

https://github.com/UrsSchreiber/HoTT/blob/master/Coq/Cohesion/Cohesion.v

which implements the following simple idea:

first define two product-preserving reflections $\mathbf{\Pi}$ and $\sharp$ to discrete and to codiscrete objects, respectively. Then impose the axiom that $\sharp|_{discrete} : DiscType \to coDiscType$ is an equivalence. In terms of this define the remaining $\flat$ to be $\sharp_{discrete}^{-1} \circ \sharp$ followed by the embedding.

This is lacking one more property of $\flat$ , which may be precisely the difficult one. But it already encodes a nontrivial bit of the interplay between the two subcategories.

This is mostly for me to warm up (just reading Mike’s and Guillaume’s code is great but not enough, I need to start making little steps myself). I am not claiming that this is a great idea. It is just the idea that I ended up having after spending most of the day fighting with software. ;-)

I’ll keep playing with it. But may have to take a break now.

Posted by: Urs Schreiber on November 21, 2011 9:49 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Next week I’ll be travelling again and won’t have much time for homotopy type theory, unfortunately. (And the week after that, and the week after that, too…)

I feel I should eventually summarize in a followup entry what has happened here meanwhile, and what the next steps are.

Just briefly: instead of solving exercise II, we found a problem in the original HoTT axiomatics that we had two entries ago. But then Mike heroically fixed it all and in the course of this laid the foundations for a good bit of general higher topos theory in HoTT.

With that in hand it is now fairly straightforward to give the correct definition of the discrete reflection and then it should be fairly straightforward to solve exercise II after all.

What’s the next step, then? With the results of exercises I and II in hand, I think we have a quite nice example of a general theorem about differential cohomology proven in cohesive homotopy type theory. So next it would be good to do something more concrete: build some actual examples of cohesive $\infty$ -groups and then compute some actual (differential) cohomology groups with coefficients in them.

There is a fundamental example to consider, which will be relevant for plenty of other applications to: a line object $\mathbb{A}^1$ .

The key point is to combine now some algebra with geometric cohesion: apart from being an internal ring object (or at least an abelian group object), the type $\mathbb{A}^1$ should be characterized by being geometrically contractible, in that $\mathbf{\Pi} \mathbb{A}^1 \simeq *$ .

(More axioms to add would be: $\mathbb{A}^1$ -paths should reproduce the notion of path as implied by $\mathbf{\Pi}$ , but I don’t yet see a way to formalize this that looks particularly well suited for Coq implementation.)

Then from $\mathbb{A}^1$ one should be able to axiomatically produce the corresponding “circle group” $\mathbb{G}_m$ . Its internal deloopings $\mathbf{B}^n \mathbb{G}_m$ would then be the most fundamental cohesive $\infty$ -groups to look at.

With that one could start to see if one can compute some actual cohomology groups, such as $H^n(T^2, \mathbb{G}_m)$ and $H^n_{diff}(T^2, \mathbb{G}_m)$ , for $T$ the corresponding torus (or some other interesting cohesive space that can now be constructed).

Posted by: Urs Schreiber on November 25, 2011 10:29 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

… build some actual examples of cohesive $\infty$ -groups and then compute some actual (differential) cohomology groups with coefficients in them.

Is it just a question of formally establishing what is already known, or could new results be found? If the latter, is that with much human guidance? Coq is more a proof assistant than a prover, isn’t it?

Posted by: David Corfield on November 26, 2011 3:34 PM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise II

$MathML-enabled post (click for more details).$

Is it [the formalization of axiomatic cohesion in HoTT-Coq] just a question of formally establishing what is already known, or could new results be found?

Something that deserves to be counted as “new results” has already shown up even in the little discussion that we had so far: the attempt to put the already quite formal axioms of cohesion into the fully formal language of homotopy type theory has shed new light on the inner workings of these axioms. The extra right adjoint $\sharp$ has been found to play a more profound role than had been clear previously.

I expect more such feedback. Fundamental notions will likely benefit from being formulated in a fundamental language. To my mind there is something like the “inner workings of the universe” showing up.

The interesting aspect here is that with homotopy type theory and cohesion combined we have also a full formalization of all the structures implied by homotopy cohesion, such as differential cohomology, higher Lie theory, Chern-Weil theory, Chern-Simons functionals, geometric quantization.

The more formalized a subject is, the more people can and will contribute to it. When topological quantum field theory was more and more formalized in the last years, we saw more and more pure mathematicians starting to contribute, people who had not been brought up with the commong folk lore, who can now take the axioms at face value and run with them. Over the bridge built by the formalization.

With homotopy cohesion and its formalization in homtopy type theory, I see a bridge with a remarkably long range being built. It will allow more traffic, in both directions.

Posted by: Urs Schreiber on November 27, 2011 9:49 PM | Permalink | Reply to this

Read the post Internalizing the External, or The Joys of Codiscreteness
Weblog: The n-Category Café
Excerpt: An internal axiomatization of factorization systems, subtoposes, local toposes, and cohesive toposes in homotopy type theory, using "higher modality" and codiscreteness.
Tracked: November 30, 2011 8:48 PM

Read the post Prequantization in Cohesive Homotopy Type Theory
Weblog: The n-Category Café
Excerpt: A proposal for axiomatics of geometric prequantization formulated in cohesive homotopy type theory.
Tracked: February 27, 2012 8:20 PM

Read the post Flat Ehresmann connections in Cohesive HoTT
Weblog: The n-Category Café
Excerpt: The formalization of flat Ehresmann connections in higher geometry.
Tracked: June 28, 2012 6:36 PM

The n-Category Café

Skip to the Main Content

November 9, 2011