strict infty-groupoids

[Vladimir Voevodsky]

While reading Michael Warren paper on the strict infty-groupoids model the following thought occurred to me.

I would conjecture that this model can be extended to interpret some higher inductive types e.g. that it can extended to interpret spheres.

If this is the case we will obtain a proof that the computations of pi_3(S^2) and pi_4(S^3) can not be done without univalence.

Indeed, in the strict infty-groupoid model the higher homotopy groups of spheres are zero. That would imply both that this model does not interpret univalence (which is probably not surprising) and that there is no construction of the Hopf map that does not use univalence.

Vladimir.

[Nicolai Kraus]

That sounds plausible. Regarding homotopy groups of spheres, isn't it
the case that the naive Set-model allows to interpret basically
everything apart from univalence? I thought that UIP and HITs are
completely compatible with each other, apart from the fact that the
power of HITs will be quite limited compared to the setting with
univalence. But with UIP, those homotopy groups will of course be trivial.
Nicolai

[Dan Licata]

I agree that there should be a model in sets interpreting the spheres higher inductives where *all* of the homotopy groups of spheres are 0.

But in strict oo-groupoids, won't you have pi_n(S^n) = Z? (but the ones above the diagonal being 0)

I remember thinking when doing the proof of of pi_n(S^n) that what you needed to get the induction to go through was: to prove pi_n+1(S^n+1) = Z, you need a univalent universe containing K(Z,n) (the n-truncation of S^n). (Take this with a grain of salt, since it's been a while and I didn't check it in detail.)

So to interpret the proof of pi_n(S^n), I think we'd only need one univalent universe closed under KG(Z,n)'s. Does that exist in strict oo-groupoids?

-Dan

> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Paolo Capriotti]

On Tue, Nov 11, 2014 at 2:09 PM, Dan Licata <d...@cs.cmu.edu> wrote:
> So to interpret the proof of pi_n(S^n), I think we'd only need one univalent universe closed under KG(Z,n)'s. Does that exist in strict oo-groupoids?

No. You can prove that every univalent universe in the strict
∞-groupoid model contains only sets. In fact, let U be such a
universe, and let X : U be a type in it. If x : X, the singleton

(y : X) × (x = y)

is a contractible type, hence equal to 1 by univalence. Therefore,
there is a term

p : ((y : X) × (x = y)) = 1

Since U itself is a strict groupoid, p⁻¹ · p ≡ idp, where ≡ is strict
equality. Hence, for every y : X, and q : x ≡ y, we have:

(y, q) ≡ coerce p⁻¹ (coerce p (y, q)) ≡ coerce p⁻¹ 0

In fact, transport is strictly functorial in this model, and coerce is
transport along the identity. In particular, if q, q' : x = y are two
equality proofs:

(y, q) ≡ coerce p⁻¹ 0 ≡ (y , q')

Since the equality is strict, it follows that q ≡ q', hence X is a set.

Paolo

[Martin Escardo]

On 11/11/14 12:19, Vladimir Voevodsky wrote:

> we will obtain a proof that the computations of pi_3(S^2) and
> pi_4(S^3) can not be done without univalence.

I think we already know that, as Nicolai said, and as discussed in
https://github.com/HoTT/book/issues/736

Without univalence, even the value of pi_1(S^1) is undecided:

With the K axiom (UIP), any loop space is the initial-terminal group.

With the univalence axiom, it is Z (which is of course what we want).

But each of these axioms is consistent with MLTT.

Hence in MLTT+S^1 without further axioms, nothing conclusive can be
said about pi_1(S^1), and the same reasoning applies to the examples
you give above.

And in MLTT+S^1 without an axiom contradicting K, such as univalence,
we can't get pi_1(S^1)=Z, and the same reasoning applies to your
examples to get the desired pi_1.

Martin

[Michael Shulman]

On Tue, Nov 11, 2014 at 6:09 AM, Dan Licata <d...@cs.cmu.edu> wrote:
> I agree that there should be a model in sets interpreting the spheres higher inductives where *all* of the homotopy groups of spheres are 0.

Yes. In fact, HITs can be constructed in the extensional type theory
of any locally presentable lccc, but since axiom K holds therein,
nothing has any higher homotopy groups.

It's an interesting question, though, whether there is some weaker
form of univalence that holds in strict oo-groupoids that would allow
one to prove pi_n(S^n) = Z. Of course, a univalent universe of *sets*
suffices for pi_1(S^1) = Z, but not for n>1 (since e.g. the groupoid
model contains a univalent universe of sets, but S^n is contractible
therein for n>1).

[Vladimir Voevodsky]

Yes, I guess there is a simpler way of showing that the homotopy groups of spheres can not be computed without the univalence. I suppose the strict infty groupoid model is still interesting as an example where interpretations of of the higher inductive types are non-trivial but different from the univalent interpretation.

There is also something that I do not quite understand. What if we represent a (finite) CW-complex X as a higher inductive type using, e.g., cofibers. Will it be possible to interpret it as a strict groupoid and if so then which one?

Will it even be possible to do it with S^3 given the arguments of the Simpson’s counterexample to my paper with Kapranov?

And if it is not possible then where precisely things go wrong and what are the extra conditions on the model that need to be satisfied for it to be possible to interpret cofibers in it?

Vladimir.

[Jason Gross]

Does functoriality of transport being strict follow from the strictification of the ∞-groupoid laws at all levels?  Said another way, how do you deduce that [coerce p (y, q) ≡ 0]?

-Jason

[Michael Shulman]

On Tue, Nov 11, 2014 at 12:06 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> There is also something that I do not quite understand. What if we represent a (finite) CW-complex X as a higher inductive type using, e.g., cofibers. Will it be possible to interpret it as a strict groupoid and if so then which one?

I'm not completely sure. I think Michael constructed the strict
oo-groupoid model explicitly, rather than by using model-categorical
machinery, so it's not immediately obvious that Peter's and my general
construction of HITs can be applied therein. But I would be surprised
if at least simple non-recursive HITs didn't exist there. Maybe
Michael or Peter has thought about this?

As for what they are if they exist, one reasonable-sounding (to me)
guess is that the HIT S^n would be interpreted by the oo-groupoid
K(Z,n).

Mike

[Guillaume Brunerie]

On 2014-11-11 13:19 GMT+01:00 Vladimir Voevodsky <vlad...@ias.edu> wrote:
> That would imply [that] there is no construction of the Hopf map that does not use univalence.

Just to clarify this point, you don’t need univalence to construct the
Hopf map : S^3 -> S^2.
But you need univalence to prove that this map is non-trivial.
It’s the same as for S^1, you can always construct the "generator" of
pi_1(S^1) as a map S^1 -> S^1 (it’s the identity function), but
without univalence this function could be constant.

Guillaume

[Paolo Capriotti]

On Wed, Nov 12, 2014 at 2:49 AM, Jason Gross <jason...@gmail.com> wrote:
> Does functoriality of transport being strict follow from the strictification
> of the ∞-groupoid laws at all levels? Said another way, how do you deduce
> that [coerce p (y, q) ≡ 0]?

No, it doesn't follow. However, I believe it holds in the strict ∞-groupoid
model as presented by Michael Warren, since types correspond to strict
∞-functors into the strict ∞-category of strict ∞-groupoids. I haven't checked
the details, though.

Interestingly, there are non-split models of strict groupoids with univalent
universes containing (at least) 1-types. Here's an example: take the category
of groupoids, with the comprehension category structure given by groupoid
fibrations.

We can build a univalent universe U as follows:

- the objects of U are "small" groupoids (i.e. say groupoids in a fixed
Grothendieck universe)
- the morphisms of U are homotopy classes of equivalences

We can build a universal fibration V → U similarly:

- the objects of V are small pointed groupoids
- the morphisms between (X, x) and (Y, y) are pairs of a function f : X → Y, and
a morphism p : Y(f x, y), again modulo homotopy.

It seems that U is a proper strict universe. Univalence should follow from the
fact that equality in U is defined to be exactly equivalence of
groupoids. Furthermore, U contains all small groupoids, hence many 1-types.

Of course, this is not yet a model of type theory as we know it, since the
comprehension category structure is fundamentally non-split (non-cloven,
even). I don't quite see immediately what happens to U after strictification:
does it stop being a universe, or does it lose univalence?

Also, can one prove that any model in which the groupoid laws hold strictly
cannot have a univalent universe containing more than sets?

Paolo

[Thomas Streicher]

The old groupoid model of Martin and myself has already been observed
to be a model of univalence. Of course, it gets trivial at higher
dimensions. But one shouldn't factorize modulo isomorphism but instead
interpret equality as isomorphism.

Thomas

On Wed, Nov 12, 2014 at 11:42:59AM +0000, Paolo Capriotti wrote:
> On Wed, Nov 12, 2014 at 2:49 AM, Jason Gross <jason...@gmail.com> wrote:
> > Does functoriality of transport being strict follow from the strictification

> > of the ???-groupoid laws at all levels? Said another way, how do you deduce
> > that [coerce p (y, q) ??? 0]?
>
> No, it doesn't follow. However, I believe it holds in the strict ???-groupoid

> model as presented by Michael Warren, since types correspond to strict

> ???-functors into the strict ???-category of strict ???-groupoids. I haven't checked

> the details, though.
>
> Interestingly, there are non-split models of strict groupoids with univalent
> universes containing (at least) 1-types. Here's an example: take the category
> of groupoids, with the comprehension category structure given by groupoid
> fibrations.
>
> We can build a univalent universe U as follows:
>
> - the objects of U are "small" groupoids (i.e. say groupoids in a fixed
> Grothendieck universe)
> - the morphisms of U are homotopy classes of equivalences
>

> We can build a universal fibration V ??? U similarly:

>
> - the objects of V are small pointed groupoids

> - the morphisms between (X, x) and (Y, y) are pairs of a function f : X ??? Y, and

[Paolo Capriotti]

On Wed, Nov 12, 2014 at 12:02 PM, Thomas Streicher
<stre...@mathematik.tu-darmstadt.de> wrote:
> The old groupoid model of Martin and myself has already been observed
> to be a model of univalence. Of course, it gets trivial at higher
> dimensions. But one shouldn't factorize modulo isomorphism but instead
> interpret equality as isomorphism.

You can do that, but then the universe is not univalent unless you
restrict it to sets. If you want both univalence and higher types, you
need to take equivalences modulo homotopy.

Paolo

[Thomas Streicher]

But I am afraid you can't factorize by equivalences and instead have
to consider higher dimensional groupoids.

Thomas

[Steve Awodey]

peraps you have a different construction of the Hopf map, Guillaume,
but the one that Peter gave does use UA to determine a family
H : S^2 —> U
and then the challenge is to show that its total space Sigma H is S^3.

Steve

[Peter LeFanu Lumsdaine]

On Wed, Nov 12, 2014 at 12:42 PM, Paolo Capriotti <pa...@capriotti.io> wrote:

On Wed, Nov 12, 2014 at 2:49 AM, Jason Gross <jason...@gmail.com> wrote:
> Does functoriality of transport being strict follow from the strictification
> of the ∞-groupoid laws at all levels?  Said another way, how do you deduce
> that [coerce p (y, q) ≡ 0]?

No, it doesn't follow.  However, I believe it holds in the strict ∞-groupoid
model as presented by Michael Warren, since types correspond to strict
∞-functors into the strict ∞-category of strict ∞-groupoids.  I haven't checked
the details, though.

I’d second this — it holds in Michael’s model due to the strict functoriality of types, but it seems conceivable that there might be a version of the strict ω-groupoid model in which types are modelled as something like general fibrations/weak ω-functors, in which case functoriality of transport would not necessarily hold.

Interestingly, there are non-split models of strict groupoids with univalent
universes containing (at least) 1-types.  Here's an example: take the category
of groupoids, with the comprehension category structure given by groupoid
fibrations.

We can build a univalent universe U as follows:

- the objects of U are "small" groupoids (i.e. say groupoids in a fixed
  Grothendieck universe)
- the morphisms of U are homotopy classes of equivalences

It seems that U is a proper strict universe. Univalence should follow from the
fact that equality in U is defined to be exactly equivalence of
groupoids.

I don’t quite see this.  Surely Id_U(a,b) will come out here as an hset — specifically, the discrete groupoid on π0 of the actual groupoid of equivalences from El(a) to El(b), which (before π0) will not necessarily be an h-set?

> Also, can one prove that any model in which the groupoid laws hold strictly cannot have a univalent universe containing more than sets?

Ooh, that’s a fun question :-)

Since every weak 2-groupoid is equivalent to a strict one, it seems somewhat plausible that one should be able to get a univalent universe of groupoids by taking a strictification of the weak 2-groupoid of groupoids and equivalences.  But whether the element fibration over this survives the strictification would depend, I guess, on how the ambient weak 2-groupoid model looks.  Has this been worked out?  I have a tenuous recollection of hearing someone talk about this, but I’m afraid I’ve forgotten who it was.  (Or I might have dreamt it.)

The smallest obstruction to general strictification, as far as I know, is the non-triviality of braiding in a weak 3-groupoid, which shows up in the 3-groupoid of 2-groupoids.  This suggests at least that there can’t be a univalent universe that looks like the “genuine universe of all 2-groupoids” — but it doesn’t seem immediately clear how to get a precise statement out of this idea.

–p.

[Peter LeFanu Lumsdaine]

On Wed, Nov 12, 2014 at 3:58 PM, Steve Awodey <awo...@cmu.edu> wrote:

peraps you have a different construction of the Hopf map, Guillaume,
but the one that Peter gave does use UA to determine a family
H : S^2 —> U
and then the challenge is to show that its total space Sigma H is S^3.

I think there are two different things getting called the Hopf map here: a map S^3 -> S^2, and a map S^2 -> U giving its fibers.  The latter requires univalence to construct, as Steve said; the former doesn’t, as Guillaume said.  (It comes just from the braiding of S^2, applied to the generating 2-cell.)  In proving the fundamental properties of the fibration, one needs both of these as ingredients.

–p.

[Michael Shulman]

On Wed, Nov 12, 2014 at 3:42 AM, Paolo Capriotti <pa...@capriotti.io> wrote:
> We can build a univalent universe U as follows:
>
> - the objects of U are "small" groupoids (i.e. say groupoids in a fixed
> Grothendieck universe)
> - the morphisms of U are homotopy classes of equivalences

As Thomas said, this doesn't work. If this is a universe (which I'm
not sure of), then it would contain S^1. But no univalent universe
containing S^1 can be a 1-type (since Aut(S^1) is not a set), whereas
all types in the groupoid model are 1-types.

[Paolo Capriotti]

Ah, right, of course. Thanks.

Paolo

[Michael Shulman]

On Wed, Nov 12, 2014 at 8:34 AM, Peter LeFanu Lumsdaine
<p.l.lu...@gmail.com> wrote:
> Since every weak 2-groupoid is equivalent to a strict one, it seems somewhat
> plausible that one should be able to get a univalent universe of groupoids
> by taking a strictification of the weak 2-groupoid of groupoids and
> equivalences. But whether the element fibration over this survives the
> strictification would depend, I guess, on how the ambient weak 2-groupoid
> model looks. Has this been worked out? I have a tenuous recollection of
> hearing someone talk about this, but I’m afraid I’ve forgotten who it was.

It might have been me; at Princeton I worked out enough to mostly
convince myself there is a weak 2-groupoid model in which the
2-groupoids are very slightly strict in a way that matches the type
theory (the composite of an identity morphism with itself is itself
again on the nose) and the functors are likewise slightly strict
(preserving identity morphisms on the nose, a.k.a. "normal"). I think
the fibrations were the fully weak 2-fibrations, i.e. lifting
isomorphisms on hom-groupoids and lifting equivalences. The problem
(or, at least, one problem) is of course that pullbacks of weak
functors don't generally exist; but I think the pullback of a
2-fibration along a normal functor does exist. I don't remember if I
worked out what a universe should look like, though.

[Michael Shulman]

On Wed, Nov 12, 2014 at 11:38 AM, Michael A. Warren
<m.alton...@gmail.com> wrote:
> There is presumably a model structure on strict oo-groupoids which corresponds to these in the same way that the usual “folk" model structure on groupoids corresponds to the notion of split Grothendieck fibrations of groupoids.

I would have said that the canonical model structure on 1-groupoids
corresponds to *non-split* fibrations. Certainly its
model-categorical fibrations are not necessarily split.

[Michael Shulman]

Michael has asked me to forward this to the list.

---------- Forwarded message ----------
From: Michael A. Warren <m.alton...@gmail.com>
Date: Wed, Nov 12, 2014 at 11:38 AM
Subject: Re: [HoTT] strict infty-groupoids
To: Michael Shulman <shu...@sandiego.edu>
Cc: Vladimir Voevodsky <vlad...@ias.edu>, Nicolai Kraus
<nicola...@gmail.com>, Peter LeFanu Lumsdaine
<p.l.lu...@gmail.com>, "HomotopyT...@googlegroups.com"
<HomotopyT...@googlegroups.com>


Types in my strict oo-groupoid model are interpreted as the
oo-categorical version of split Grothendieck fibrations. There are
two ways one could go about investigating HITs in this setting (which
I haven’t done and don’t currently have the luxury of having time to
do):

(1) Attempt to calculate the HITs explicitly. This would be in
keeping with what I’ve done in my paper and could be useful in places
where one needs an explicit recipe for calculating things. On the
other hand, calculations in strict oo-groupoids can be quite involved.

(2) From what I gather, it is more convenient when reasoning about the
semantics of HITs to work with an actual weak factorization system (or
model structure). There is presumably a model structure on strict

oo-groupoids which corresponds to these in the same way that the usual
“folk" model structure on groupoids corresponds to the notion of split

Grothendieck fibrations of groupoids. It is possible that the
appropriate model structure comes from the groupoid version of the
Lafont-Métayer-Worytkiewicz “folk” model structure on strict
oo-categories, but this is something that would have to be checked.
One would then use the abstract machinery of Mike and Peter to show
that HITs can be interpreted in this setting. Then I suppose one
should appeal to some coherence theorem or other to get an actual
model of type theory back (although this may not be needed to simply
investigate the properties of the HITs).

As far as what the S^n are Mike’s guess is as good as any I could
make. Perhaps some of the work of Richard Steiner and other’s on
strict oo-categories and chain complexes might be of use for
investigating HITs in this model.

Sorry that I can’t give a more definitive answer at this time.

Best,

Michael

[Michael Shulman]

And this.

---------- Forwarded message ----------
From: Michael A. Warren <m.alton...@gmail.com>
Date: Wed, Nov 12, 2014 at 11:42 AM
Subject: Re: [HoTT] strict infty-groupoids
To: Michael Shulman <shu...@sandiego.edu>

> On Nov 12, 2014, at 11:40 AM, Michael Shulman <shu...@sandiego.edu> wrote:
>
>> There is presumably a model structure on strict oo-groupoids which corresponds to these in the same way that the usual “folk" model structure on groupoids corresponds to the notion of split Grothendieck fibrations of groupoids.
>
> I would have said that the canonical model structure on 1-groupoids
> corresponds to *non-split* fibrations. Certainly its
> model-categorical fibrations are not necessarily split.

When I say correspond, I mean that they are related not that the
fibrations in the model structure are split which of course I know
they are not.