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

November 2, 2011

HoTT Cohesion – Exercise I

Posted by Urs Schreiber

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

In the discussion of a previous entry finally the Coq-formulation of the axioms of cohesion in homotopy type theory (HoTT) materialized (thanks to prodding by David Corfield and expertise by Mike Shulman). See

Axiomatic cohesion in HoTT .

With these axioms in hand, I would now enjoy to see the machinery put to work. I’ll try to take this as an occasion to learn HoTT and its coding as we go along. Currently I still know next to nothing, and so I am hoping that by stating in public the exercises that I pose to myself, I might get some hints from the experts and some help from whoever likes to join in.

The following should be a very basic and nevertheless interesting first exercise to warm up.

Exercise I a) Give the Coq-code that describes from a connected type – to be denoted

BG : Type

the homotopy fiber type of

map_from_flat BG : flat BG -> BG

to be denoted

flat_dR BG : Type

(The de Rham coefficient object.)

Exercise I b) Give the Coq-code that describes the canonical term

theta : G -> flat_dR BG

where G is the identity type

Id_BG pt pt : Type

(This $\theta$ formalizes the notion of the Maurer-Cartan form on $G$ .)

Hint: use uuo.v.

Warning: I assume that comprehensive code for the notion of connected objects is more involved than the rest of the exercise, so probably it is helpful to first adopt a more ad hoc treatment.

Posted at November 2, 2011 10:15 PM UTC

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

35 Comments & 3 Trackbacks

Re: HoTT Cohesion – Exercise I

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

Here is my code :-) (and the Cohesive_Topos module I’m using is here)

Note that I needed to use univalence in order to prove that the point is discrete (and I needed this to build a base point of $\flat BG$ from a base point of $BG$ ). Perhaps this is not necessary.

By the way, what do you mean by a connected object? Your link only defines a $n$ -connected object. Do you mean $0$ -connected? (in my code I just assumed that $BG$ is (constructively) inhabited).

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

Re: HoTT Cohesion – Exercise I

I would guess that connected object means 0-connected: the intuition is that every element of the type is connected by a path iff every object of the infinity-groupoid is isomorphic iff the space is path-connected.

Posted by: David Roberts on November 3, 2011 4:41 AM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise I

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

Hi Guillaume,

it was the most pleasant sensation this morning to find this message of yours, and the files you have created. Thanks!

I’ll get back to you on various points in a little while, just need to vacate my hotel room first and take care of some other things.

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

Re: HoTT Cohesion – Exercise I

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

Guillaume asked:

what do you mean by a connected object? Your link only defines a n-connected object. Do you mean 0-connected?

David suggested:

I would guess that connected object means 0-connected

Yes, that’s what is meant. If the counting seems to be unpleasantly off by one, you should think of “ $n$ -connected” as being shorthand for “ $n$ -simply connected”.

I have now added an explicit remark to this effect below the definition of n-connected objects.

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

Re: HoTT Cohesion – Exercise I

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

In the file …guillaumebrunerie/…/Cohesion.v there is currently the following observation and question

The space of points of [flat BG] is equivalent to the space of points of [BG], this is just a consequence of the fact tha [flat] is a coreflection and that the point is discrete.

(Is this expected? Is seems strange)

Yes, this is expected and makes good sense.

To see this you should think of $\mathbf{B}G$ as being the moduli ∞-stack of $G$ -principal $\infty$ -bundles, and of $\mathbf{\flat} \mathbf{B}G$ as the moduli $\infty$ -stack of flat $G$ -principal $\infty$ -bundles. Namely for any other object $X$ the space of maps $X \to \mathbf{B}G$ is identified with the space of $G$ -bundles over $X$

$G Bund(X) \simeq \mathbf{H}(X, \mathbf{B}G)$

and

$G Bund_{\nabla_{flat}}(X) \simeq \mathbf{H}(X, \mathbf{\flat}\mathbf{B}G) \,.$

Notice furthermore that in every $\infty$ -topos $\mathbf{H}$ we have that the global section geometric morphism $\Gamma$ (see there for details) is given by

$\Gamma(-) \simeq \mathbf{H}(\ast,-) \,,$

where $\ast$ denotes the terminal object of the $\mathbf{H}$ . Therefore

$\Gamma \mathbf{B}G \simeq \mathbf{H}(*,\mathbf{B}G)$

is the $\infty$ -groupoid of $G$ -principal $\infty$ -bundles over the point. Similarly

$\Gamma \mathbf{\flat}\mathbf{B}G \simeq \mathbf{H}(*,\mathbf{\flat}\mathbf{B}G)$

is the $\infty$ -groupoid of $G$ -principal $\infty$ -bundles equipped with fat $\infty$ -connection over the point.

But over the point every $G$ -principal $\infty$ -bundle should have a unique (and trivial) flat $\infty$ -connection. This is what the equivalence

$\Gamma \mathbf{\flat} \mathbf{B}G \stackrel{\simeq}{\to} \Gamma \mathbf{B}G$

asserts.

If this were not true, much of the interpretation of the theory would break. For instance there would be no sensible notion of $G$ -bundles being locally trivial, which however is important to have.

I have added a remark along these lines also to cohesive ∞-topos – structures – flat ∞-connections.

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

Re: HoTT Cohesion – Exercise I

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

In that remark, where you have

Notice here that the axioms of cohesion imply in particular that the terminal object $* \in \mathbf{H}$ really behaves like a geometric point…

presumably that allows this calculation:

$\Gamma \mathbf{\flat}\mathbf{B}G \simeq \mathbf{H}(*,\mathbf{\flat}\mathbf{B}G) \simeq \mathbf{H}(\mathbf{\Pi}(*),\mathbf{B}G) \simeq \mathbf{H}(*,\mathbf{B}G) \simeq \Gamma \mathbf{B}G.$

Posted by: David Corfield on November 3, 2011 11:47 AM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise I

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

presumably that allows this calculation:

$\Gamma \flat \mathbf{B}G \simeq \mathbf{H}(\ast, \flat \mathbf{B}G) \simeq \mathbf{H}(\mathbf{\Pi}(\ast), \mathbf{B}G) \simeq \mathbf{H}(\ast, \mathbf{B}G) \simeq \Gamma \mathbf{B}G$ .

Yes, but just for the record notice that this computation uses two more axioms (local and global connectedness, hence existence of $\mathbf{\Pi}$ as well as $\mathbf{\Pi}(\ast) \simeq \ast$ ) than are strictly necessary to establish the result. The total equivalence is already implied just from $\mathbf{\flat}$ being a coreflection. Of course using just that it is a little harder to prove.

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

Re: HoTT Cohesion – Exercise I

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

Thanks for the explanation Urs!

I’m still not sure what it really mean for $BG$ to be $0$ -connected. Does this imply that $BG$ has a distinguished base point pt? You are using pt several times, so I guess it does.

I’m asking this because there are ways to define what it means for a type to be path-connected (its $0$ th truncation is contractible) without being able to extract a point from this information.

In that remark, […] presumably that allows this calculation: Γ♭BG≃H(∗,♭BG)≃H(Π(∗),BG)≃H(∗,BG)≃ΓBG.

Yes, this is exactly how I proved it.

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

Re: HoTT Cohesion – Exercise I

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

I’m still not sure what it really mean for BG to be 0-connected. Does this imply that BG has a distinguished base point pt?

Yes, this is implied by cohesion. But it requires a little bit more discussion. This is why I had that “warning” in the above exercise.

I was wondering if working that out should be the next “exercise”. But currently I cannot quite see how hard this will be to do in HoTT. Maybe it’s much more than just an exercise, I am not sure. So it’s good that you are asking. You can maybe tell me if the following will be hard to implement in Coq-HoTT or not.

There are several different (but related) notions of “dimension” of an $\infty$ -topos. One of them is homotopy dimension. An $\infty$ -topos is said to have homotopy dimension $\leq n$ if every $(n-1)$ -connected object $A$ admits a morphism $\ast \to A$ .

Now, every local ∞-topos has homotopy dimension $\leq 0$ .

This is the statement of this proposition, which in turn refers to HTT, lemma 7.2.1.7.

If somebody could turn that argument from HTT to HoTT, that would be a very nice result.

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

Re: HoTT Cohesion – Exercise I

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

I was wondering if working that out should be the next “exercise”. But currently I cannot quite see how hard this will be to do in HoTT. Maybe it’s much more than just an exercise, I am not sure. So it’s good that you are asking. You can maybe tell me if the following will be hard to implement in Coq-HoTT or not.

One difficult notion seems to be the notion of effective epimorphisms, because formalizing the Čech nerve will be very difficult.

I’ve tried to unwrap the definition to see if this could be simplified, and I’ve found something that can be implemented in HoTT and that seems to be equivalent, but I have no idea if this is correct, so I’d rather check if you agree with my definition:

First, let $f : Y \to \star$ be a morphism, I want to know when $f$ is an effective epimorphism. By definition, $f$ is an effective epimorphism iff its the colimit of its Čech nerve. This means that for every $X$ and every map from the Čech nerve to $X$ , there is a unique map from $\star$ to $X$ such that the diagrams commute. More precisely, the end of the diagram looks like this $Y\times Y\stackrel{\to}{\to} Y\to X$ (with a map from $Y\times Y$ to $X$ and two homotopies inside the triangles (is it possible to use xypic)?) If I call $g_2$ (resp. $g_1$ ) the map from $Y\times Y$ (resp. $Y$ ) to $X$ , then for $x,y\in Y$ I have a path from $g_2(x,y)$ to $g_1(x)$ and another from $g_2(x,y)$ to $g_1(y)$ . So we conclude that $g$ is constant. (I don’t know if I can talk about elements and paths, but given that I can in HoTT, I guess I can here too).

So a map from the Čech nerve to some object $X$ is just a constant function $f:Y\to X$ (meaning that forall (y y' : Y), f y ~~> f y')

The universal property of the colimit then says that such a constant function $f$ factor through $\star$ in a unique (contractible) way.

This gives the following definition in HoTT:

Definition terminal_eff_epi (Y : Type) :
  forall (X : Type) (f : Y -> X) (p : forall y y' : Y, f y ~~> f y'),
  is_contr ({t : Y & forall x, f x ~~> t}).

Is this correct?

If it is, I think that this is not very difficult to pass to general effective epimorphisms. Indeed, $f : X\to Y$ is an effective epimorphism in $H$ iff $f \to (id : X \to X)$ is an effective epimorphism in $H_{/X}$ (where $id : X\to X$ is the terminal object of $H_{/X}$ ). So we can apply the previous proposition, and we should get that $f$ is an effective epimorphism iff every constant map between $Y$ and another object over $X$ factor in a unique way through $id : X\to X$ .

If it’s correct, then it’s good news, because we can talk about effective epimorphisms in HoTT (and effective epimorphisms are used in the proof).

Posted by: Guillaume Brunerie on November 4, 2011 2:29 AM | Permalink | Reply to this

Re: HoTT Cohesion – Exercise I

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

So a map from the Čech nerve to some object $X$ is just a constant function $f : X \to Y$ (meaning that forall (y y' : Y), f y ~~> f y')

[…]

Is this correct?

The reasoning looks quite plausible to me, but I’ll have to think now how this remains true as we translate the languages, using, I suppose, the HoTT↔HTT dictionary. Maybe that’s all automatic now, but a priori it seems to me that one would have to check that your arguments involving just objects and morphisms lifts to higher $k$ -morphisms (in $Y$ , notably).

So let’s see. First of all, we have in HoTT the fibration classified by (please check if my code is okay)

Definition P : Y & Y -> Type := 
  fun y y' => f y ~~> f y' end.

In HTT this is the $\infty$ -pullback

$\array{ P &\to& X \\ \downarrow && \downarrow^{\mathrlap{\Delta}} \\ Y \times Y &\stackrel{(f,f)}{\to}& X \times X }$

in our ambient $(\infty,1)$ -topos $\mathbf{H}$ . Equivalently, in terms of a presentation of the $\mathbf{H}$ by a suitable homotopical category, this is the ordinary pullback

$\array{ P &\to& X^{\Delta[1]} \\ \downarrow && \downarrow^{\mathrlap{X^{\partial \Delta[1] \hookrightarrow \Delta[1]}}} \\ Y \times Y &\stackrel{(f,f)}{\to}& X \times X } \,,$

which also serves to present $P \to Y \times Y$ explicitly by a fibration (since the morphism on the right is a fibration.

Next, the type

forall (y y' : Y), f y ~~> f y'

is the $\infty$ -groupoid $\Gamma_{Y \times Y}(P)$ of homotopy sections of $P \to Y \times Y$ , which is the $\infty$ -pullback

$\array{ \Gamma_{Y \times Y}(P) &\to& \mathbf{H}(Y \times Y, P) \\ \downarrow && \downarrow \\ {\ast} &\stackrel{id}{\to}& \mathbf{H}(Y \times Y, Y \times Y) }$

(or equivalently the ordinary such pullback if we present $\mathbf{H}$ by a suitable model category, and choose $Y \times Y$ to be cofibrant and fibrant, choose $P$ to be fibrant and $P \to Y \times Y$ to be a fibration a above).

(Or is it? Do I maybe, instead of the external homs $\mathbf{H}(Y \times Y, P)$ etc., need to form the internal homs $[Y \times Y, P]$ here? )

So your question

Is this correct?

comes down to the following:

Is it true that a morphism $f : Y \to X$ in $\mathbf{H}$ fits into a diagram of simplicial objects $Y^{\times (\bullet+1)} \to X$ precisely if the $\infty$ -limit object in $\mathbf{H}$ given by

$\Gamma_{Y \times Y}(P):= \Gamma_{Y \times Y}( X \times_{X \times X} (Y \times Y) )$

is (-1)-connected?

That seems to be true. Yes. First, by the universal property of the $\infty$ -pullback one finds (looking at the above squares) an equivalence

$\Gamma_{Y \times Y}(P) \simeq \mathbf{H}_{/ X \times X}(Y \times Y, X) \,.$

So if the left hand is non-empty, this means that on th right we find a homotopy-commuting diagram of the form

$\array{ Y \times Y \\ \downarrow\downarrow & \searrow \\ Y &\stackrel{f}{\to} & X } \,.$

Okay, good! :-) Now I need to make some telephone calls, then I can try to look at the rest of your message.

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

Re: HoTT Cohesion – Exercise I

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

I’ll continue now my above reply.

The universal property of the colimit then says that such a constant function $f$ factor through $\ast$ in a unique (contractible) way.

Yes.

This gives the following definition in HoTT:

Definition terminaleffepi (Y : Type) : forall (X : Type) (f : Y -> X) (p : forall y y' : Y, f y ~~> f y'), is_contr ({t : Y & forall x, f x ~~> t}).

Is this correct?

What’s the precise interpretation of the code { t : Y & P t}? I understand that it means “the space of terms t of Y times the spaces of paths f x ~~> t.” It’s clear that this is the right idea, but I am not sure how I would go about formally verifying that this expresses indeed precisely the universal property of the $\infty$ -colimit. Can you help me here?

Indeed, $f : X \to Y$ is an effective epimorphism in $\mathbf{H}$ iff $f \to (id : X \to X)$ is an effective epimorphism in $\mathbf{H}_{/X}$

Wait. So you mean

iff $f \to (id : Y \to Y)$ is an effective epimorphism in $\mathbf{H}_{/Y}$ .

But I am being dense: what are you using here?

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

Re: HoTT Cohesion – Exercise I

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

What’s the precise interpretation of the code { t : Y & P t}?

It means exactly the same thing as total (fun (t : Y) => P t), it’s the total space of the fibration P (sometimes it’s more natural to write this instead of total, but this is really the same).

It’s clear that this is the right idea, but I am not sure how I would go about formally verifying that this expresses indeed precisely the universal property of the ∞-colimit. Can you help me here?

In fact, to be more precise, I should have written {t : unit -> Y & forall x, f x ~~> t tt} (but this is equivalent). This is the space of homotopy commutative triangles factoring f through $\star$ . Is it enough?

Wait. So you mean iff $f\to(id:Y\to Y)$ is an effective epimorphism in $\mathbf{H}_{/Y}$ .

Hum yes, sorry.

But I am being dense: what are you using here?

No idea :D

There are a lot of places in the nLab where some reasoning looking like that is used, so I was hoping that this is trivial (and true).

Perhaps we can we say something like that (I’m using proposition 1 of this page):

On the one hand, $f : X \to Y$ is an effective epimorphism in $\mathbf{H}$ iff $\tau_{\le-1}(f)$ is terminal in $\mathbf{H}_{/Y}$ , iff $\widetilde{\tau_{\le-1}(f)} : f\to (id : Y\to Y)$ is terminal in $(\mathbf{H}_{/Y})_{/(id:Y\to Y)}$ .

On the other hand, $\widetilde f : f\to(id:Y\to Y)$ is an effective epimorphism in $\mathbf{H}_{/Y}$ iff $\tau_{\le-1}(\widetilde f)$ is terminal in $(\mathbf{H}_{/Y})_{/(id:Y\to Y)}$ .

Then, probably that $\widetilde{\tau_{\le-1}(f)}$ and $\tau_{\le-1}(\widetilde f)$ are equal (?).

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

Re: HoTT Cohesion – Exercise I

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

What’s the precise interpretation of the code { t : Y & P t}?

It means exactly the same thing as total (fun (t : Y) => P t), it’s the total space of the fibration P (sometimes it’s more natural to write this instead of total, but this is really the same).

Ah, thanks!

By the way, am I right that this is also the same as

exists x : X, P x

I have added what you just explained to the dictionary. But I need more help with that dictionary. I am not sure about some of the statements that I currently make there (but there is also a warning to that effect).

Mainly I am not sure about whether several constructions are to be regarded as happening internally or externally.

For instance for X Y : Type we have also

X -> Y : Type

Now what is this really in terms of the ambient $(\infty,1)$ -category $\mathbf{H}$ ? Is it the external hom- $\infty$ -groupoid $\mathbf{H}(X,Y)$ regarded internally by assuming $\mathbf{H}$ to be $\infty$ -tensored over $\infty Grpd$ ? Or are we assuming $\mathbf{H}$ to be cartesian closed and form the internal hom $[X,Y] \in \mathbf{H}$ ? That will in general be a much richer object and will make a big difference.

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

Re: HoTT Cohesion – Exercise I

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

By the way, am I right that this is also the same as exists x : X, P x?

No. The term exists x : X, P x exists in Coq but is never used in HoTT. The reason is that P x need to be a Prop, which is a feature of the calculus of constructions which is not used in HoTT at all.

Now you’ve perhaps seen sentences like exists x. in some Coq files, but this is something completely different. In this case exists is a tactic used to construct terms of type total P.

For instance for X Y : Type we have also X -> Y : Type Now what is this really in terms of the ambient (∞,1)-category H?

I don’t see how it could be the external Hom. It’s a type, so it’s an object of our ambient $(\infty, 1)$ -category, so I think it can only be the internal Hom.

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

Re: HoTT Cohesion – Exercise I

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

The term exists x : X, P x exists in Coq but is never used in HoTT. The reason is that P x need to be a Prop

Hm, too bad. Wouldn’t it be nice to have it mean the total space? Then forall would be the right adjoint and exists the left adjoint to pullback. I thought that was regarded to be a nice fact to have.

When you say “need to be”, what is the need? Is it just that Coq happens to work this way, or do you mean a deeper need?

I would have thought that one should regard exists x : X, P x as the total space, and then in cases where one really wanted it to be a truth value (such as in Lemma exists x : X, P x I suppose) one would implicitly form its (-1)-truncation first.

Independently of whether this is the way it currently works in Coq or not: wouldn’t that be sensible?

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

Re: HoTT Cohesion – Exercise I

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

Hm, too bad. Wouldn’t it be nice to have it mean the total space? Then forall would be the right adjoint and exists the left adjoint to pullback. I thought that was regarded to be a nice fact to have.

Well, there is no problem, what I mean is just that exists x : X, P x is not the correct syntax, the correct syntax is {x : X & P x} (or total (fun x : X => P x)). But it still can be the left adjoint to the pullback functor.

When you say “need to be”, what is the need? Is it just that Coq happens to work this way, or do you mean a deeper need?

exists is a keyword in Coq, so we can’t redefine it to mean something else.

Note also that because forall is a keyword, not a term or a function, it does not mean anything to write forall alone. So it would not even be forall the right adjoint to pullback but probably some “eta-expanded” form of it.

I would have thought that one should regard exists x : X, P x as the total space, and then in cases where one really wanted it to be a truth value (such as in Lemma exists x : X, P x I suppose) one would implicitly form its (-1)-truncation first.

In Coq (not HoTT) there is a special universe called Prop which is supposed to contain the propositions, or truth values. It has some special features like impredicativity (which means that if you quantify on all the universe Prop you will stay in Prop, in Martin-Löf type theory you would end up higher in the universe hierarchy). And the exists x : X, P x is used in Coq when P x is in the universe Prop.

But in the univalent foundations we would indeed do what you describe: to take the $(-1)$ -truncation of the total space. But Coq is not based on the univalent foundations, it’s based on the calculus of constructions (but we can fake it by using only the common subset of both formal systems and adding what’s missing as axioms).

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

Re: HoTT Cohesion – Exercise I

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

in the univalent foundations we would indeed do what you describe: to take the (−1)-truncation of the total space. But Coq is not based on the univalent foundations,

I see. Are there any plans to write some software that would allow to write HoTT code in a more natural way? My impression is that good and natural notation goes a long way in programming in general and in the context of HoTT in particular.

For instance if one really wants to claim that HoTT is a formalization of “ $(\infty,1)$ -logic”, then it seems one will want to allow exists x : X, P x to denote the total space of a bundle, because that’s what it should be in $(\infty,1)$ -logic.

One would just need a simple script that converts the “natural HoTT code” to the actual Coq code.

Of course this is not such a big deal. Just a vain thought now that I am getting tired and will go offline. See you tomorrow! :-)

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

Re: HoTT Cohesion – Exercise I

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

it’s an object of our ambient (∞,1)-category, so I think it can only be the internal Hom.

Indeed.

I could point out that actually actually, it’s probably even more internal than that: after forming the internal Hom, we pass to a global element of the object classifier which classifies it, since what we want is actually a term of type Type in the empty context (or, more generally, whatever context we happen to be working in). But that would probably be overly confusing, so I won’t (oops).

The important point is that everything happens internally; there is no “externally”, except insofar as we put it in manually using operations like $\flat$ . If we wanted to form the “external Hom”, we would have to say something like flat (X -> Y) — that would be the internal discrete object corresponding to the external hom.

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

Re: HoTT Cohesion – Exercise I

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

it’s an object of our ambient (∞,1)-category, so I think it can only be the internal Hom.

Indeed.

Well, if we assume tensoring over $\infty$ -groupoids, then also the external hom becomes an internal object, canonically.

Okay, but if X -> Y is the internal hom, then we need to rethink all the above discussion about characterization of $\infty$ -limits by contractibility of certain mapping spaces. Because the standard statements along these line all refer to the external hom spaces, of course.

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

Re: HoTT Cohesion – Exercise I

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

If X -> Y is the internal hom $[X,Y]$ , what would be the Coq-code that proves the statement

$\forall X, Y, Z, \;\;[X, [Y,Z]] \simeq [X \times Y, Z]$

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

Re: HoTT Cohesion – Exercise I

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

If X -> Y is the internal hom $[X,Y]$ , what would be the Coq-code that proves the statement

∀X,Y,Z,[X,[Y,Z]]≃[X×Y,Z] ?

See here. Basically you define the two functions from one side to the other, and you check that the composites are homotopic to the identities using function extensionality.

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

Re: HoTT Cohesion – Exercise I

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

See here.

Ah. Thanks!

I wish, though, you had said this earlier. I asked about it several times in the above. Because this means now that everything I said about how your code should correspond to $\infty$ -topos theory needs to be re-thought. I was all arguing with the external hom-spaces $\mathbf{H}(X,Y)$ .

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

Re: HoTT Cohesion – Exercise I

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

Now that I understand the { ... }-notation I can at least try to further unwind the HTT meaning of Guillaume’s HoTT code. But I’ll keep running into the problem I mentioned: I am not sure whether to interpret some things internally or externally.

First of all

fun (x : X) => f x ~~> t

is the homotopy fiber $hofib(f)$ over $t$ in

$\array{ hofib(f) &\to& {*} \\ \downarrow && \downarrow \\ X &\stackrel{f}{\to}& Y } \,.$

Then

forall x, f x ~~> t

is its space of homotopy sections $\sigma$

$\array{ && hofib(f) &\to& {*} \\ &{}^{\mathllap{\sigma}}\nearrow& \downarrow && \downarrow \\ X &\stackrel{=}{\to}& X &\stackrel{f}{\to}& Y } \,,$

which by the universal property of the $\infty$ -pullback is

$\mathbf{H}_{/ Y}(f, t)$

(or maybe the internal version of that(?)).

So then

{t : Y & forall x, f x ~~> t}

should maybe be externally the Cartesian fibration classified by

$\Gamma Y \stackrel{\simeq}{\to} \mathbf{H}(\ast, Y) \stackrel{\mathbf{H}_{/Y}(f,-)}{\to} \infty Grpd \,.$

I may need to think a bit more, but requiring that to be contractible should be the right condition for the $infty$ -colimit.

But now I really first need to sort out this external/internal problem.

Can anyone help??

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

Re: HoTT Cohesion – Exercise I

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

My initial inclination would have been to define $f\colon X\to Y$ to be an effective epimorphism if forall y:Y, is_inhab { x : X & f x ~~> y }. That is, since we expect to have a factorization system into effective-epis and monos, a map should be effective-epi if and only if its reflection into monos is an equivalence.

Guillaume’s approach looks clever too, though, but I haven’t fully understood it yet. One question first: is forall (y y' : Y), f y ~~> f y' necessarily a prop?

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

Re: HoTT Cohesion – Exercise I

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

Guillaume’s approach looks clever too, though, but I haven’t fully understood it yet.

Me neither :D I don’t really know what are effective epimorphisms, so I just tried to unwrap the definition.

One question first: is forall (y y' : Y), f y ~~> f y' necessarily a prop?

Indeed, this is not a prop (take Y := unit). But it’s probably not really a problem, calling such a f a “constant function” was just a bad terminology. I don’t know how I should call it then, perhaps “homotopically constant”? (in the same way as a homotopy-commutative square is a structure rather than a property).

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

Re: HoTT Cohesion – Exercise I

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

As a first stab at comparing the two definitions, the impredicative coding of is_inhab would be:

Definition is_inhab Y := forall (X : Type), (Y -> X) -> (forall (x1 x2:X), x1 ~~> x2) -> X.

Note that this is very close to Guillaume’s definition of when $Y\to \star$ should be effective epi. There are two differences:

The impredicative coding of is_inhab outputs only an element of X, rather than the contractibility of { t : X & forall y, f y ~~> t } (I presume this is what was meant?). However, since one of its hypotheses is that X is a prop, being given a point of X implies that X is contractible, which then implies that its path spaces are contractible, so the stronger conclusion should be provable.
The impredicative coding of is_inhab assumes that X is a prop, rather than forall y y' : Y, f y ~~> f y'. Guillaume’s version is somewhat nicer in this way; it’s bothered me for a while that is_inhab only lets you eliminate into props, rather than via a “constant function” into any type.
While I’m at it, I should mention that the higher-inductive definition of is_inhab also has a dependent eliminator, while neither its impredicative encoding nor Guillaume’s definition do so. However, I don’t think we’ve ever found a use for the dependent eliminator of is_inhab.

However, I’m still worried that forall y y' : Y, f y ~~> f y' may not be a prop. Actually, I think that it obviously will not always be; for instance if Y is unit, then forall y y' : Y, f y ~~> f y' is just f tt ~~> f tt, which is not a prop in general. This isn’t necessarily a problem, since Guillaume’s terminal_eff_epi will itself be a prop regardless (since is_contr is a prop and forall preserves props no matter what you quantify over). But it makes me uneasy.

In particular, at the end of this comment, Urs derives from Guillaume’s definition a homotopy-commuting diagram $\array{ Y\times Y \\ \downarrow\downarrow & \searrow \\ Y & \to & X}$ But can you extend this to the whole Cech nerve of $Y\to \star$ ? It’s not obvious to me.

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

Re: HoTT Cohesion – Exercise I

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

But can you extend this to the whole Cech nerve of Y→⋆? It’s not obvious to me.

Yes (I think). Suppose that you have extended this to the Čech nerve of $Y\to\star$ up to the function $f_n:Y^n\to X$ (we will start with $n = 2$ ), and for $0\le k\le n$ call $\pi^n_k:Y^{n+1}\to Y^n$ the projection where you forget the $k$ -th term.

What we need is to find a map $f_{n+1}:Y^{n+1}\to X$ and homotopies between $f_{n+1}$ and $f_n\circ\pi^n_k$ for all $0\le k\le n$ (am I right?)

Let $f_{n+1} := f_n\circ\pi^n_0$ and let $k$ be such that $1\le k\le n$ (there is nothing to prove for $k = 0$ ). By induction hypothesis, we have an homotopy between $f_n$ and $f_{n-1}\circ\pi^{n-1}_{k-1}$ and another one between $f_n$ and $f_{n-1}\circ\pi^{n-1}_0$ . So in order to find an homotopy between $f_{n+1}$ and $f_n\circ\pi^n_k$ , we just have to find an homotopy between $f_{n-1}\circ\pi^{n-1}_{k-1}\circ\pi^n_0$ and $f_{n-1}\circ\pi^{n-1}_0\circ\pi^n_k$ . But these two maps are equal, so we have one.

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

Re: HoTT Cohesion – Exercise I

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

What we need is to find a map $f_{n+1}\colon Y_{n+1}\to X$ and homotopies between $f_{n+1}$ and $f_{n}\circ \pi_k^n$ for all $0\le k\le n$ (am I right?)

I don’t think that’s all we need. Even laying aside the question of degeneracies (semi-simplicial Cech nerves are hard enough), we also need all those homotopies to be coherent. For instance, we need a homotopy between the two homotopies

$f_{n-1} \pi^{n-1}_i \pi^{n}_j \to f_n \pi^n_j \to f_{n+1}$

and

$f_{n-1} \pi^{n-1}_{j-1} \pi^n_i \to f_n \pi^{n_i} \to f_{n+1}$

(whose domains are equal, by one of the identities of a simplicial object). And higher homotopies, and so on.

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

Re: HoTT Cohesion – Exercise I

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

I have now finally found the time to go through Guillaume’s code in detail. This is very helpful for me. I would never have been able to come up with this code myself, at this stage.

I think I essentially understand what’s happening in each line, but there are a few coding details that I am not fully sure about. So I’ll ask now a bunch of questions, most of them just about absolute basics of Coq.

The first line says.

Parameter BG : Type.

So I guess Parameter I should read as “Let”, as in “Let there be an object (a term of type Type) to be called BG”.

The next line says

Axiom pt : BG.

Could we exchange Axiom with Parameter here?

(On the one hand we say “Let $\mathbf{B}G$ be an object and let $\ast \stackrel{pt}{\to} \mathbf{B}G$ be a morphism”, on the other we might equivalently say “Let $\mathbf{B}G$ be an object and assume that there is a morphism $\ast \stackrel{pt}{\to} \mathbf{B}G$ .” ?)

Then when it says something of the form

Lemma x : X

the idea is that we say “There is a term x of type X”, right? Or “The type X is inhabited.” Right?

A few lines further below is the first occurence of a keyword that I don’t know

 tpair _ (flat_is_coreflection BG unit is_discrete_unit).

What does tpair refer to, and what is the underscore doing here?

I was a bit surprised to see the line

Definition pt_flat_fun : unit -> flat BG := eq_points_flatBG_BG^-1 pt_fun.

I understand what it says, but I am wondering what the computer makes of that ^-1, because these homotopy inverses are not unique.

Then I wondered a bit about the line

Definition pt_compatible : map_from_flat BG pt_flat ~~> pt := map (fun p => p tt) pt_compatible_fun.

I understand that (or believe I understand that) this is taking the $\infty$ -groupoid that I might denote

$\mathbf{H}^{\Delta[1]}(\ast \to \mathbf{\flat}\mathbf{B}G \to\mathbf{B}G, \ast \to \mathbf{B}G)$

and then applies an evaluation that takes natural transformations to their components on the point. But could somebody maybe say a word about how exactly the code

map (fun p => p tt) pt_compatible_fun.

takes care of this?

In the very last line,

fun l => tpair pt_flat (pt_compatible @ l).

I see what is being said, but need again help with the precise meaning of that tpair.

Finally, the file ends with defining a map $\theta : G \to \mathbf{\flat}_{dR} \mathbf{B}G$

Definition theta : G -> flat_dR_BG := fun l => tpair pt_flat (pt_compatible @ l).

but should we not also have a Lemma or something that asserts that this is indeed the canonical such morphism, up to equivalence, namely the one induced by the universal property of the homotopy fiber?

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

Re: HoTT Cohesion – Exercise I

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

Never mind the tpair-question, I have looked it up in Voevodsky’s Bonn talk notes.

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

Re: HoTT Cohesion – Exercise I

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

Could we exchange Axiom with Parameter here? (On the one hand we say “Let BG be an object and let ∗−→ptBG be a morphism”, on the other we might equivalently say “Let BG be an object and assume that there is a morphism ∗−→ptBG.” ?)

First of all, Axiom and Parameter mean really exactly the same thing to Coq, you can write the one you want, it will always work.

But just as you said, I like to think of Parameter as a “Let” and Axiom as “Assume that”, so what I wanted to say is “Let BG be an object such that BG is connected (and such that there is a point pt:BG)”

But this is really a minor point, the two mean the same thing.

Then when it says something of the form Lemma x : X the idea is that we say “There is a term x of type X”, right? Or “The type X is inhabited.” Right?

Yes, I tell Coq that there is a term x of type X. Of course, Coq does not trust me (or does not know which term of type X I want), so there is a Proof. [...] Defined. block in which I construct step by step this term x of type X.

What does tpair refer to, and what is the underscore doing here?

tpair is used to construct terms of a dependent sum type. If P:A->Type is a fibration, the dependent sum (total space of P) is denoted by total P, and if a is of type A and t of type P a, you have tpair a t : total P.

The underscore means “I do not want to write this term, please guess what I mean”. In this case, I want to create an equivalence (recall that an equivalence is a dependent pair tpair f e where f is a function and e a proof that f is an equivalence), and the term flat_is_coreflection ... is already a proof that some function is an equivalence, so Coq should be (and is) able to guess what this function is.

I am wondering what the computer makes of that ^-1, because these homotopy inverses are not unique.

You can prove that if you have an equivalence, then there is an equivalence in the other direction. So this gives you a Coq function transforming an equivalence into “its” inverse. Using Coq’s notation mechanism, this inverse of an equivalence e is denoted e-¹ (instead of inverse e). I do not think that the fact that the inverse is not unique is a problem (but I guess that the inverse is unique up to homotopy?).

But could somebody maybe say a word about how exactly the code map (fun p => p tt) pt_compatible_fun. takes care of this?

First of all (perhaps you already know this, but I do not find it intuitive at all), unit is the type corresponding to the terminal object and its unique point is named tt (it is implemented with an inductive type with only one constructor). For example, the elimination rule of unit says that in order to build a map unit -> A, you just have to say what is the image of tt.

map takes a function f : A -> B and a path p : x ~~> y in A, and transform it into a path map f p : f x ~~> f y (in B). map f is a witness of the functoriality of f on paths.

Here, A is the type of maps unit -> BG, B is BG and f is the evaluation at tt.

In the very last line, I see what is being said, but need again help with the precise meaning of that tpair.

You’ve probably already understood, a point of the homotopy fiber is a (dependent) pair of a point and a path, so I’m using tpair to build the pair.

should we not also have a Lemma or something that asserts that this is indeed the canonical such morphism, up to equivalence, namely the one induced by the universal property of the homotopy fiber?

Indeed, I just constructed $\theta$ without proving anything about it. I know that this is the map induced by the pullback diagram of the homotopy fiber because I proved the universal property of the pullback here and so I know how to build the map induced by the universal property of the pullback.

What should I do? I will try to use the map I defined in my Pullbacks.v file in the definition of theta, but this will be a little more complicated and the reader will need to understand also the content of the file Pullback.v. Or perhaps there is another simple property I could prove about theta to be sure it’s the right function?

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

Re: HoTT Cohesion – Exercise I

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

I will try to use the map I defined in my Pullbacks.v file in the definition of theta, but this will be a little more complicated and the reader will need to understand also the content of the file Pullback.v.

I added the new definition of theta and a proof that the two definitions give the same function.

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

Re: HoTT Cohesion – Exercise I

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

But just as you said, I like to think of Parameter as a “Let” and Axiom as “Assume that”, so what I wanted to say is “Let $B G$ be an object such that $B G$ is connected (and such that there is a point pt:BG)”

Except that BG is not a Prop, so postulating a point in BG is structure rather than a property. I usually only say “assume that” when what I’m assuming is a property, rather than a structure. “Assume that $B G$ is connected” would translate into Coq for me as an axiom that is_inhab BG, which is a Prop. So if one is inclined to make the distinction, I would tend to agree that your pt : BG should be a parameter rather than an axiom. But as you say, it makes little difference.

You can prove that if you have an equivalence, then there is an equivalence in the other direction. So this gives you a Coq function transforming an equivalence into “its” inverse.

More precisely, recall that as discussed here, the proposition $IsEquiv(f)$ is defined (or might as well be defined) so that an inhabitant of it consists of a coherent homotopy inverse to $f$ . That is, to prove that a map is an equivalence consists of giving a coherent homotopy inverse to it. Therefore, if we are given a proof that a map $f$ is an equivalence, there is a definite, constructive way to extract from that proof the “inverse” of $f$ , which we can therefore give a notation to.

Of course, in order to extract the inverse, we need not only the map $f$ , but the proof that it is an equivalence. In order to be able to say “ $f^{-1}$ ” when $f$ is an equivalence, we define an equivalence to mean “a function, together with a proof that that function is an equivalence”. (Of course, this is a dependent sum type.) Coq then has a nice “coercion” mechanism which allows us to say “if I have an equivalence — that is to say, a function together with a proof that it is an equivalence — then I can treat that object as if it were a function and apply it to an argument. When I do that, what I mean is to just throw away the proof and apply the underlying function.” Thus we can write both $f(x)$ and $f^{-1}$ for the same object $f$ .

(What we can’t do, the way the code is currently set up, is write $(f^{-1})^{-1}$ , because the operation of inversion only extracts a function, rather than a function together with a proof that that function is an equivalence. It would be easy to improve the code to do that, though.)

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

Re: HoTT Cohesion – Exercise I

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

Note that I needed to use univalence in order to prove that the point is discrete

Yes, in retrospect, that necessity is obvious from how we formulated pi_preserve_terminal. We could instead have used the axiom is_discrete unit, which ought to imply that is_equiv (map_to_pi unit) (and also is_equiv (map_from_flat unit)) by a somewhat longer argument not requiring univalence. Perhaps that would be cleaner.

I don’t really mind using univalence, though. We’re going to need that anyway if we want to know more generally that anything equivalent to a discrete object is discrete, which seems like a useful thing.

By the way, I have written a post over at the HoTT blog to let them know what’s going on here.

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

Read the post HoTT Cohesion -- Exercise II
Weblog: The n-Category Café
Excerpt: How to code in homotopy type theory the intrinsic definition of ordinary differential cohomology and the proof of its basic properties?
Tracked: November 9, 2011 10:39 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 Flat Ehresmann connections in Cohesive HoTT
Weblog: The n-Category Café
Excerpt: The formalization of flat Ehresmann connections in higher geometry.
Tracked: June 28, 2012 6:38 PM

The n-Category Café

Skip to the Main Content

November 2, 2011