Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: type theory & logic

Topic: Model of univalence

Verity Scheel (May 05 2021 at 16:07):

One more comment on metatheorems: this business about “closed terms” is crucial, and it’s a meta property: it cannot be expressed internally. You could postulate something like $\forall (f : \forall A, A \to A), \forall A, \forall (a : A), f_A(a) = a$ to state something like the metatheorem internally. But now it applies to all terms, not just closed terms! The internal logic cannot treat open and closed terms differently. So you end up extrapolating a property of closed terms to a property of all terms. But intuitively we assume that, in a computable type theory, $f$ will _eventually_ be a closed term, will _eventually_ by the identity function, and so no contradiction will occur. So there really is something “meta” about that theorem.

Leopold Schlicht (May 05 2021 at 17:38):

Thanks all!
Mike Shulman said:

I just don't get why spaces should be so essential to univalence.

Would you get it if we said "$\infty$-groupoids" instead of "spaces"?

No, I'm not yet really comfortable with considering either "space" or "$\infty$-groupoid" as primitive notions in a foundational system. However, I completely accept using HoTT as an internal language (rather than a foundational system). From that perspective, the second quote just says that univalence is true in the internal language of the category of Kan complexes (or something like that). But when mathematicians are using the principle "isomorphic structures have the same structural properties" in practice, I think they are not working in the internal language of the category of Kan complexes. So I don't agree with the undertone of the first quote suggesting that univalence gives a sort of justification of a statement mathematicians are already using (but maybe I'm over-interpreting!).
If I remember correctly, Solomon Feferman has written a paper in which he argues that a foundational system shouldn't axiomatize the notion of "category" as a primitive concept (the same argument applies to "$\infty$-groupoid"). I guess this was in reaction to Lawvere's ETCC. The reason is that some notion of a "collection of things" is psychologically necessary to understand the notion of a "category".
Looking forward to hearing arguments that enable me to change my opinion. :-)

Kenji Maillard (May 05 2021 at 17:51):

I think the point in the context of Martin-Löf Type Theory is that you do not formalize the notion of $\infty$-groupoid but automatically obtain such structure externally from the iteration of identity types and the algebra of paths operations that are definable from induction on identity types (this happens even before throwing univalence into the mix). The relevant papers are Types are weak $\omega$-groupoids and Weak omega-categories from intensional type theory.
So the notion of space or $\infty$-groupoid was historically not forced upon the axioms but was rather discovered after almost ~30 years of investigation of the theory.

Mike Shulman (May 05 2021 at 20:20):

Leopold Schlicht said:

No, I'm not yet really comfortable with considering either "space" or "$\infty$-groupoid" as primitive notions in a foundational system.

I'm glad you added "yet"! Can you explain your discomfort? I tried to give an explanation of $\infty$-groupoids from a foundational perspective in https://arxiv.org/abs/1601.05035, I don't know if you have looked at that.

But when mathematicians are using the principle "isomorphic structures have the same structural properties" in practice, I think they are not working in the internal language of the category of Kan complexes.

Would you accept that they are working with groupoids, whether or not they make it explicit? A groupoid is, after all, just the formal structure possessed by isomorphisms, so whenever you are working with isomorphisms you are working with groupoids.

And groupoids are a full subcategory of $\infty$-groupoids, so whenever you are working with groupoids you are working with (certain, particularly simple) $\infty$-groupoids. The rest of the $\infty$-groupoids don't impinge on the average mathematician very often, but when they start to say things like "equivalent categories have the same structural properties" then they're implicitly working with 2-groupoids, and so on.

If I remember correctly, Solomon Feferman has written a paper in which he argues that a foundational system shouldn't axiomatize the notion of "category" as a primitive concept (the same argument applies to "$\infty$-groupoid"). I guess this was in reaction to Lawvere's ETCC. The reason is that some notion of a "collection of things" is psychologically necessary to understand the notion of a "category".

This is a philosophical argument that probably isn't going to be settled any time soon. But I believe $\infty$-groupoids can be regarded as a notion of "collection of things", not requiring a prior notion of "collection" to be built out of. The claim is just that whenever we collect a bunch of things together, we always (explicitly or implicitly) also have in mind a "notion of sameness" between them.

Leopold Schlicht (May 06 2021 at 14:23):

Mike Shulman said:

I tried to give an explanation of $\infty$-groupoids from a foundational perspective in https://arxiv.org/abs/1601.05035, I don't know if you have looked at that.

No, I wasn't aware of that paper! Great read, really fantastic, exactly the thing I needed!
Can the

"an $\infty$-groupoid consists of a collection of elements, together with for any two elements $x$, $y$ a collection of ways in which $x = y$, and for any two such ways $f$, $g$ a collection of ways in which $f = g$, and so on, plus operations . . ."

approach be used to give, inside ZFC, a definition of the notion of an $\infty$-groupoid so that the category of these $\infty$-groupoids satisfies HoTT? I would find this more satisfying than a model in Kan complexes, which I think of as very topological things.

FH (May 06 2021 at 14:25):

Maybe take a look at https://ncatlab.org/nlab/show/algebraic+definition+of+higher+categories

John Baez (May 10 2021 at 23:59):

It's the thing you said you'd find "more satisfying":

Can the

"an $\infty$-groupoid consists of a collection of elements, together with for any two elements $x$, $y$ a collection of ways in which $x = y$, and for any two such ways $f$, $g$ a collection of ways in which $f = g$, and so on, plus operations . . ."

approach be used to give, inside ZFC, a definition of the notion of an $\infty$-groupoid so that the category of these $\infty$-groupoids satisfies HoTT? I would find this more satisfying than a model in Kan complexes, which I think of as very topological things.

John Baez (May 11 2021 at 00:01):

That remark you quoted was giving a very sketchy definition of a "globular" $\infty$-groupoid, where the shapes of n-morphism are "globes".

You've got 0-morphisms, or objects $x,y,\dots$, which look like points.

And you've got 1-morphisms like $f: x \to y$, which look like arrows.

And you've got 2-morphisms like $\alpha: f \Rightarrow g$ when $f,g : x \to y$, which look like 2-dimensional discs.

And so on. If you draw the n-morphisms, they look like n-dimensional balls, or "globes".

John Baez (May 11 2021 at 00:03):

There are also simplicial $\infty$-groupoids, called Kan complexes, where the shapes of morphisms are simplexes, but apparently you think simplexes are "very topological" and thus unsatisfying.

John Baez (May 11 2021 at 00:03):

And there are cubical $\infty$-groupoids, where the shapes of n-morphisms are cubes.

John Baez (May 11 2021 at 00:05):

• Wikipedia, Globular set.

This would be a lot better with pictures.

John Baez (May 11 2021 at 00:09):

People have worked a lot on simplicial and cubical models of HoTT, so I asked about work on globular models of HoTT, and people started talking about those...

Leopold Schlicht (May 12 2021 at 14:58):

Ah, thanks! But I don't yet see why the quoted sketchy definition suggests that the shape of n-morphisms is a "globe". In fact, it isn't even talking about "shape" at all, it basically just says that we want to have a collection of n-morphisms, for each n.

Nick Hu (May 12 2021 at 15:15):

The crucial thing is that it only makes sense to have $n$-morphisms between parallel pairs of $n-1$-morphisms. This is called the globularity condition.

Mike Shulman (May 12 2021 at 15:17):

It's the part where the informal description said "for any two such ways $f, g$ a collection of ways in which $f = g$" that starts it off globular. The simplicial version would have instead, as I mentioned earlier, "for any three ways $f,g,h$ in which $x=y$, $y=z$ and $x=z$ respectively, a collection of ways in which $f\cdot g = h$."

John Baez (May 12 2021 at 18:38):

Yup, that's the part.

It may help, @Leopold Schlicht, to note that the usual concept of "natural transformation between functors" is an example of a globular 2-morphism. It only makes sense to talk about a natural transformation between parallel functors, by which I mean functors with the same domain and the same codomain, like $f,g: A \to B$.

(Nick Hu said "parallel" but I'm not sure you know what that means so I wanted to define it.)

John Baez (May 12 2021 at 18:40):

Thus, when we draw a natural transformation it looks like a 2-dimensional globe, meaning this:

John Baez (May 12 2021 at 18:40):

It does not look like a cube, or simplex, etc.

John Baez (May 12 2021 at 18:42):

Natural transformations are 2-morphisms in the 2-category Cat - at least if we take the usual "globular" approach to 2-categories!

John Baez (May 12 2021 at 18:42):

You seem to be more comfortable with the globular approach than the simplicial approach or the cubical approach, except for the fact that you didn't know the word "globular".

James Wood (May 12 2021 at 19:15):

By the way, are there any similarly familiar examples of simplices or cubes at low dimensions? I feel like squares and cubes come up fairly naturally in dependent type theory when you consider equality between diverging telescopes/dependent tuples, but (1) I can't remember how to state this cleanly, and (2) I can't think of an example of simplices. Double category morphisms look a bit like squares, but they're strictly more general IIRC, and all the familiar examples (modules) use that generality.

John Baez (May 12 2021 at 19:45):

Double category morphisms look exactly like squares - indeed, I often call them "squares".

John Baez (May 12 2021 at 19:46):

An easy example of a double category is: take a category, and create a double category where both the vertical and horizontal arrows in the double category are morphism in that category, and the squares are commuting squares.

John Baez (May 12 2021 at 19:47):

One can play the same game with higher-dimensional cubes and get easy examples of n-tuple categories.

John Baez (May 12 2021 at 19:49):

Even the squares in double categories of modules look just like squares: they have four objects, two horizontal arrows, two vertical arrows and a square in the middle.

James Wood (May 12 2021 at 19:54):

Still, the example with commuting squares feels a bit degenerate. There's some basic globular structure (parallel morphisms can be compared for equality), but then you force it to have two extra corners by saying that the two morphisms being compared have to be composites. You could do the same and get any shape you wanted. Modules are a better example of a double category because the square shape isn't artificial. Perhaps the example of modules is related to the example of telescopes/dependent pairs? Modules are naturally dependently typed.

John Baez (May 12 2021 at 19:57):

Still, the example with commuting squares feels a bit degenerate.

Sure! I was merely trying to reassure you that the morphisms in double categories look exactly like squares.

John Baez (May 12 2021 at 19:59):

Also, you asked if there are any "familiar examples of cubes at low dimensions", so I wanted to point out that commuting squares, common in category theory, are a familiar example.

John Baez (May 12 2021 at 19:59):

There's no shortage of more complicated, less degenerate examples.

James Wood (May 12 2021 at 20:00):

Are double categories exactly cubical 2-categories? I thought it was a problem that the horizontal and vertical 1-cells could be different.

John Baez (May 12 2021 at 20:04):

I don't actually know what a "cubical 2-category" is - it's not something I say. I use double categories a lot, and there's a famous kind of double category where the vertical and horizontal 1-cells are the same, and composed the same way. There's some name for that kind....

Mike Shulman (May 12 2021 at 20:05):

"edge-symmetric"?

Mike Shulman (May 12 2021 at 20:10):

James Wood said:

By the way, are there any similarly familiar examples of simplices or cubes at low dimensions?

I'm not sure if this is quite what you're thinking of, but I would say that the commutative square in the definition of a natural transformation is a specific example. Of course, as John said, any commutative square is a square, but I think naturality squares are particularly closely related to the appearance of cubes in type theory. For instance, suppose in type theory you have $f,g:A\to B$, which induce maps ${\rm ap}_f: {\rm Id}_A(x,y) \to {\rm Id}_B(fx,fy)$ and similarly ${\rm ap}_g$. Then suppose you have $p:{\rm Id}_{A\to B}(f,g)$, meaning $p : \prod_{x:A} {\rm Id}_B(fx,gx)$. Then $p$ should induce an identification of ${\rm ap}_f(e)$ with ${\rm ap}_g(e)$, but this has to be a dependent identification since their codomains ${\rm Id}_B(fx,fy)$ and ${\rm Id}_B(gx,gy)$ are different. This sort of doubly-dependent identification is precisely what gives rise to cubes in type theory, and in this case it's clearly also a naturality square for $p$.

Mike Shulman (May 12 2021 at 20:15):

As for simplices, the simplest sort of simplex is a composition relation $g\circ f = h$. Simplices also come up naturally when you talk about (co)descent objects, which are a sort of 2-categorical (co)limit that generalizes (co)equalizers one dimension up and also truncates geometric realization at dimension 2. Descent objects are so-named because they're the natural way to construct categories of descent data when defining stacks, but they also come up when strictifying (co)algebras for 2-(co)monads and when constructing general 2-dimensional (co)limits out of more basic ones.

Nick Hu (May 12 2021 at 20:18):

James Wood said:

Are double categories exactly cubical 2-categories? I thought it was a problem that the horizontal and vertical 1-cells could be different.

I would be comfortable with this description. $n$-fold enrichment in Cat yields globular higher categories, whereas $n$-fold internalisation of a category yields cubical higher categories

John Baez (May 12 2021 at 20:29):

The usual term for an n-fold internal category, though, is not "cubical higher category" but "n-fold category" or "n-tuple category". I think it's best to stick with established terminology here, since the terminology in higher category theory is already confusing enough without making up even more new terms.

James Wood (May 12 2021 at 20:50):

Tying this all back together, I'd expect the HoTT type $\Sigma_{R : \mathrm{Ring}} R\mathrm{-Mod}$ to be a groupoid, but more particularly to naturally form a double groupoid which is like the double category of modules, but with isomorphisms instead of morphisms everywhere.

Mike Shulman (May 12 2021 at 21:17):

If you write down the definition of "category" naively in HoTT, you get a structure that looks sort of "double" because you have the morphisms in your "category" but also the paths in the type of objects. The "univalence" condition on a category (see e.g. Chapter 9 of the Book) collapses this information by making the paths coincide with invertible morphisms. Most naturally-occurring 1-categories are univalent when defined straightforwardly in HoTT, but plenty of naturally-occurring 2-categories aren't -- because even in set theory they're better defined as double categories!

This may be what you're thinking of with modules: if you define the bicategory of rings and bimodules in HoTT, it's not "univalent" because the paths in the type of objects are ring isomorphisms whereas the invertible bimodules are Morita equivalences. Viewed as a double category, this structure consists of the ring isomorphisms and the bimodules. If you want to see the noninvertible ring homomorphisms, of course, you have to define it as a double category inside HoTT.