Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

October 26, 2011

Prequantum Physics in a Cohesive ∞-Topos

Posted by Urs Schreiber

In a few hours starts the conference

Quantum Physics And Logic 2011 .

Since beamer-talks are being required, I have prepared some slides, titled

Maybe you enjoy having a look. Comments are most welcome.

Also Joost Nuiten, whose bachelor thesis I had the pleasure to advise this year, is giving a talk, on

Posted at October 26, 2011 8:05 PM UTC

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

103 Comments & 6 Trackbacks

Re: Prequantum Physics in a Cohesive ∞-Topos

Fun! Is it worth telling the ‘Logician’ that they’ll be able to encode the physics in Univalent foundations?

On p.86 (99 of 173) and next page, presumably it should be X\int_{X}.

Hmm, is there something of the intensive/extensive business going on there?

Posted by: David Corfield on October 26, 2011 10:15 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

Is it worth telling the ‘Logician’ that they’ll be able to encode the physics in Univalent foundations?

Right, so this is something I find potentially pretty interesting. But maybe we (or “they”) are not quite there yet. A little bit is missing.

The way I see it, cohesive \infty-toposes bring a good deal of physics a considerable distance towards the realm that might reasonably be formalized in homotopy type theory. But there is still a little gap.

I was thinking that maybe the most direct way to fill the gap is to try to nail down a “cohesive \infty-Giraud theorem” that characterizes cohesive \infty-toposes entirely in terms of structure internal to them (instead by adjoint functors on them in the meta-theory). But beyond that idea, I haven’t really spend energy on this question.

On p.86 (99 of 173) and next page, presumably it should be X\int_X.

Yes, thanks! Or alternatively the previous XX should be a Σ\Sigma. I have fixed that now.

Hmm, is there something of the intensive/extensive business going on there?

I understand why you are thinking in this direction, but I still don’t see how this intensive/extensive thing helps here in this case.

But something nice is going on nevertheless: it’s the idea that I once called Integration without integration . A while back Domenico Fiorenza kindly provided the last step of a rigorous proof that I had been lacking.

Posted by: Urs Schreiber on October 26, 2011 11:55 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

How much can you do internally to your cohesive \infty-topos if all you know is that it has the “elementary” structure of an \infty-topos, and contains a subcategory of “discrete objects” which is both reflective and coreflective?

Posted by: Mike Shulman on October 27, 2011 1:38 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

David,

“intensive” and “extensive” are words from measurement theory. The standard monograph is:

Krantz, R, Suppes, P., Luce, R, Tversky, A. 1971, Foundations of Measurement.

An extensive measurement structure has a weak ordering, xyx \succeq y and a concatenation operation, xyx \circ y, and then concatenation behaves rather like addition of the values of the quantity. So, if f:Df : D \rightarrow \mathbb{R} represents the quantity, then, for all x,yDx,y \in D,

(a) f(xy)=f(x)+f(y)f(x \circ y) = f(x) + f(y)

The Representation Theorem for extensive quantities says that if (D,,)(D, \succeq, \circ) satisfies “certain conditions”, then there is a function f:(D,,)(,,+)f: (D, \succeq, \circ) \rightarrow (\mathbb{R}, \geq, +) satisfying (a) and

(b) xyx \succeq y iff f(x)f(y)f(x) \geq f(y),

and ff is unique up to multiplication by a positive real. (The function is a “measurement scale”; the transformations between scales are analogous to co-ordinate transformations in geometry.)

(see Theorem 1, p. 74, Krantz et al. The “certain conditions” are that \succeq is a weak order, \circ is weakly associative, and certain forms of monotonicity, Archimedeanness and positivity hold.)

Roughly, length is extensive because when you “concatenate” physical objects aa and bb, then the length of aba \circ b is the length of aa plus the length of bb. Temperature for example is intensive. So, if you concatenate aa and bb of the same temperature, then the temp of aba \circ b is the same as the temp of aa.

There’s a more recent monograph by Louis Narens on this material.

Jeff

Posted by: Jeffrey Ketland on October 27, 2011 3:13 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

There are many places where it would be good to see how category theoretic and other formal treatments of a topic match up. The extensive/intensive distinction would be worth investigating, even though as you see from this discussion Lawvere’s treatment is not standard yet with some category theorists.

One topic begging for alternative treatment is mereology. If we mentioned to the people here that there is a subject which studies

the relations of part to whole and the relations of part to part within a whole,

I’m sure they’d all expect some category theoretic framework would be at the heart of some suitably broad interpretation of it.

Ah, I see the philosopher Thomas Mormann is working on such a thing

I’ll show that traditional mereology does not describe parthood and composition in its full generality. My thesis is that the foundational theory of categories provides a general theory of parthood and composition (cf. Mac Lane 1986; Lawvere and Rosebrugh 2003; Lawvere and Schanuel 1996) of which standard mereology is only a tiny part.

Mormann was one of the editors of The Space of mathematics, which contains Mac Lane’s ‘The Protean Character of Mathematics’ and Lawvere’s ‘Categories of Space and of Quantity’.

Posted by: David Corfield on October 28, 2011 8:53 AM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

David,

I can’t seem to access anything by Lawvere on this issue. Do you have a link?

Does Lawvere discuss the notion of an extensive measurement structure, (D,,)(D, \succeq, \circ)? Or the representation and uniqueness theorems for these structures? There is a large literature on measurement structures and representation theorems, originating with Helmholtz and Hölder about a century ago, and now a cottage industry in parts of psychology and economics, called fundamental measurement theory. Krantz et al. 1971 is the classic (actually three volumes). Psychologists and economists are very interested in the properties of scales - ordinal, interval, etc.

Roughly, a physical quantity on a domain DD is extensive if, along with its ordering, it has some associated concatenation operation \circ, and for any scale f:Df : D \rightarrow \mathbb{R}, we have, for any x,yDx,y \in D, f(xy)=f(x)+f(y)f(x \circ y) = f(x) + f(y); so the operation \circ on DD behaves like addition on \mathbb{R}. For example, mass and length are extensive (actually, strictly speaking, they aren’t, when one includes relativity).

Is this what Lawvere means?

Mereology is, to all intents and purposes, Boolean algebra, so I assume category theorists have studied such categories and their morphisms.

Jeff

Posted by: Jeffrey Ketland on October 28, 2011 12:53 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

I don’t think there’s a definitive place he treats extensive quantities, but you can catch a discussion here. If you haven’t read Lawvere before, you may be in for a shock.

Anders Koch has been working on extensive quantities in Lawvere’s sense.

Regarding mereology, one would first look to subobjects, and then toposes. No need to expect the Boolean property in general.

Posted by: David Corfield on October 28, 2011 3:57 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

Jeff,

Thank you for your interesting comments. Speaking as someone who was competely unaware of measurement theory until your posts, it looks to me that measurement theory could use some category theory.

For example, we learn on p. 3 of Measurement, theory of that

“A key concept in the theory of measurement is that of a representation, which is defined to be a structure preserving map…”

Sounds like “representation” is a functor, doesn’t it.

Posted by: Eugene Lerman on October 28, 2011 4:29 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

Eugene, thanks - yes, as far I understand the suggestion. So, Lawvere is saying that, for example, the mass-in-g scale m gm_{g} and the mass-in-kg scale m kgm_{kg} are covariant functors. Is that it?

(Measurement theory is usually done by mathematical psychologists and economists; hence the lack of disciplinary overlap.)

Jeff

Posted by: Jeffrey Ketland on October 29, 2011 5:19 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

The most basic idea is that the assignment of the set of functions to a space for some set of values, RR, is contravariant. So if f:XYf: X \to Y is a function between two spaces, there is an induced map R YR XR^Y \to R^X. For example, if ff is the vertical projection map of a room down to the floor, then for every RR-valued function on the floor, I can induce an RR-valued function on the room by taking the value of the new function at any point to be the value of the old function at the projection.

Distributions on XX form some subset of R R XR^{R^X}, since a distribution maps functions, R XR^X, to RR. The functor which sends a space to the set of distributions is covariant. Integration over the room with respect to a measure will be sent to integration over the floor with respect to the induced measure.

The first of these paragraphs describes the intensive quantities; the second the extensive quantities. See how they behave on the terminal morphism X1X \to 1. For intensive quantities, any function on 11, i.e., any value rRr \in R, gives rise to the constant function on XX with value rr. For extensive quantities, any distribution on XX is sent to a distribution on 11, i.e., a (linear) map from functions on 11, or in other words RR, to RR. These themselves correspond to values of RR, and are the total of the extensive quantity on XX.

Posted by: David Corfield on October 30, 2011 4:56 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

Thanks, David. I still don’t quite get the connection between what you’ve said and the notions of extensive/intensive quantity in (Krantz et al.-style) measurement theory. But I have a fairly strong inkling that measurement structures, and scales for them, is not what is meant here!

Jeff

Posted by: Jeffrey Ketland on October 30, 2011 9:50 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

How much can you do internally to your cohesive \infty-topos if all you know is that it has the “elementary” structure of an \infty-topos, and contains a subcategory of “discrete objects” which is both reflective and coreflective?

That would already go a long way. Essentially all the differetial-geometry-type structures appear from just this.

The extra axioms mainly serve to fine-tune the behaviour of these structures (for instance making the de Rham coefficient object Π dRX\mathbf{\Pi}_{dR}X satisfy not just some but all the axioms of a de Rham schematic homotopy type).

One exception is the integration theory: in order to properly have integration of differential cocycles on internal moduli stacks, one needs concretification, hence the fact that also the codiscrete objects are reflectively embedded.

So now I am interested why you are asking. Can you say “reflective and coreflective embedding” in HoTT?

Posted by: Urs Schreiber on October 27, 2011 4:22 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

Of course I am freely making use of the \infty-Giraud-axioms in all of this. I’d have to think a little to disentangle where exactly these axioms are used and what would break if they weren’t there.

Posted by: Urs Schreiber on October 27, 2011 4:27 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

Can you say “reflective and coreflective embedding” in HoTT?

Yes, I think so. I’m thinking of adding the following axioms:

is_discrete : Type -> Type.

is_discrete_is_prop : forall X, is_prop (is_discrete X).

pi : Type -> Type.

pi_is_discrete : forall X, is_discrete (pi X).

map_to_pi : forall X, X -> pi X.

pi_is_reflection : forall X Y, is_discrete Y ->
               is_equiv (fun f : pi X -> Y => f o (map_to_pi X)).

flat: Type -> Type.

flat_is_discrete : forall X, is_discrete (flat X).

map_from_flat : forall X, flat X -> X.

flat_is_coreflection : forall X Y, is_discrete Y ->
                   is_equiv (fun f : Y -> flat X => (map_from_flat X) o f).

The first two say we have a property of types called is_discrete. The types satisfying this form our full subcategory.

Then we have an operation on types which assigns to every type X a type pi X, which is discrete, and comes equipped with a map from X. Moreover, if Y is discrete, then the induced map from Hom(piX,Y)Hom(pi X, Y) to Hom(X,Y)Hom(X,Y) is an equivalence. This should say that pi X is a reflection of X into the discrete objects.

Finally we have the dual operation flat which is the coreflection.

Of course I am freely making use of the \infty-Giraud-axioms in all of this.

The main issue still remaining there, I think, is exactness. We have yet to decide how to formalize the notion of “groupoid object” so that we can take its quotient. Probably you are using such exactness in e.g. constructing classifying spaces?

Posted by: Mike Shulman on October 28, 2011 2:56 AM | Permalink | PGP Sig | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

Just for fun, I’ve basically copy-pasted these axioms and they type-check, hurray :)

https://github.com/0x01/HoTT/blob/05db0bca04e5ffecf0f559940934f22b915c28fc/Coq/Cohesive.v

(this includes Π()=\mathbf{\Pi}(\star) = \star)

Posted by: Jelle on October 28, 2011 4:12 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

Just for fun, I’ve basically copy-pasted these axioms and they type-check, hurray :)

https://github.com/0x01/HoTT/blob/05db0bca04e5ffecf0f559940934f22b915c28fc/Coq/Cohesive.v

Hi Jelle,

we talked a lot this evening, that was great for me!

Just for the record and so that people here see it, too, I’ll record some things that I or we have said tonight.

First, thanks for creating the above file Coq/Cohesive.v ! This makes me see a whole new perspective here.

Now that the file exists, I feel like it should be enhanced a bit. I am not sure how to go about it, practically, but the following would be nice to have.

Commentary

There should be some commentary, so that humans can understand what it is that the code is trying to achieve. I’ll try to write up something and then send it to you.

Remaining axioms

There should be a warning that there are more axioms, at least one of them mandatory.

Namely what seems to be missing at the moment is the information that the reflector of flatflat is the coreflector of pipi. In other words, what the code currently axiomatizes is, I think, the situation

{HΓDiscΠB;HcoDiscΓ˜B; HΠ( H)} \left\{ \mathbf{H} \stackrel{\overset{\Pi}{\to}}{\stackrel{\overset{Disc}{\hookleftarrow}}{\underset{\Gamma}{\to}}} \mathbf{B} \,; \mathbf{H} \stackrel{\overset{\tilde \Gamma}{\to}}{\underset{coDisc}{\hookleftarrow}} \mathbf{B} \,; *_{\mathbf{H}} \stackrel{\simeq}{\to}\Pi(*_{\mathbf{H}}) \right\}

but what is missing is the information that here Γ=Γ˜\Gamma = \tilde \Gamma.

I need to think about how to say that best in terms of the units/counits that are axiomatized in the file. Probably one should state some of the properties of an adjoint quadruple as an extra axiom.

Question (to whoever might know)

What does HoTT already know about adjoints? The axioms so far must imply that pipi preserves homotopy colimits and that flatflat preserves homotopy limits. Both these statements are crucial for deriving some central consequences of cohesion. What’s the status of this?

Posted by: Urs Schreiber on October 28, 2011 10:28 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

I wrote:

There should be some commentary, so that humans can understand what it is that the code is trying to achieve. I’ll try to write up something and then send it to you.

I have added this now to the nnLab entry cohesive (∞,1)-topos.

In fact, I have split the Definition-section there into three subsections:

  1. external definition;

  2. internal definition;

  3. internal definition formulated in HoTT.

In 2. I have included the relevant statement that the internal formulation is indeed equivalent to the external one. In 3. I have added some commentary and the codicsrete reflective subcategory.

Missing in the internal description is still the condition that Γ=Γ˜\Gamma = \tilde \Gamma. But I have to quit now and continue tomorrow.

Posted by: Urs Schreiber on October 29, 2011 12:05 AM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

I wrote:

Question (to whoever might know)

What does HoTT already know about adjoints? The axioms so far must imply that pi preserves homotopy colimits and that flat preserves homotopy limits. Both these statements are crucial for deriving some central consequences of cohesion. What’s the status of this?

There’d be more such elementary facts which would now be useful to have realized in HoTT in order to start deducing structure from cohesion.

For instance, what does HoTT/Coq already know about fiber sequences?

Because the next step towards the construction of differential cohomology in HoTT is the construction of the ∞-Maurer-Cartan form.

This involves the following two steps.

First we define for every pointed connected object (type) BGBG the morphism

map_from_flatdR : flatdR BG -> flat BG

as the homotopy fiber of

map_from_flat : flat BG -> BG ,

which exists by one of the axioms.

Then we deduce that the next homotopy fiber is of the form

canonical_form : G -> flatdr BG,

where G is the loop space object of BG.

This morphism has the interpretation of the canonical (Maurer-Cartan) form on G.

How would we teach Coq about this story?

Posted by: Urs Schreiber on October 29, 2011 9:33 AM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

VV theory about fiber sequences is here:
https://github.com/vladimirias/Foundations/blob/master/Generalities/uu0.v

The double fibration is there too.

Posted by: Bas Spitters on October 31, 2011 1:39 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

VV theory about fiber sequences is here:

https://github.com/vladimirias/Foundations/blob/master/Generalities/uu0.v

Thanks! I have added a link to it at nLab:fiber sequence.

(By the way, for both browser on my machine, when I point to this file, they crash…)

Posted by: Urs Schreiber on October 31, 2011 2:52 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

what is missing is the information that here Γ=Γ˜\Gamma = \tilde{\Gamma}.

You confused me for a minute, because the axioms I wrote down didn’t say anything about codiscrete objects yet. But I see that you added corresponding axioms to the nLab page.

As for the question you pose, since this data gives us an adjunction between the discrete objects and the codiscrete ones (the left adjoint being the restriction of conc and the right adjoint the restriction of flat), would it be enough to demand that that adjunction is an equivalence of categories? Which we could do, of course, by asserting that its unit and counit are equivalences.

What does HoTT already know about adjoints?

Not much. As far as I know, no one has thought about (co)reflective subcategories of Type before. But the facts you cite should be straightforward to prove….

what does HoTT/Coq already know about fiber sequences?

Here the answer is: a fair bit. Some basic facts about fiber sequences are here. I think probably Voevodsky has proven more than this, but I don’t know my way around his Coq files, so I can’t point you directly to them.

Posted by: Mike Shulman on October 29, 2011 10:01 PM | Permalink | PGP Sig | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

As for the question you pose, since this data gives us an adjunction between the discrete objects and the codiscrete ones (the left adjoint being the restriction of conc and the right adjoint the restriction of flat),

I thought that’s what is missing in the code currently, an axiom that makes conc and flat be related in any way. We want them to form an adjunction, yes, but it seems to me that this information still needs to be added to the Coq code in some way.

Posted by: Urs Schreiber on October 30, 2011 10:42 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

an axiom that makes conc and flat be related in any way. We want them to form an adjunction, yes, but it seems to me that this information still needs to be added to the Coq code in some way.

We have a coreflective subcategory DiscDisc, with flat the coreflector, and a reflective subcategory CodiscCodisc, with conc the reflector. (What does conc stand for, by the way? My initial impulse was to call that functor coarse.) So we have a composite adjunction

DiscflatHconcCodisc Disc \;\underset{flat}{\rightleftarrows}\; \mathbf{H} \;\overset{conc}{\rightleftarrows}\; Codisc

no?

Posted by: Mike Shulman on October 31, 2011 1:23 AM | Permalink | PGP Sig | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

no?

Now I understand what you mean, sorry for being slow.

And maybe I am still slow: certainly we want it be implied that this composite adjunction is an equivalence. But why is that sufficient for the condition that I denoted ΓΓ˜\Gamma \simeq \tilde \Gamma?

What does conc stand for, by the way?

It was supposed to mean “concrete”. Because the image factorization of the corresponding unit is concretification. But I keep looking for a better term. Maybe coarse is indeed better. I wish I had a term that would harmonize more with “Π\Pi” and “\flat”, though.

Posted by: Urs Schreiber on October 31, 2011 6:22 AM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

But why is that sufficient for the condition that I denoted ΓΓ˜\Gamma\simeq \tilde{\Gamma}?

Well, I think there’s an inaccuracy in the diagram you drew back here: nothing we have so far guarantees that the category B\mathbf{B} occurring in the functors Π\Pi, DiscDisc, and Γ\Gamma is the same as the category B\mathbf{B} occurring in the functors coDisccoDisc and Γ˜\tilde{\Gamma}. Asking that the composite adjunction be an equivalence gives us a canonical way to identify these two categories, and under that identification, I believe it should be the case that ΓΓ˜\Gamma \simeq \tilde{\Gamma}.

I wish I had a term that would harmonize more with “Π\Pi” and “\flat”, though.

Well, the obvious dual of \flat is \sharp

Posted by: Mike Shulman on October 31, 2011 8:23 PM | Permalink | PGP Sig | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

Oops! My bad. You’re right, there is another condition necessary.

For any type XX, we have a canonical composite map XXX. \flat X \to X \to \sharp X. Under the adjunction (discrete objects)(codiscrete objects) (\text{discrete objects}) \underoverset{\flat}{\sharp}{\rightleftarrows} (\text{codiscrete objects}) this corresponds to maps XX\flat X \to \flat \sharp X and XX\sharp\flat X\to \sharp X. The necessary condition is that these two maps always be equivalences.

(The condition that the above adjunction is an equivalence is equivalent to saying that these two maps are equivalences when XX is discrete or codiscrete—or that for any XX, one is an equivalence iff the other one is.)

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

Re: Prequantum Physics in a Cohesive ∞-Topos

Well, the obvious dual of \flat is \sharp

Good point. I like that.

The necessary condition is that these two maps always be equivalences.

I see now. That looks good.

It’s too late for me tonight. But hopefully tomorrow I find a free minute to use this to complete the HoTT formulation of the axioms in the nnLab entry. Thanks!

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

Re: Prequantum Physics in a Cohesive ∞-Topos

I have written out details of the above internal formulation of cohesion at nLab:cohesive (∞,1)-topos – internal definition .

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

Re: Prequantum Physics in a Cohesive ∞-Topos

Now I am trying to write the remaining Coq code for the axioms (here). Is the following valid code that does what I expect it to do:

Axiom codiscrete_respects_discrete : forall X, is_equiv ( hash ( map_from_flat X ) )

Axiom discrete_respects_codiscrete : forall X, is_equiv ( flat ( map_to_hash X ) )

?

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

Re: Prequantum Physics in a Cohesive ∞-Topos

The usual pronunciation of \sharp in English is “sharp”, so I changed “hash” to “sharp” in your Coq code. (Now I’m afraid some Brit is going to step in and tell me that they pronounce it “hash”, but I checked on Wikipedia and it didn’t mention any other names…)

Your axioms codiscrete_respects_discrete and discrete_respects_codiscrete are almost right, I think, but not quite, because as it stands flat and sharp are not functors on the category of types, only on the space (=type) of types (namely, Type), so you can’t apply them to noninvertible maps. (Even if you were applying them to invertible maps, i.e. paths in Type, you’d need to notate that somehow; the HoTT files use map f ... for the action of a function f on paths.)

Of course, because they are reflectors, their functorial structure can be defined in a canonical way, but we haven’t done that yet. Because I was feeling lazy, I just added functor_map in front of them on the nLab page.

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

Re: Prequantum Physics in a Cohesive ∞-Topos

The usual pronunciation of ## in English is “sharp”

I know. But I didn’t like that!

Because the word “sharp” also invokes geometric associations (in me, at least), and these are (in me, at least) almost directly opposite to the geometric intuition to be modeled by objects of the form coDiscAcoDisc A. These objects are “maximally smooth” in a sense, and have nothing “sharp” (kinky) about them at all.

But with “hash” one can almost pretend that it actually captures the mashed and dizzy feeling of these objects.

Do you see what I mean? Is there at all a chance that it appears reasonable to change it back to “hash”?

as it stands flat and sharp are not functors on the category of types, only on the space (=type) of types (namely, Type)

Ah, I see. I was wondering to which extent functoriality is implicit. But what you say here of course makes a lot of sense, now that you say it.

Because I was feeling lazy, I just added functor_map in front of them on the nLab page.

All right, so how do I have to think about that now? This functor_map is some thing (“procedure”? “function”?) that would still have to be coded before Coq would accept the code now on the nnLab page? Or it has already been coded and would just have to be read in from some library file?

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

Re: Prequantum Physics in a Cohesive ∞-Topos

Why was \flat chosen for the other map? What is the intuition behind that map?

Posted by: David Corfield on November 2, 2011 6:49 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

Why was \flat chosen for the other map? What is the intuition behind that map?

Because it produces coefficient objects for flat \infty-connections.

For GG an \infty-group, BG\mathbf{B}G the moduli \infty-stack of GG-principal \infty-bundles, we have that BG\mathbf{\flat} \mathbf{B}G is the moduli \infty-stack of GG-principal \infty-bundles equipped with flat \infty-connection.

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

Re: Prequantum Physics in a Cohesive ∞-Topos

Is there at all a chance that it appears reasonable to change it back to “hash”?

Well, I would find it extremely confusing to have two dual objects, one notated by \flat and one by \sharp, but where one is pronounced “flat” and the other pronounced “hash”. I’d be interested to hear others’ reactions. The word “sharp” doesn’t have bad associations for me; I can see that one might in theory describe a space with kinks as being “sharp”, but I’ve never actually heard the word used that way in mathematics.

Nor does the word “sharp” as used to pronounce the symbol \sharp naturally bring up connotations of pointiness for me, any more than pronouncing \flat makes me think of a level surface. Perhaps there is an etymological connection, but in my mind they are just homophones. The use of \flat to relate to flat connections is a clever pun, but not an association that would naturally have occurred to me.

This functor_map is some thing (“procedure”? “function”?) that would still have to be coded before Coq would accept the code now on the nLab page?

Yes. But what I wrote isn’t actually ever going to compile literally, because in order to define the action of (say) flat on functions, we’re going to have to make use of map_from_flat and flat_is_coreflection as well. So really it’s a single function flat_map rather than an application functor_map flat that’ll have to be defined.

One could, however, define a general function which associates to any reflective subcategory of Type, specified in the way we’ve been doing, its action on functions, and then apply that to all of our examples.

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

Re: Prequantum Physics in a Cohesive ∞-Topos

The word “sharp” doesn’t have bad associations for me

By the way, it would be different if we were using it as an adjective for the spaces in question. I wouldn’t want to say that codiscrete spaces are “sharp spaces”. But using it to name the reflector into codiscrete spaces doesn’t bother me.

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

Re: Prequantum Physics in a Cohesive ∞-Topos

The word “sharp” doesn’t have bad associations for me

By the way, it would be different if we were using it as an adjective for the spaces in question. I wouldn’t want to say that codiscrete spaces are “sharp spaces”.

Ah, goot to hear. Then we share the same feeling here, to some extent, after all.

But using it to name the reflector into codiscrete spaces doesn’t bother me.

Okay, I see. But then, once we say “sharp” for the functor ##, we will inevitably pronounce “#X# X” as “sharp X”. But it should be pronounced “mushy X”!

(Now “hash” is not “mush”, but there is a meaning where both are close, right?)

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

Re: Prequantum Physics in a Cohesive ∞-Topos

But then, once we say “sharp” for the functor \sharp, we will inevitably pronounce “X\sharp X” as “sharp X”

Yes. But pronouncing it “sharp X” doesn’t mean that it is sharp in the pointy sense, only that the functor called \sharp and pronounced “sharp” has been applied to it. There isn’t any sense in which the note CC\sharp is “pointier” than the note CC; it’s just had the operation called “sharp” applied to it.

By the way, it took me a while to realize that your “hash” was a pronunciation of the symbol #. In America we usually call that a number sign. But regardless, it is a different symbol from \sharp.

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

Re: Prequantum Physics in a Cohesive ∞-Topos

I realize now that “sharp” is a great name for the right adjoint to \flat, after all.

I said above that I was unhappy with it because the objects A\sharp A are far from having a “sharp” feel to them. This is true, but besides the point. Also the objects A\flat A are far from having a flat feel to them. Instead, they are moduli spaces for things that do! The homotopy fibers of maps XAX \to \flat A do have a flat feel to them, because they are locally constant over XX.

Similarly, the homotopy fibers of maps XAX \to \sharp A do indeed generically have a “sharp” feel to them: because these are fiber bundles whose fibers may jump around discontinuously (dis-cohesively, to be precise ;-). So the generic such space classified by A\sharp A is all kinky and pointed. The association with “sharp” makes good sense, therefore.

Just thought I’d post this remark, for the record.

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

Re: Prequantum Physics in a Cohesive ∞-Topos

Ah, wonderful! I had a vaguely similar thought this morning after your reference to “sharp logic” — since the sharp logic is “external”, it enables us to make distinctions which the ordinary internal logic, being restricted to pullback-stable things, can’t do. Thus it is “sharp” in that it is able to cut apart more things. (-:

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

Re: Prequantum Physics in a Cohesive ∞-Topos

the parenthetical remark

only on the space (=type) of types (namely, Type)

made me think that there should be a dictionaty

Coq \leftrightarrow (,1)(\infty,1)-category theory ,

and so I made the plan to start one. But I didn’t get far beyond making the plan itself and have to run now to meet people for dinner. But maybe it would be both fun and useful to expand the list I have started there (and correct it!)

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

Re: Prequantum Physics in a Cohesive ∞-Topos

I proved (rigorously I think, except the few parts where I haven’t proved what should be a definitional equality) that (homotopy) pullbacks and pushouts are indeed what one can think they are (see here for the code):

The pullback of f:ACB:gf:A\to C\leftarrow B:g is the type of the triples (a,b,p) where a is of type A, b is of type B and p is a path between f a and g b.

The pushout of g:ACB:fg:A\leftarrow C\to B:f is the higher inductive type defined by :

Inductive hopushout :=
  | inl : A -> hopushout
  | inr : B -> hopushout
  | glue : forall x : C, inl (g x) ~~> inr (f x).

I do not have the time to put it in the nLab now but I’ll do it in a few hours, after my algebraic topology class.

Posted by: Guillaume Brunerie on November 3, 2011 3:23 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

I proved (rigorously I think, except the few parts where I haven’t proved what should be a definitional equality) that (homotopy) pullbacks and pushouts are indeed what one can think they are (see here for the code):

Interesting!

I started looking at it, but need to look at it again.

Just one meta-question, so that I get a better idea of the state of the art: does this mean that neither homotopy pullbacks nor homotopy pushouts had been Coq-coded previously, say by Voevodsky? Are you doing something new here or improving on something that already existed?

The pushout of g:ACB:fg : A \leftarrow C \to B : f is the higher inductive type defined by :

Inductive hopushout := | inl : A -> hopushout | inr : B -> hopushout | glue : forall x : C, inl (g x) ~~> inr (f x).

That is certainly a pleasing statement.

Two related questions:

Is there, for Coq, a technical difference between “inductive type” and “higher inductive type”? Or is it just that the latter uses code form the Homotopy-library?

Should there also be “higher coinductive types” and a similar formula for homotopy pullbacks in terms of higher coinductive types? I mean, is it conceivable that Coq could be extended to know about a notion of coinductive types?

I do not have the time to put it in the nLab now but I’ll do it in a few hours, after my algebraic topology class.

I have added pointers to your code to the References sections of the nnLab entries homotopy limit, (infinity,1)-limit and homotopy pullback.

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

Re: Prequantum Physics in a Cohesive ∞-Topos

does this mean that neither homotopy pullbacks nor homotopy pushouts had been Coq-coded previously

Homotopy pullbacks have been used extensively in all current developments, whether or not there was a unified name for them. The homotopy fiber, used in defining equivalences, is a special case.

The definition of homotopy pushouts as a higher inductive type (HIT) was proposed here.

Is there, for Coq, a technical difference between “inductive type” and “higher inductive type”?

Yes! As explained at that same post, Coq has had built-in inductive types for a long time, but higher inductive types are a very new invention by homotopy-type-theorists and are not built into Coq yet; we have to add them as axioms. Higher inductive means that we can have constructors such as glue which output a path (or a higher path), rather than a point.

Should there also be “higher coinductive types” and a similar formula for homotopy pullbacks in terms of higher coinductive types?

There should be higher coinductive types. But they aren’t what you’re thinking; the difference between inductive and coinductive types only arises when you include recursive constructors (which take input coming from the type being defined). A non-recursive inductive definition, higher or otherwise, like the homotopy pushout, will be exactly the same if you called it a coinductive definition.

Limits and colimits are very not-dual in terms of their formulation in HoTT. Which makes sense because they are very not-dual in terms of their behavior in toposes.

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

Re: Prequantum Physics in a Cohesive ∞-Topos

Homotopy pullbacks have been used extensively in all current developments, whether or not there was a unified name for them. The homotopy fiber, used in defining equivalences, is a special case.

The definition of homotopy pushouts as a higher inductive type (HIT) was proposed here.

Ah right, of course, I should have remembered. Thanks for reminding me.

To help my memory, and help others not following the nnCafé discussions, I am trying to add all this kind of information in a structured way to the nnLab.

So there is now a remark at nLab:homotopy pullback. Please expand as necessary!

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

Re: Prequantum Physics in a Cohesive ∞-Topos

Just one meta-question, so that I get a better idea of the state of the art: does this mean that neither homotopy pullbacks nor homotopy pushouts had been Coq-coded previously, say by Voevodsky? Are you doing something new here or improving on something that already existed?

As Mike said, people have been using homotopy pullback for a long time (the loop space of a type is a homotopy pullbacks), and the definition of homotopy pushout was proposed in the sixth post of Mike. What I have done is just the (more or less) straightforward verification that the universal property is indeed satisfied.

In Vladimir Voevodsky’s files, there is a section “Homotopy fiber squares”, so perhaps he has already proved it (for homotopy pullbacks), but his Coq code is rather hard to read so I’m not sure.

Posted by: Guillaume Brunerie on November 4, 2011 7:27 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

What I have done is just the (more or less) straightforward verification that the universal property is indeed satisfied.

Okay, thanks. That is of course crucial! And crucial information for me, too.

As my above “meta-question” and the reactions to it maybe demonstrate: I feel that the Coq-HoTT project is badly lacking a good public documentation. After talking to my new local Coq-experts, I realize that there is loads of information that I need, but which I have no chance to find by searching around on the web.

Eventually there should be a Wiki that soaks up all the available information and cristallizes it out in useful structured form.

I consider myself lucky that I have now next to me a printout of

HoTT-Coq-code.pdf

thanks to Jelle Herold. That already answers lots of question which I had in the other thread.

Chapter 2 “Paths” reads like a tale of black and powerful magic. Of course I have heard about this, and how it is the source of all the excitement, but seeing it happen explicitly with the code here is just so amazing.

What I am trying to understand next is the detailed way in which the formal proofs of those Lemmas in chapter 2 work. I was looking today at the Coq-output for these proofs, but I still need to wrap my mind around what’s actually happening (and to parse all the lengthy expressions that appear in the course of the proofs).

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

Re: Prequantum Physics in a Cohesive ∞-Topos

I feel that the Coq-HoTT project is badly lacking a good public documentation.

Well, don’t judge it too harshly – the project is really still in its infancy! More documentation would certainly be helpful, but we don’t want to spend a long time polishing and documenting any current version of the code when it may be replaced entirely by next year.

For instance, perhaps instead of the “paths” type used by the HoTT library, we should be using Coq’s built-in identity type, which works with Coq’s rewrite tactic. That may make a lot of the tactics in chapter 2 unnecessary. I think Voevodsky’s files are now doing the latter, although I haven’t looked at them for a while (too much unrelated stuff to do).

I think the same goes for the idea of a “natively homotopical” proof assistant – once the ideas of what such a thing ought to look like settle down some, it might be worth trying to implement one. In the meantime, Coq and Agda are mature and powerful and basically sufficient for almost everything we need, even if there are a few notational quirks that one has to get used to. Getting used to them is even a good thing, I think, because it helps educate one in the way type theorists think.

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

Re: Prequantum Physics in a Cohesive ∞-Topos

VV has Paths as a Notation for identity.
It solves a lot a problems.

Posted by: Bas Spitters on November 10, 2011 10:14 AM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

Well, don’t judge it too harshly – the project is really still in its infancy!

Okay, sure. Just a bit of frustration on my side showing through. I should simply continue to quiz you and others as much as possible! :-)

More documentation would certainly be helpful, but we don’t want to spend a long time polishing and documenting any current version of the code when it may be replaced entirely by next year.

This is something I was worrying about and asked somebody about today: is code that builds on the currently existing HoTT libraries and their implementation risking to be not forward compatible rather sooner than later? How do you deal with this?

For instance, perhaps instead of the “paths” type used by the HoTT library, we should be using Coq’s built-in identity type

That’s another thing I was asking somebody else about today. What’s the difference between the two? Is it (just?) that paths is an implementation by an inductive type of the idea that identity implements without inductive types?

I think Voevodsky’s files are now doing the latter, although I haven’t looked at them for a while (too much unrelated stuff to do).

I have a vision of a blog or something analogous to the nnForum where one could post under a “latest changes”-category messages like “Uploaded new version of xyz.v, switched from using paths to using identity.” Inconceivable? It’s such a small community, it would help so much.

I think the same goes for the idea of a “natively homotopical” proof assistant – once the ideas of what such a thing ought to look like settle down some

I can believe that. I just hope that somebody spends some thoughts on forward compatibility. It would be a pity if much of work on HoTT coding would have to be redone once these ideas have settled down.

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

Re: Prequantum Physics in a Cohesive ∞-Topos

Urs wrote

I have a vision of a blog or something analogous to the nForum where one could post under a “latest changes”-category messages like “Uploaded new version of xyz.v, switched from using paths to using identity.” Inconceivable? It’s such a small community, it would help so much.

Do you mean like this?

Posted by: David Roberts on November 10, 2011 2:13 AM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

Do you mean like this?

Ah, yes, that looks perfect, much better even than what I had envisioned.

But now I am confused: since all homotopy typers are already “on” GitHub, does this mean this collaboration infrastructure (HoTT Wiki, HoTT Code Review, etc.) is already in place, in principle? And just not used?

From https://github.com/plans it seems that even the 0 dollar plan counts as a plan and hence “comes with Wikis, Issues, Downloads, Pages & more”.

?

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

Re: Prequantum Physics in a Cohesive ∞-Topos

this collaboration infrastructure (HoTT Wiki, HoTT Code Review, etc.) is already in place, in principle? And just not used?

I guess you could say that. You seem to have a vision of “homotopy typers” as a much more coherent (dare I say “cohesive”?) group of people than I think is actually the case.

is code that builds on the currently existing HoTT libraries and their implementation risking to be not forward compatible

Yes. In fact, I think it’s nearly certain that such code is definitely not going to be forward compatible. Forward compatibility is something that you worry about with release versions of software. I think currently we are in development mode. Or even earlier.

Actually, forward compatibility is a serious issue with all formalized proof. Even in plain ordinary Coq, proof scripts can break when the system is upgraded. Say you wrote induction; auto. and saw that auto solved three of the five subgoals generated by induction, then went on to prove the other two manually. Then in the next version of Coq, auto is improved so that now it solves four of your five subgoals. The proof script is going to break.

Some people say the way to deal with this is to write better-structured proof scripts which break in comprehensible ways when this happens, so you can easily see what went wrong and fix it quickly. Other people say you should put your effort into designing powerful custom tactics which don’t break as much as when you write more manual proofs. I don’t think there is a universally accepted solution yet.

How do you deal with this?

Personally, I take a deep breath and control my impatience. (-:

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

Re: Prequantum Physics in a Cohesive ∞-Topos

I get it, thanks. Evident as it may seem to you, that was very useful information.

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

Re: Prequantum Physics in a Cohesive ∞-Topos

That’s another thing I was asking somebody else about today. What’s the difference between the two? Is it (just?) that paths is an implementation by an inductive type of the idea that identity implements without inductive types?

No, identity is also implemented with an inductive type, but it’s a Prop (in the sense of the calculus of constructions) and nobody knows what happen when you mix the calculus of constructions with HoTT. So far everybody has been working with Martin-Löf type theory as the base theory (which is a subset of the calculus of constructions).

Vladimir Voevodsky is using a modified version of Coq where Coq’s builtin identity is no longer a Prop (and identity A is in a bigger universe than A).

Posted by: Guillaume Brunerie on November 10, 2011 10:48 AM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

No, identity is also implemented with an inductive type, but it’s a Prop (in the sense of the calculus of constructions) and nobody knows what happen when you mix the calculus of constructions with HoTT.

Let me see if I am following this. So paths is defined simply as

Inductive paths {A} : A -> A -> Type 
  := idpath : forall x, paths x x.

And that’s it. Right?

What about

Inductive identity {A} : A -> A -> Prop 
  := refl : forall x, identity x x.

Is that the definotion of identity?

I have been exposed to this definition of identity types. Are these rewrite rules those generated automatically for an inductive type as above?

I looked at the induction rule that Coq generates for the inductive definition of paths yesterday. It seemed to say that “if a proposition holds for an identity path, then it holds for any path”. That confused me.

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

Re: Prequantum Physics in a Cohesive ∞-Topos

Let me see if I am following this. So paths is defined simply as

Inductive paths {A} : A -> A -> Type 
  := idpath : forall x, paths x x.

And that’s it. Right?

Yes.

What about

Inductive identity {A} : A -> A -> Prop 
  := refl : forall x, identity x x.

Is that the definotion of identity?

This would probably work but I think that the definition of identity is simply

Inductive identity {A : Type} (a b : A)
  := refl : forall (x : A), identity x x.

There is no explicit reference to Prop here, but in the calculus of inductive constructions (calculus of constructions + inductive types), an inductive type with exactly one constructor is automatically a Prop. The intuition is that if there is only one constructor (as with identity), then the only thing that matters is whether the type is inhabited or not, the nature of the terms is not relevant, nobody cares about how a and b are equal, knowing that they are equal is enough.

Of course this is completely at the opposite of the HoTT intuition of the identity types, so we must be careful when mixing the two.

The definition of paths with type A -> A -> Type (instead of having two arguments of type A) is a workaround to bypass this property of inductive types with only one constructor (apparently it does not apply to inductive families defined directly with type X -> Type)

I have been exposed to this definition of identity types. Are these rewrite rules those generated automatically for an inductive type as above?

Yes.

I looked at the induction rule that Coq generates for the inductive definition of paths yesterday. It seemed to say that “if a proposition holds for an identity path, then it holds for any path”. That confused me.

Yes, this is more or less what it says (except that the proposition must hold for every identity path, was this a typo?). And the elimination rule written in the nLab also says the same thing. It is also compatible with the intuition that the paths type is inductively generated by the identity paths, so it is enough to know something about the identity paths in order to know it for any path.

But keep in mind that it can be applied only if you already have a proposition that makes sense for any path. For example the fact that every path x ~~> x is equal to the identity path is true for the identity paths but there is no way to extend this property into a property of any path (because you can’t talk about the identity path of type x ~~> y), so we cannot use the elimination rule here and loop spaces don’t have to be trivial.

Posted by: Guillaume Brunerie on November 10, 2011 12:09 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

I realize that I need to come back to this issue here about how to think about the induction rule for paths. I had persuaded myself that I understand its “meaning”, but now I realize that I still don’t.

Here a concrete question:

Mike in his files defines the type circle and proves an equivalence between paths circle base base and int.

Question: why does the path induction rule thereby not imply that a proposition about all integers that is true for 0 is true for every single integer?

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

Re: Prequantum Physics in a Cohesive ∞-Topos

why does the path induction rule thereby not imply that a proposition about all integers that is true for 0 is true for every single integer?

An excellent question! The reason is that such a proposition, when transferred over to circle base base, is not sufficiently general for the path induction rule to apply to it. The path induction rule only applies to a proposition P(x,y,p)P(x,y,p) that makes sense for any two points x,yx,y and any path p:xyp\colon x \rightsquigarrow y. A proposition that is only about endo-loops of base cannot be proven by path-induction.

So it’s essentially the same reason why you cannot prove “3 is prime” by ordinary mathematical induction. (-:

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

Re: Prequantum Physics in a Cohesive ∞-Topos

The path induction rule only applies to a proposition P(x,y,p)P(x,y,p) that makes sense for any two points x,yx,y and any p:xyp : x \rightsquigarrow y. A proposition that is only about endo-loops of base cannot be proven by path-induction.

But circle only has a single point! So to my mind, what you say here (which is essentially what Guillaume said before) does not address the confusing point that I mentioned. Do you see what I mean?

Allow me to propose the following different way of “explaining” in words what’s going on.

The situation is easy to understand in the model of HoTT in Kan complexes. There paths A is A Δ[1]A^{\Delta[1]}. The key point is that this is of course very different from the pullback paths A x x = Ω xA\Omega_x A

Ω xA x A Δ[1] A x A \array{ \Omega_x A &&\to&& * \\ \downarrow &&&& \downarrow^{\mathrlap{x}} \\ \downarrow && A^{\Delta[1]} &\to& A \\ \downarrow && \downarrow \\ * &\stackrel{x}{\to}& A }

even if AA just has a single vertex xx. The difference is not in the points in both cases, but in the equivariance at these points.

In particular for the circle A=circle=S 1=BA = circle = S^1 = \mathbf{B}\mathbb{Z} we have

pathsA=A Δ[1]=//(×) paths A = A^{\Delta[1]} = \mathbb{Z}//(\mathbb{Z}\times \mathbb{Z})

but

Ω baseA=. \Omega_{base} A = \mathbb{Z} \,.

The objects are the same: integers in both cases. A proposition about A Δ[1]A^{\Delta[1]} (a morphism to the object classifier Kan complex) makes a statement about all paths in AA just as a proposition about paths A x x does. The difference is instead in the equivariance: a proposition about A Δ[1]A^{\Delta[1]} is necessarily equivariant in the path endpoints. While a proposition about pathsAxx=Ω xApaths A x x = \Omega_x A need not be.

Of course in the model this just reflects the fact that there is a weak homotopy equivalence AA Δ[1]A \stackrel{\simeq}{\to} A^{\Delta[1]} . This weak equivalence makes manifestly clear why any proposition about A Δ[1]A^{\Delta[1]} is fixed by knowing what it does to AA. After all, they are the same up to a little fluff.

So I propose to “explain” the magic of paths types / identity types as follows:

A proposition about paths A may look like just a proposition about every path in A, but really it is restricted to be such a proposition which is equivariant with respect to pre- and postcomposition of paths.

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

Re: Prequantum Physics in a Cohesive ∞-Topos

But circle only has a single point!

Ah, I see the confusion. Actually, that’s not true; I think you’re letting the model you have in mind lead you astray. The inductive definition of circle only “puts” one point into it, but there’s no useful sense in which the statement “circle only has a single point” is true internally. See the comment after circle_cover_contrbase in Pi1S1.v. What the type theory calls a point has nothing to do with vertices in simplicial sets. Remember that everything happens locally, so that when the type theory talks about “a point” of a space, it really means a generalized element.

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

Re: Prequantum Physics in a Cohesive ∞-Topos

But actually, I think your explanation is correct too. It took me a little while to understand what you meant by “a proposition about paths A”, but of course you were referring to the sort of propositions that we can prove by path-induction. In that case, the fact that such a proposition must be equivariant with respect to paths is just a special case of the fact that any dependent type P : A -> Type must come with an action by the paths in A. What I said is that the propositions that path-induction applies to are dependent over two points x:A, y:A together with a path p : x == y between them; it follows that such a proposition must be acted upon by paths x == x' and y == y', as well as paths p == p'.

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

Re: Prequantum Physics in a Cohesive ∞-Topos

The definition of identity in the Coq standard library is

Inductive identity (A:Type) (a:A) : A -> Type :=
  identity_refl : identity a a.

Note that it explicitly says Type, not Prop. Nevertheless, because in Coq Type is pseudo-polymorphic, sometimes Type can mean Prop, and in this case Coq is too smart for its own good and say “ah-hah, because you have a one-constructor type, I’ll put it in Prop for you.”

This should be compared with the Coq definition of eq:

Inductive eq (A : Type) (x : A) : A -> Prop :=
  eq_refl : eq x x

which is exactly the same, except that it says Prop instead explicitly.

There is a further discussion about the difference between the (a:A) : A -> Type (the “Paulin-Mohring formulation”) and the A -> A -> Type (the Martin-Lof formulation) versions of identity types here.

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

Re: Prequantum Physics in a Cohesive ∞-Topos

Thanks, Guillaume, that helps.

I was kindly pointed to http://prover.cs.ru.nl/ and am using this right now to play around with Coq, for the first time, through the web interface (while on the train…).

So I copy and paste the definition of path types.

Inductive paths (A : Type) : A -> A -> Type 
 := idpath : forall x : A, paths A x x.

Coq produces from this the following three terms

paths_rect = 
fun (A : Type) (P : forall a a0 : A, paths A a a0 -> Type)
  (f : forall x : A, P x x (idpath A x)) (y y0 : A) 
  (p : paths A y y0) =>
match p as p0 in (paths _ y1 y2) return (P y1 y2 p0) with
| idpath x => f x
end
     : forall (A : Type) (P : forall a a0 : A, paths A a a0 -> Type),
       (forall x : A, P x x (idpath A x)) ->
       forall (y y0 : A) (p : paths A y y0), P y y0 p

and

paths_ind = 
fun (A : Type) (P : forall a a0 : A, paths A a a0 -> Prop) => paths_rect A P
     : forall (A : Type) (P : forall a a0 : A, paths A a a0 -> Prop),
       (forall x : A, P x x (idpath A x)) ->
       forall (y y0 : A) (p : paths A y y0), P y y0 p

and

paths_rec = 
fun (A : Type) (P : forall a a0 : A, paths A a a0 -> Set) => paths_rect A P
     : forall (A : Type) (P : forall a a0 : A, paths A a a0 -> Set),
       (forall x : A, P x x (idpath A x)) ->
       forall (y y0 : A) (p : paths A y y0), P y y0 p

I can easily read the last two. They do nothing but read in a Prop-valued function and a Set-valued function, respectively, on all the paths in A, regard it as a Type-valued function and feed that into paths_rect, which accepts generally Type-valued functions on paths.

So I need to understand paths_rect. I understand that this reads in a Type-valued function f on paths and a proof that this is inhabited over all identity paths and spits out something that exhibits for any path an inhabitant of f over that path. So this is, as we said above, the assertion that a “generalized proposition” about all paths which holds over all identity paths already holds over all paths.

Okay, what I don’t understand yet is how paths_rect accomplishes this via that match-line. What’s happening there? What is p0 doing there?

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

Re: Prequantum Physics in a Cohesive ∞-Topos

what I don’t understand yet is how paths_rect accomplishes this via that match-line

The idea is that the path type is inductively generated by reflexivity/identity paths. Therefore, to define a function acting on all paths, it suffices to define it for identity paths. Just like the natural numbers are inductively generated by zero and successor, so to define a function acting on all natural numbers it suffices to say what to do in those two cases. The Coq syntax for the recursive definition of, say, factorials is

Fixpoint fact (n : nat) : nat :=
  match n with
  | 0    => 1
  | S n' => (S n') * fact n'
  end.

which says “given a natural number nn, if n=0n=0, then output 11, while if nn is the successor of some other natural number nn', output the product of nn (the successor of nn') with the factorial of nn'.” Since nat is defined inductively by 00 and SS, this suffices to define fact for all natural numbers.

Similarly,

match p with
| idpath x => f x
end

would say “given a path pp, if pp is the identity path of a point xx, then output f(x)f(x).” Since paths are defined inductively by identities, this suffices to determine the operation on all paths.

The as and in and return clauses are annotations which are sometimes necessary to clue Coq into your intent when you start doing more complicated dependent type hackery. They are not necessary in the definition of paths_rect – try removing them and you’ll see that it still compiles. However, when displaying the definition, Coq always automatically puts them in.

Posted by: Mike Shulman on November 13, 2011 2:03 AM | Permalink | PGP Sig | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

Some basic facts about fiber sequences

Specifically, the fact that:

  • A map of fibrations lying over an equivalence of base spaces is an equivalence on total spaces iff it is an equivalence on fibers.

In particular, in a fibration with contractible total space, the fiber is equivalent to the loop space of the base. I proved this because it was part of what I needed to identify ΩS 1=\Omega S^1 = \mathbb{Z}.

It looks like what you need is that a double homotopy fiber is the loop space of the original base. I remember Voevodsky mentioning this fact when he went through his Coq files with us at Oberwolfach, so I’m sure it’s in there somewhere; but as I said, I don’t know exactly where.

Posted by: Mike Shulman on October 29, 2011 10:08 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

Hi Mike,

thanks for these replies. I’ll get back to them a little later when I have more time. For the moment just a quick question/comment on this one here:

I proved this because it was part of what I needed to identify ΩS 1=\Omega S^1 = \mathbb{Z}

I was looking for your Coq file with the proof of this the other day, since I thought I might learn a bit of HoTT coding from staring at it. But I didn’t find the file. Could you post the url again, for convenience?

I did go to

https://github.com/HoTT/HoTT

and looked for the file, but this page did leave me a bit puzzled.

Did “you” (those of you who maintain the site) think about adding some summary and explanation on this page? Coming from the outside I am missing here some text that tells me something like: “Go here for this code and there for that code. If you are new here you need to first read this, then that.” Of course I understand that this is probably not meant to be read by any outsiders. But maybe eventually if would be useful if it were.

Need to rush off now. More substantial messages later…

Posted by: Urs Schreiber on October 30, 2011 6:19 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

I was looking for your Coq file with the proof of this the other day

It’s in the “Coq” subdirectory, in the further “HIT” subdirectory for Higher Inductive Types: https://github.com/HoTT/HoTT/blob/master/Coq/HIT/Pi1S1.v.

some summary and explanation on this page?

More summary and explanation somewhere would be nice; I’m not sure whether that page is the right place for it.

Posted by: Mike Shulman on October 30, 2011 10:38 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

in the further “HIT” subdirectory

Ah, thanks. I had clicked around here and there, but never on that one.

More summary and explanation somewhere would be nice; I’m not sure whether that page is the right place for it.

The README-file on that Coq-directory page would be the canonical place.

Posted by: Urs Schreiber on October 30, 2011 10:49 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

I realize that I may have a basic confusion about the above HoTT axiomatics of cohesion: the universal properties of reflection and coreflection are formulated there currently with respect to the internal homs. Need they not be formulated in terms of the external homs, suitably re-internalized?

The \flat-operation sends internal homs [,][-,-] to external homs H(,)\mathbf{H}(-,-), in that [A,B]DiscH(A,B)\flat[A,B] \simeq Disc \mathbf{H}(A,B). The adjunction isomorphism holds as

H(ΠX,A)H(X,A) \mathbf{H}(\mathbf{\Pi}X, A) \simeq \mathbf{H}(X, \flat A)

hence as

[ΠX,A][X,A] \flat [\mathbf{\Pi}X, A] \simeq \flat [X, \flat A]

but not as

[ΠX,A][X,A], [\mathbf{\Pi}X, A] \simeq [X, \flat A] \,,

which however is implied by the above axiomatics, it seems to me.

For instance we have A[*,A]\flat A \simeq [\ast, \flat A]. If we had [Π(*),A]\cdots \simeq [\mathbf{\Pi}(\ast), A] then this would be [*,A]A\cdots \simeq [\ast, A] \simeq A for all AA, hence would force all objects to be discrete.

Am I mixed up?

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

Re: Prequantum Physics in a Cohesive ∞-Topos

Curses!!! You’re right! Back to the old drawing board.

Hmm… this makes it much harder.

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

Re: Prequantum Physics in a Cohesive ∞-Topos

Back to the old drawing board.

Okay. It’s the same problem that bit me in the other thread here when I was trying to see if Guillaume’s proposed HoTT code for effective epimorphisms did capture the HTT that it was supposed to capture: do we use external or internal homs to characterize universal properties. So we need to get back to this drawing board anyway.

I won’t have much time for this today, but here is a quick thought that might be helpful:

at least for cohesive \infty-toposes that have an ∞-cohesive site of definition, we have for every representable UU that Π(U)*\mathbf{\Pi}(U) \simeq \ast and Π(X×U)Π(X)×Π(U)Π(X)\mathbf{\Pi}(X \times U) \simeq \mathbf{\Pi}(X) \times \mathbf{\Pi}(U) \simeq \mathbf{\Pi}(X).

This implies that whenever AA is discrete, the internal homs into AA already coincide with the re-internalized external homs: for all XX we have

[X,A][X,A]. \flat [X, A] \simeq [X, A] \,.

(For the record and for other readers: this is because the internal hom of \infty-stacks is the \infty-stack which sends [X,A]:UH(X×U,A)[X,A] : U \mapsto \mathbf{H}(X \times U , A) and by the above H(X×U,A)H(Π(X×U),A)H(X,A)\mathbf{H}(X \times U, \flat A) \simeq \mathbf{H}(\mathbf{\Pi}(X \times U), A) \simeq \mathbf{H}(X, A).)

This means for instance that over an \infty-cohesive site our current HoTT coding of the reflection (ΠDisc)(\Pi \dashv Disc) happens to be correct after all.

Moreover, for the coreflection (DiscΓ)(Disc \dashv \Gamma) it means that it would be sufficient to say in HoTT that the map

[X,A][X,A] [X, \flat A] \to [X,A]

from a discrete XX, while not an equivalence, factors through [X,A][X,A]\flat [X, A] \to [X,A] by an equivalence.

Posted by: Urs Schreiber on November 14, 2011 8:34 AM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

And here’s the part that’s really going to bake your noodle: is the site of definition an internal or external construction? :P

Posted by: David Roberts on November 14, 2011 10:22 AM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

is the site of definition an internal or external construction? :P

I see what you mean, but just for clarification:

here it is not supposed to be an internal construction. I was just pointing out that the alleged internal characterization of the reflective embedding of discrete objects that we considered in HoTT language happens to be correct in cases where externally we happen to know of an \infty-cohesive site of definition. Once the dust has settled we don’t want to be speaking of sites at all for characterizing cohesion, whether externally or internally.

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

Re: Prequantum Physics in a Cohesive ∞-Topos

I wrote:

Moreover, for the coreflection (DiscΓ)(Disc \dashv \Gamma) it means that it would be sufficient to say in HoTT that the map [X,A][X,A][X, \flat A] \to [X, A] from a discrete XX, while not [necessarily] an equivalence [itself], factors through [X,A][X,A]\flat[X,A] \to [X,A] by an equivalence.

So let me try if I can say that in Coq (imagine me speaking with a heavy accent):

Axiom flat_is_coreflection : 
  forall X A, is_discrete X ->
   exists factorization : (X -> flat A) -> flat( X -> A ),
    is_equivalence(factorization)
    /\
    paths 
      ( map_from_flat (X -> A) o factorization ) 
      (fun f : X -> flat A => (map_from_flat X) o f)

How’s that?

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

Re: Prequantum Physics in a Cohesive ∞-Topos

It’s the same problem that bit me in the other thread

I’m not convinced of that – I think limits and colimits usually do internalize in the obvious way, using the Yoneda lemma. But I suppose there could also be a problem there.

Here are the thoughts I’ve been having so far; somewhat similar to yours.

First of all, since the discrete and codiscrete objects are reflective subcategories whose reflectors preserve finite products, they are both exponential ideals. Thus, [X,A][X,A] is discrete if AA is discrete, and codiscrete if AA is codicrete. This implies that our expressions for the adjunctions ΠDisc\Pi\dashv Disc and ΓCodisc\Gamma\dashv Codisc are correct, at least in that regard.

Secondly, if FGF\dashv G is an adjunction between cartesian closed categories in which FF preserves products, then the adjunction isomorphism internalizes to yield [X,GY]G[FX,Y]. [X, G Y] \xrightarrow{\cong} G [F X, Y].

Applying this to DiscΓDisc \dashv \Gamma, we obtain [A,ΓX]Γ[DiscA,X] [A, \Gamma X] \cong \Gamma [ Disc A, X] or, in internal terms, [A,X][A,X]when A is discrete [A, \flat X] \cong \flat [A,X] \qquad\text{when A is discrete} which is, I think, about the same as your final conclusion.

Your Coq expression of that looks pretty good, except that as Guillaume pointed out, you don’t want to use exists since that refers only to Coq’s Prop. Moreover, for ease of use, I would break it up into three axioms:

Axiom flat_factorization : forall X Y, flat (X -> flat Y) -> flat (X -> Y).

Axiom flat_factorization_factors : forall (X Y : Type) (f : flat (X -> flat Y)),
  map_from_flat _ o (map_from_flat _ f) ~~>
  map_from_flat _ (flat_factorization _ _ f).

Axiom flat_is_coreflection :
  forall X Y, is_discrete X -> is_equiv (flat_factorization X Y).
Posted by: Mike Shulman on November 14, 2011 5:37 PM | Permalink | PGP Sig | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

Shouldn’t it be

Axiom flat_factorization : forall X Y, (X -> flat Y) -> flat (X -> Y).

instead ?

Posted by: Guillaume Brunerie on November 15, 2011 12:00 AM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

Hmm, if we’re assuming strong connectedness, then yes; thanks. (I wrote that code before I noticed the exponential-ideal property, then just copied and pasted it.)

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

Re: Prequantum Physics in a Cohesive ∞-Topos

since the discrete and codiscrete objects are reflective subcategories whose reflectors preserve finite products, they are both exponential ideals.

Ah, right, thanks. That’s of course much better than my assumption of a special site. Good. (But we need to code strong connectedness, too, then.)

as Guillaume pointed out, you don’t want to use since that refers only to Coq’s Prop.

Yes, right, I did remembered after posting, but was too busy to fix it.

for ease of use, I would break it up into three axioms:

Okay, sure.

Apart from how to typeset it, I was beginning to worry about the “ease of use” of this axiom in proofs. Guillaume should try it out if this allows him to finish his proof as indicated here.

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

Re: Prequantum Physics in a Cohesive ∞-Topos

But we need to code strong connectedness, too, then.

Yes, but that should be fairly easy, I think, once we have the right axiomatization of the discrete objects. It could be that our axiomatization will force it automatically without needing to add it as a separate axiom.

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

Re: Prequantum Physics in a Cohesive ∞-Topos

I’m now worried about a different issue, which I should have been worried about as soon as Steve Awodey pointed us back to his paper with Lars Birkedal: pullback-stability. When we say

flat : Type -> Type

we actually mean that \flat is an endomorphism of the object classifier. That means that not only do we have an operation acting on the core of H\mathbf{H}, we have operations acting on the cores of all its slice categories H/X\mathbf{H}/X which commute with pullback.

This is not a problem for \sharp, I think, since the codiscrete objects are a subtopos and sheafification does commute with pullback. But I am worried about \flat. Perhaps we should axiomatize \sharp first and then say

flat : sharp Type -> sharp Type

? That seems like it would get painful quickly….

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

Re: Prequantum Physics in a Cohesive ∞-Topos

I’m thinking of adding the following axioms:

Ah, thanks! I didn’t appreciate that it would be this straightforward.

This should say that piXpi X is a reflection of XX into the discrete objects.

Yes, by this proposition (HTT, prop. 5.2.7.8).

I should try to acquire more of a working knowledge of HoTT, going beyond my current tourist knowledge.

I am guessing now that it will be comparably straightforward to say

Π \Pi * \simeq *

?

And to say that the coreflector of the discrete objects is related to the reflector of the codiscrete object? (This I should be able to figure out myself now.)

The main issue still remaining there, I think, is exactness. We have yet to decide how to formalize the notion of “groupoid object” so that we can take its quotient.

But the existence of the quotient is clear? I thought there was a problem with existence of colimits, still. No?

And how about universality (pullback-stability) of colimits?

Probably you are using such exactness in e.g. constructing classifying spaces?

Yes, it enters heavily in the proof of GBund(X)H(X,BG)G Bund(X) \simeq \mathbf{H}(X, \mathbf{B}G). In fact the whole proof is effectively just an appeal to exactness in the arrow topos H Δ[1]\mathbf{H}^{\Delta[1]}.

And pullback stability of colimits enters crucially in the proof that in a cohesive \infty-topos every object has a cover by a union of contractibles. This gives the notion of local trivializability of GG-bundles.

But all this is less central to the development of geometric structure in a cohesive \infty-topos than one might think. For most purposes that I have come across so far, it is less important to have the bundle PXP \to X than it is to have the cocycle XBGX \to \mathbf{B}G that classifies it. And of the remaining cases it is usually more important to know that every cocycle gives rise to a bundle, than to know that all bundles arise this way.

So for many purposes it’s not fatal not to have exactness.

Posted by: Urs Schreiber on October 28, 2011 8:47 AM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

I am guessing now that it will be comparably straightforward to say Π**\Pi \ast\simeq\ast?

Yes:

pi_unit_is_equiv : is_equiv (pi unit).

But the existence of the quotient is clear? I thought there was a problem with existence of colimits, still. No?

Higher inductive types should let us construct any “computable” colimit. Finite colimits are easy, and so I think should be any sequential colimit, or other diagram shape that we can describe easily. So I believe that once we know how to define simplicial objects, we should be able to take their colimits without too much trouble.

And how about universality (pullback-stability) of colimits?

Should follow from local cartesian closure.

And of the remaining cases it is usually more important to know that every cocycle gives rise to a bundle, than to know that all bundles arise this way.

What sorts of group objects GG are you considering? There are two cases in which I think it shouldn’t be hard to construct BGB G with current technology:

  1. If GG is categorically discrete (or even nn-truncated for some finite nn), then it should be possible to give a finite presentation for BGB G as a HIT, since it will be (n+1(n+1)-truncated.

  2. If GG is realizable as the automorphisms of some type XX (or even a structured type, if the structure is finitely describable), then using the univalence axiom, we should be able to find BGB G as a full subobject of the universe Type (the image of the classifying map *Type\ast\to Type of XX — images can be constructed with HITs).

Posted by: Mike Shulman on October 28, 2011 3:09 PM | Permalink | PGP Sig | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

I was thinking how we might define simplicial objects inductively, and came up with the following, perhaps misguided, attempt. I make to guarantees about the following working :)

The goal is to inductively define simplicial objects and the decalage functor simultaneously.

Start with an internal reflective graph i.e. a 1-truncated simplicial object sk 1Xsk_1 X (at present this is just notation saying that this thing is 1-truncated, not that it is the truncation of anything - but you see where I’m headed). If we are given another 1-truncated simplicial object over sk 1Xsk_1 X, p:sk 1DXsk 1Xp:sk_1 D X \to sk_1 X, such that the collection of 0-simplices of sk 1DXsk_1 D X is isomorphic to the collection of 1-simplices of sk 1Xsk_1 X (hmm, yes, issue there with saying things are isomorphic perhaps), pp is split, and other identities that are satisfied by the 1-truncation of the map Dec 1YYDec^1 Y \to Y for a simplicial set YY.

We then define a 2-truncated simplicial object to be the data we can extract from this setup: the collection of 2-simplices is the collection of 1-simplicies of sk 1DXsk_1 D X, and we get all the relevant face/degeneracy maps from the structure we have at hand. This is the induction step.

I suppose we also need to define, as part of this inductive definition what a map of nn-truncated simplicial objects is.

I don’t know enough about Coq to say this is formalisable therein, or even if this really is any different to how one might naively try to define simplicial objects in Coq. In any case, it all seems to need extensional equality - do we really want this when talking about simplicial objects in an (,1)(\infty,1)-category?

Posted by: David Roberts on October 30, 2011 12:21 AM | Permalink | Reply to this

Simplicial objects in type theory

Ha! I have my own radical idea for how to define simplicial objects, which I’ve been sitting on quietly for a while because it doesn’t quite work yet, and I’m not sure yet whether it can be made to work. But I think your suggestion is a bit similar to mine, so let me put my thoughts out there, and maybe we can get somewhere.

Here’s my idea: a semi-simplicial type (i.e. no degeneracies) XX consists of

  1. A type X 0X_0, together with
  2. For every x:X 0x:X_0, a semi-simplicial type dependent over XX.

This is a coinductive definition. I could explain further how a semi-simplicial object falls out of it, but I won’t, because it’s more fun to figure out for yourself. It’s also fun to figure out how to define, starting from this definition, constructions like the simplicial kernel of a map of types, the geometric realization / colimit of XX, the types of nn-simplices, nn-spheres, and nn-kk-horns in XX, and the opposite X opX^{op}. I find this all very pleasing!

However, for purposes of formalization, this definition has two problems. Firstly, it is coinductive in a way that Coq’s native coinductive types can’t obviously express (part of the data consists of a type dependent on the object being defined). But I think this can be worked around by phrasing it impredicatively. (And, perhaps, eventually, by extending the notion of coinductive type.)

Secondly, and more seriously, it requires knowing the notion of “dependent semi-simplicial type” in order to define a non-dependent one. (Just as you noted that your definition requires defining maps at the same time.) Clearly, the definition of dependent s.s.t. will then involve knowing a notion of “doubly-dependent s.s.t.”, and so on into an infinite descent. You can try to phrase it in terms of maps rather than dependent types, but then to define maps you end up having to define composition of maps, and to define composition of maps you end up having to define the associativity isomorphism for triple composition of maps, and so on. Having extensional equality might solve those problems, but as you say, we don’t want that! (One way to say what’s going on is that we seem to be defining the category of semi-simplicial objects coinductively, but categories are not basic objects in the type theory (yet).)

I have some ideas about how to work around this second problem, too, but they’re kind of messy and I’m not positive yet that they’ll work. But maybe you or some other reader will come up with a nicer solution!

Posted by: Mike Shulman on October 31, 2011 4:54 AM | Permalink | PGP Sig | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

I am guessing now that it will be comparably straightforward to say Π**\Pi \ast \simeq \ast?

Yes: […]

All right, that’s evident enough.

What sorts of group objects GG are you considering?

Two cases are of central interest:

  1. We will want to axiomatize a line object 𝔸\mathbb{A} and then form the corresponding abelian group object 𝔾\mathbb{G}.

  2. We will want to add the axioms for infintesimal cohesion , then give finite presentations of infinitesimal group objects B𝔤\mathbf{B}\mathfrak{g}. The formalism will then know how to integrate them up.

Posted by: Urs Schreiber on October 28, 2011 10:47 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

How much can you do internally to your cohesive ∞-topos if all you know is that it has the “elementary” structure of an ∞-topos, and contains a subcategory of “discrete objects” which is both reflective and coreflective?

I’m probably mistaken, but every ∞-topos has this property (by taking the subcategory to be the whole topos). Unless “discrete objects” has a particular meaning?
Posted by: Guillaume Brunerie on October 28, 2011 10:38 AM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

How much can you do internally to your cohesive ∞-topos if all you know is that it has the “elementary” structure of an ∞-topos, and contains a subcategory of “discrete objects” which is both reflective and coreflective?

I’m probably mistaken, but every ∞-topos has this property (by taking the subcategory to be the whole topos).

You are correct that this is a case one can always consider. Degenerate as this case is, it can actually be useful to make it explict in cases where we have an interesting equivalence of \infty-toposes and take all the embeddings here to be given by this equivalence. Some comments on this are at discrete ∞-groupoids , where the cohesive \infty-topos

TopcoDiscΓDiscΠGrpd Top \stackrel{\overset{\Pi}{\to}}{\stackrel{\overset{Disc}{\leftarrow}}{\stackrel{\overset{\Gamma}{\to}}{\underset{coDisc}{\leftarrow}}}} \infty Grpd

is considered, with Π=Sing\Pi = Sing the ordinary fundamental \infty-groupoid functor, which famously is an equivalence.

Generally, one may consider cohesion over an arbitrary base \infty-topos B\mathbf{B} other than Grpd\infty Grpd, and then of course every \infty-topos H\mathbf{H} is cohesive over itself, via

HIdIdIdIdH. \mathbf{H} \stackrel{\overset{Id}{\to}}{\stackrel{\overset{Id}{\leftarrow}}{\stackrel{\overset{Id}{\to}}{\underset{Id}{\leftarrow}}}} \mathbf{H} \,.

This is not really interesting in itself, obviously, but, as always, it is useful for the general theory to explicitly carry the degenerate cases along.

Posted by: Urs Schreiber on October 28, 2011 12:29 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

Ah, now I see that the comment

I’m probably mistaken, but every ∞-topos has this property (by taking the subcategory to be the whole topos).

may arise from a misunderstanding: we are not talking about characterizing the property of any \infty-topos to be cohesive over some other \infty-topos. We are talking about equipping it explicitly with one such structure.

Posted by: Urs Schreiber on October 28, 2011 12:33 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

Indeed, I was thinking of the property to be cohesive over another ∞-topos.

But I still do not really understand what you are trying to do. When you say that you can do physics in a cohesive ∞-topos, don’t you need it to be cohesive over ∞Gpd? Can you do something interesting with an ∞-topos cohesive over itself via the identity?

Moreover, if find the Axiom is_discrete : Type -> Type. part a bit misleading.
For me an axiom is something that you should not be able to prove, and in this case you can take the proposition always true for is_discrete and take the identity for pi and flat.

Perhaps something like Parameter is_discrete : Type -> Type. would be better? (it means exactly the same thing for Coq, but tells the human reader that this is not an axiom but a parameter, and I think this is what you want in this case)

Posted by: Guillaume Brunerie on October 30, 2011 8:53 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

When you say that you can do physics in a cohesive ∞-topos, don’t you need it to be cohesive over ∞Gpd?

No, it may be over a different base \infty-topos. For instance supergeometric cohesion and hence supersymmetric physics is not over discrete \infty-groupoids, but over discrete super ∞-groupoids.

Indeed, the point of these internal constructions is that they make sense in any cohesive \infty-topos.

But in some models of the axioms the constructions may be more interesting than in others. For instance…

Can you do something interesting with an ∞-topos cohesive over itself via the identity?

Indeed, the physics in a topos of discrete cohesion is mostly trivial. Still, as I mentioned in my previous comment, it is useful not to exclude discrete cohesion from the picture.

Compare to this: the empty set in itself is not interesting. But it is nevertheless very useful to include the empty set in the collection of all sets. This is a common pattern in mathematics. It is useful to include the degenerate cases in the general theory.

Perhaps something like Parameter is_discrete : Type -> Type. would be better? (it means exactly the same thing for Coq, but tells the human reader that this is not an axiom but a parameter, and I think this is what you want in this case)

Could you point me to some documentation that explains how Parameter and Axiom two should be used in Coq?

Posted by: Urs Schreiber on October 30, 2011 10:30 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

When you say that you can do physics in a cohesive ∞-topos, don’t you need it to be cohesive over ∞Gpd?

Well, part of the point of topos theory is that any topos can perfectly well “pretend” to be the topos of sets, so that we can then do all sorts of mathematics “over” that topos. (From a foundational point of view, “the” topos of sets isn’t particularly special anyway.) Similarly, any (,1)(\infty,1)-topos can pretend to be Gpd\infty Gpd. So if we have an (,1)(\infty,1)-topos which is cohesive over another one, we can always pretend the latter one is Gpd\infty Gpd.

Perhaps something like Parameter is_discrete : Type -> Type. would be better?

Sure. I actually find it kind of confusing that Coq has two words Axiom and Parameter (and also Conjecture!) that mean exactly the same thing—especially because they don’t mean (quite) the same thing as Hypothesis and Variable, and I can never remember without looking it up which word is the same as which word and different from which other word and what the difference is. But if Parameter makes you happier than Axiom, that’s fine with me.

Posted by: Mike Shulman on October 30, 2011 10:46 PM | Permalink | PGP Sig | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

In reaction to Guillaume Brunerie’s various comments, I have done the following to the nnLab:

“As always in topos theory and higher topos theory, such definitions can be made sense of over any base . Here: over any base (∞,1)-topos.

Over the canonical base ∞Grpd of ∞-groupoids, the definition of a cohesive (∞,1)-topos is equivalently the following: […]

Often we will tacitly assume to work over ∞Grpd. But most statements and constructions have straightforward generalizations to arbitrary bases.

In particular, below in the internal definition of cohesion, it takes more effort to fix the base topos than to leave it arbitrary.”

Posted by: Urs Schreiber on October 31, 2011 3:52 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

Sorry, there is still something I don’t understand.

Generally, one may consider cohesion over an arbitrary base ∞-topos B other than ∞Grpd

This nLab page says:

Every cohesive (,1)(\infty,1)-topos is a hypercomplete (,1)(\infty,1)-topos.

What does it mean?

It’s probably not that if HH is an \infty-topos cohesive over any other \infty-topos, then HH is hypercomplete, or every \infty-topos would be hypercomplete.

It’s perhaps that the notion of hypercompleteness makes sense over any base \infty-topos and that if HH is cohesive over HH', then HH is hypercomplete over HH', but I did not find anything about hypercompleteness over an arbitrary \infty-topos in the nLab.

Perhaps that the result is true only when the \infty-topos is cohesive over Gpd\infty{}Gpd, but then I don’t understand why the argument “any (∞,1)-topos can pretend to be ∞Gpd” does not work.

No, it may be over a different base ∞-topos. For instance supergeometric cohesion and hence supersymmetric physics is not over discrete ∞-groupoids, but over discrete super ∞-groupoids.

Just to be sure, when you say “discrete something \infty-groupoid”, this is exactly the same thing as a “something \infty-groupoid” and the word “discrete” is just there to emphasize that what you are really interested in is an \infty-topos cohesive over the \infty-topos of “something \infty-groupoids”, right?

Posted by: Guillaume Brunerie on October 31, 2011 1:43 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

Hey Guillaume,

right, the nnLab entries mostly work over Grpd\infty Grpd, currently. Somebody should generalize them.

You may notice that the discussion of generalization to arbitrary base \infty-toposes is more pressing when we formulate the theory – as we just start doing now – in HoTT, where we cannot easily say: let the sub-\infty-topos of discrete objects be Grpd\infty Grpd.

Posted by: Urs Schreiber on October 31, 2011 2:58 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

Just to be sure, when you say “discrete something ∞-groupoid”, this is exactly the same thing as a “something ∞-groupoid” and the word “discrete” is just there to emphasize that what you are really interested in is an ∞-topos cohesive over the ∞-topos of “something ∞-groupoids”, right?

The word “discrete cohesion” refers to cohesion induced by the identity functors.

Over the canonical base \infty-topos, “discrete \infty-groupoid” just means “\infty-groupod”. Also topological spaces are “discrete \infty-groupoids”, in the sense of homotopy theory, because the functors that exhibit TopTop as being cohesive over Grpd\infty Grpd are equivalences.

If we choose a different base \infty-topos B\mathbf{B} then the objects of B\mathbf{B} are equipped with “discrete cohesion relative to B\mathbf{B}”. Any \infty-topos equivalent to B\mathbf{B} exhibits discrete cohesion relative to B\mathbf{B}.

Posted by: Urs Schreiber on October 31, 2011 3:07 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

Nice talk! David Roberts announced it on Google+.

Posted by: John Baez on October 27, 2011 5:10 AM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

Nice talk!

Thanks.

David C. asks me to say how it went. I am being told that it went well. But even so I am of course not the one to judge this.

David Roberts announced it on Google+.

Yes, I got an email alert to this effect. Somehow I have a Google+-account with some people in some circle, but I never look at it. I can’t handle it, too much, without a topic filter!

Posted by: Urs Schreiber on October 27, 2011 4:12 PM | Permalink | Reply to this

HoTT and HTT

By coincidence, the very moment after I had sent the above message about cohesive axioms in HoTT yesterday, Bas Spitters told me of plans to plan a workshop on “Homotopy Type Theory and Higher Topos Theory” in summer 2012.

The question was: how many people would I know who might be interested in attending such. The ones who I could readily name he had already on his list, of course. But maybe we could have a show-of-hands here.

Posted by: Urs Schreiber on October 28, 2011 9:03 AM | Permalink | Reply to this

Re: HoTT and HTT

Count me in on the mailing list about the event.

Posted by: David Corfield on October 28, 2011 10:19 AM | Permalink | Reply to this

Re: HoTT and HTT

You probably don’t know me and I’m still a student but I would be very interested too!

Posted by: Guillaume Brunerie on October 28, 2011 10:44 AM | Permalink | Reply to this

Re: HoTT and HTT

I expect I’m already on the list, but I’d be interested of course. Did he say anything about where it might be held?

Posted by: Mike Shulman on October 28, 2011 3:12 PM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

Could you point me to some documentation that explains how Parameter and Axiom two should be used in Coq?

Here is the official doc about Axiom and Parameter. It is not very helpful, though, it only says that the two are equivalent.

I was looking for your Coq file with the proof of this the other day, since I thought I might learn a bit of HoTT coding from staring at it. But I didn’t find the file. Could you post the url again, for convenience?

A little remark (I don’t know how much Coq you know, sorry if you already know what I’m saying): staring at the Coq files may be interesting to understand the definitions and theorems, but understanding the proofs will be most likely very difficult. The reason is that in Coq a proof script is something like that:

Let's prove this result by induction on n   (induction n)
This case is trivial                        (auto)
Let's apply theorem foo                     (apply foo)
Let's simplify the result                   (simpl)
Let's cancel the identity paths             (cancel_units)
The result is now trivial                   (auto)
Proof completed                             (Defined)

The problem is that at each line you have to know what is the current goal (and it will change after each line), and except for the statement of the theorems/lemmas the goals are never written in the files (because Coq will be able to deduce them from the previous steps).

If you want to understand the proofs, you should install Coq, download the files and run the files inside Coq. This way you will be able to navigate through the proofs step by step, and Coq will show you the goals at each point of the proof.

If you’ve never used Coq, Andrej Bauer has some nice video tutorials here that are definitely worth checking out.

Well, part of the point of topos theory is that any topos can perfectly well “pretend” to be the topos of sets, so that we can then do all sorts of mathematics “over” that topos.

Indeed, that makes sense.

Posted by: Guillaume Brunerie on October 31, 2011 2:50 AM | Permalink | Reply to this

Re: Prequantum Physics in a Cohesive ∞-Topos

I don’t know how much Coq you know

Nothing of substance, really. I have been following the meaning of code that has been discussed here on the blog over the time, or on notepads of people I was chatting with, but that’s already it. I like to get a working understanding though.

What you say and the links that you provide is already quite helpful. Maybe we should collect more along such lines at nLab:Coq.

Posted by: Urs Schreiber on October 31, 2011 6:46 AM | Permalink | Reply to this
Read the post WZW Models in a Cohesive ∞-Topos
Weblog: The n-Category Café
Excerpt: A talk on (higher dimensional) Wess-Zumino-Witten models internal to a cohesive infinity-topos.
Tracked: October 31, 2011 6:05 PM
Read the post HoTT Cohesion -- Exercise I
Weblog: The n-Category Café
Excerpt: de Rham coefficient objects and Maurer-Cartan forms in cohesive homotopy type theory.
Tracked: November 2, 2011 11:44 PM
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:49 PM
Read the post Multiple M5-branes, String 2-connections, and 7d nonabelian Chern-Simons theory
Weblog: The n-Category Café
Excerpt: An article on 7-dimensional Chern-Simons theory of nonabelian String 2-form fields.
Tracked: January 22, 2012 1:14 AM
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 Quantum Gauge Field Theory in Cohesive Homotopy Type Theory
Weblog: The n-Category Café
Excerpt: A survey article on the formalization of aspects of quantum gauge field theory in the formal language of cohesive homotopy type theory.
Tracked: August 20, 2012 7:54 AM

Post a New Comment