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: algebraic topology

Topic: HoTT

Nikolaj Kuntner (Jul 25 2020 at 10:01):

I'm not sure if the HoTT book says that all functions are already continuous or whether the associated functoriality property can fail, but in any case: Given that algebraic-topology notions a conventionally always defined using continuous functions (spaces X in terms of which concepts are defined already carry some topology and we define homotopies with continuous functions etc etc), how can I even expect a good chunk of alg. top. to by captured in HoTT?
Naively, one would then assume that even in ZF general alg. top definitions in terms of general functions should be just around the corner. Is the "weaker" (constructive realizations are more likely to be possible) framework enough to be able to just drop the 'continuous' predicate on all involved functions and we can just define all notions for 'just functions'?!

Reid Barton (Jul 25 2020 at 12:39):

There is no notion of "all functions are continuous" and it's independent of the question of constructivity. I would explain it a different way.

Reid Barton (Jul 25 2020 at 12:40):

Namely, in HoTT, types (whatever they are) have this kind of "higher" structure given by something we call "paths" (but are really identity types), paths between paths, etc. These paths are automatically preserved by functions, in the same way that equality between two elements of a set (in ZF say) is automatically preserved by functions.

Reid Barton (Jul 25 2020 at 12:45):

One model/analogy that can give a lot of intuition is to think of a type as a topological space, a function as a continuous map, an equality as a path/homotopy, etc.; the word "continuous" is in there because if it isn't you get something else which isn't what we're interested in.

Reid Barton (Jul 25 2020 at 12:46):

The closest internal statement to continuity would be something like $\Pi \, A \, B \, (f : A \to B) \, a \, a'. \, (a = a') \to (f a = f a')$.

Reid Barton (Jul 25 2020 at 12:48):

Nikolaj Kuntner said:

how can I even expect a good chunk of alg. top. to by captured in HoTT?

maybe the answer is that you shouldn't expect it, but it is true anyways?
How can you expect the same homotopy theory to be describable using either topological spaces or simplicial sets, for instance?

Nikolaj Kuntner (Jul 25 2020 at 12:56):

I got an idea of the setup of HoTT, but the question arises why set theoretical homotopy theory would need topologies, then.

Nikolaj Kuntner (Jul 25 2020 at 12:56):

Reid Barton said:

There is no notion of "all functions are continuous" and it's independent of the question of constructivity. I would explain it a different way.

The HoTT book definately makes such points, although I'm not sure what "continuous" always means in those contexts.

Reid Barton (Jul 25 2020 at 13:00):

In set theory you're starting from a mathematical universe where there isn't any of this funny higher "homotopy" stuff going on, so you have to put some effort in to model it somehow: topological spaces are one of many ways to do this.

Reid Barton (Jul 25 2020 at 13:01):

For me "set" is basically synonymous with "no higher stuff", so I'm probably explaining this poorly.

Nikolaj Kuntner (Jul 25 2020 at 13:12):

Maybe I'm overestimating how easy stuff like CW complex fit into the early HoTT framework. If it works, then I wonder why you can't just require the whole "higher (not point-setty) structure" from your sets X, instead of the 3 topology axioms on T\subset PX and functions continuous w.r.t to T

Reid Barton (Jul 25 2020 at 13:28):

The advantage of the topology axioms is being an actual definition and not just intuition or handwaving.

Reid Barton (Jul 25 2020 at 13:30):

I guess a second advantage is that it gives something you can draw a picture of (especially in low dimensions, e.g., we can represent the circle as literally a subset of $\mathbb{R}^2$ and draw it as a circle on a piece of paper).

Reid Barton (Jul 25 2020 at 13:32):

For intuition or high level reasoning, it's can be perfectly sensible to say a space is basically like a set except it also has the right kind of higher structure that makes it into a space.

Nikolaj Kuntner (Jul 25 2020 at 13:47):

Probably, although the idea that a line is a set of points was always contested.

Nikolaj Kuntner (Jul 25 2020 at 13:50):

https://en.wikipedia.org/wiki/Hermann_Weyl#Foundations_of_mathematics
:)

Reid Barton (Jul 25 2020 at 13:50):

I think the following two claims are indisputable:

• "A topological space is a set together with a collection of open subsets satisfying the following axioms: ..." is a valid definition. (Never mind what the definition might be good for; just that it is a definition of something.)
• "A space is like a set but with higher (not point-setty) structure" is not a valid definition of anything.

Nikolaj Kuntner (Jul 25 2020 at 13:52):

So would you argue that the concept of space isn't yet properly formalized in HoTT?

Reid Barton (Jul 25 2020 at 13:53):

In HoTT a "space" (in the sense I've been using it) is a fundamental undefined notion in the same way that "set" is the fundamental undefined notion of traditional mathematics.

Nikolaj Kuntner (Jul 25 2020 at 13:57):

Ah okay, that's what you meant. Well as soon as there's a hard formalism to it (first-order logic, formation rules) - i.e. as soon as how to move around symbols associated with a topological space are clear - then I'd not call it handwaving. Even if the intuition is fundamentally up for grabs.

Reid Barton (Jul 25 2020 at 13:57):

Traditionally we start from the undefined notion of set and define things like real numbers, groups, manifolds. There are a lot of different ways to define things that behave the way that "spaces" ought to behave, and all of them take a fair amount of work.
In HoTT we take a space as the undefined notion. It's like you redefined the finish line to be the starting line.

Reid Barton (Jul 25 2020 at 13:58):

Of course HoTT can be made into a well-defined formal system; but the game is different. You cannot get the right answer in ZF by just defining a space to be a set.

Nikolaj Kuntner (Jul 25 2020 at 13:59):

Well okay, in any case I still have to understand how something that looks like theorems related to CW complexes follow from the rules of the "higher structures", as opposed to point-topological formalism.

John Baez (Jul 25 2020 at 20:17):

The idea is that homotopy type theory lets you do homotopy "synthetically" - homotopy types and a sufficient collection of operations on them are built into the formalism from the start, so you can do a lot of homotopy theory without messing with explicit models like CW complexes or topological spaces or simplicial sets. But you have to work through the details to see how this actually works. I haven't done much of this myself, but I've seen enough to get the following rough picture:

A bunch of homotopy theory can be done synthetically in HoTT (for example at least up to and including the proof of the Blakers-Massey theorem, which is supposedly more elegant in HoTT), but there's fancier stuff that nobody knows how to do in HoTT, which may require new ideas.

John Baez (Jul 25 2020 at 20:21):

This fancier stuff is not mainly stuff that people would do with CW complexes; it's stuff involving "homotopy coherent diagrams" and the like. You might like to read Lurie's comment on this blog article, and subsequent discussion, to see some experts arguing about the significance and current limitations of homotopy type theory.

Dan Doel (Jul 25 2020 at 21:27):

There seem to be at least a couple camps among the mathematicians studying it, and at least one of them seems to object to the "synthetic" thing. And I guess that is the Voevodsky tradition.

Specifically, people seem to categorize defining "higher inductive types" as doing homotopy theory "synthetically". For instance, you can give inductive definitions of the homotopy types of spheres. But actually none of that is necessary to define a bunch of homotopical notions in type theory, and very few homotopical assumptions are necessary for people to develop a lot of theorems about the defined structure. Basically, you can give a characterization of something and prove theorems about that characterization without assuming the characterized objects can be constructed (synthetically or otherwise).

I can't say the distinction really matters to me, but it does to some people.

Dan Doel (Jul 25 2020 at 21:36):

I suppose as an example of the latter, you can define what it means for a type to be $n$-dimensional, and prove that the type of (small) $n$-dimensional types is $(n+1)$-dimensional in type theory from the 1970s, I think.

Spencer Breiner (Jul 26 2020 at 13:32):

John Baez said:

This fancier stuff is not mainly stuff that people would do with CW complexes; it's stuff involving "homotopy coherent diagrams" and the like. You might like to read Lurie's comment on this blog article, and subsequent discussion, to see some experts arguing about the significance and current limitations of homotopy type theory.

Beautiful quote from the blog comments: "The dream is that the computer assistant will eat the spinach for you. The nightmare is that it will force-feed it to you." -DT

Reid Barton (Jul 26 2020 at 13:50):

We also don't know whether it is possible to define in HoTT many objects of geometric origin, such as the complex cobordism spectrum $MU$, which is absolutely central to the modern understanding of stable homotopy theory.

Reid Barton (Jul 26 2020 at 13:52):

Generally these are objects that come from things like classical Lie groups, and topological spaces really are the easiest way to describe their homotopy types.

Reid Barton (Jul 26 2020 at 14:11):

Note that both of these limitations apply to (our current understanding of) "book HoTT", and there are proposed extensions in which these kinds of constructions are probably possible.

Mike Shulman (Jul 28 2020 at 19:39):

Dan Doel said:

I suppose as an example of the latter, you can define what it means for a type to be $n$-dimensional, and prove that the type of (small) $n$-dimensional types is $(n+1)$-dimensional in type theory from the 1970s, I think.

Not exactly -- in addition to Martin-Lof Type Theory (which I presume is what you mean by "type theory from the 1970s") you need the univalence axiom, which was only formulated about a decade ago. MLTT alone is unable to prove hardly anything about the homotopy type of the universe. But it's true that you don't need HITs for this.

Dan Doel (Jul 28 2020 at 19:47):

Hmm, okay. I didn't trace through the proofs closely enough. So I guess about all you can do is define what it means to be $n$-dimensional.

Dan Doel (Jul 28 2020 at 19:54):

That particularity is kind of irrelevant, anyway, because the actual point is that some people seem to try to see what you can prove with e.g. just univalence, propositional truncation, and hypothetical specifications, rather than extending the type theory with some class of HITs.

Mike Shulman (Jul 29 2020 at 16:37):

Nikolaj Kuntner said:

Well okay, in any case I still have to understand how something that looks like theorems related to CW complexes follow from the rules of the "higher structures", as opposed to point-topological formalism.

Can you give an example of the sort of "theorems related to CW complexes" that you have in mind?

John Baez (Jul 29 2020 at 17:19):

I can make one up if desired, but I should let Nikolaj.

Nikolaj Kuntner (Jul 30 2020 at 14:26):

I'm seeing in front of me balls being glued together on their boundary and when people ask "what are those things being operated on" they would eventually refer back to parametrized blobs that inherit their topology from R^n for some n. If those spaces in a type theory are abstracted further to types with maybe based points or particular boundaries, or maybe characterized by their algebraic-geometry groups (cohomologies etc.), that seems to mean that all the theorems are also abstracter. So it would seem textbook theorems (e.g. about deformation retracts where the standard examples are given in terms of parameters and homotopies where the interval is a genuine [0,1]) spit into abstract and R-parameter ones.

Paolo Capriotti (Jul 30 2020 at 18:11):

I don't know if this is going to answer your question, but one thing to keep in mind is that theorems proved in HoTT will not imply the corresponding results in terms of topological spaces up to homeomorphisms, only up to homotopy equivalence. So if you prove in HoTT that two balls glued by their boundaries give a sphere, you will only get the corresponding statement for topological spaces up to homotopy equivalence.

In fact, it doesn't make that much sense to talk about "balls" in HoTT, because they are contractible, hence indistinguishable from points. Therefore, this result is almost a tautology, because "gluing" two points on an $n$-sphere is (by definition) the suspension of the $n$-sphere, which is (again by definition) the $(n+1)$-sphere.

As for why HoTT works as a language of spaces, it should really not be that surprising (but of course the details are not entirely trivial). Ultimately, there are some operations on spaces that are well-defined up to homotopy equivalence (like say products, loop spaces, suspensions...), and you can abstract them out in terms of a category equipped with some structure. This is an old story: model categories and similar notions are motivated by the same idea. The new aspect of HoTT is the realisation that these structures can be presented nicely using type theory with some minor additions.

Runlei XIAO (Aug 01 2020 at 05:43):

Paolo Capriotti said:

In fact, it doesn't make that much sense to talk about "balls" in HoTT, because they are contractible, hence indistinguishable from points. Therefore, this result is almost a tautology, because "gluing" two points on an $n$-sphere is (by definition) the suspension of the $n$-sphere, which is (again by definition) the $(n+1)$-sphere.

I do not know why is " on an $n$-sphere ", where is $n$-sphere come from?

Paolo Capriotti (Aug 01 2020 at 08:36):

The sphere is the boundary of the two balls, which we realise as just points. Gluing means taking the pushout $1 \leftarrow S^n \to 1$.

Runlei XIAO (Aug 01 2020 at 12:53):

So because we glued boundary of ball, so it do not contract?

Valery Isaev (Aug 01 2020 at 18:06):

It's not that simple. You can glue cells in various ways and it's not that easy to show that you get equivalent spaces. For example, you can just attach one 2-cell to a point or glue two 2-cells or three, or whatver number you want in different ways. It's nuch easier with topological spaces.

Mike Shulman (Aug 02 2020 at 01:31):

You might have an easier time understanding HoTT if you forget anything you ever heard about it being related to "topology" and instead think about types being $\infty$-groupoids. That's really the proper intuition; the relationship to topological spaces is only by way of how spaces can be used to present $\infty$-groupoids.

Henry Story (Sep 15 2020 at 19:06):

I had a few questions about Modal HoTT. It may seem a bit odd as I am only a little familiar with HoTT. This comes from having a background in Modal Logic (Kripke, David Lewis) and so recognizing modalities quite quickly. I read @David Corfield's book Modal HoTT which is more a philosophical introduction to the area and a few talks on it such as @Mike Shulman's Type 2 Theories slides. I keep getting redirected there by David.

So more surprising is I am coming from a practical application of the Semantic Web, which I believe has a modal aspect. It is quite obvious that it has using it (if one knowns modal logics), and my aim is to find out how to make this clear. So of course being able to bring in the latest research would be helpful. Also the semantic web came from work on "Contexts: A Formalization and Some Applications" by Guha (now at Google), and a number of papers have been written on contexts from various perspectives (Context Mereology by Pat Hayes, Context Representation for the Semantic Web in terms of Insitutions)

Henry Story (Sep 15 2020 at 19:27):

The basic structure of RDF is $s,p,o: A \to N$ which allows one to express 2-graphs, and explains why reasoning happens in 2 categories as shown by @Evan Patterson in bicategories of relations. But really in order to speak of where graphs come from on the web (who said what, when?, how?) one needs $s,p,o,g: A \to N$. The $g$ acts as an index.
Hence for example the relevance of Index Monads in the saying_that logic of Abadi, used for security reasoning Access Control in a Core Calculus of Dependency.
Knowing who said what is essential on the web, since as we all know, everyone can saying anything, and the quality is not always good (British understatement).

Henry Story (Sep 15 2020 at 19:35):

I am probably not going to need a lot of modal HoTT (perhaps even simple HoTT will do). But I was wondering if from those that know there is a minimal part of it that should cover what is needed?

Say we wanted to take "Bicategories of Relations" and index it not perhaps by speaker, but by statement events, which could then be tied to speakers/publishers allowing one to then build more complex logics on top. I am thinking here that Philosophers such as Robert Brandom start with the basic notion of "saying that" as a speech act on which they then build meaning. But we also find that logicians like Per Martin-Lof see speech acts as central to constructive logic.

I just came across a paper Indexed Type Theories by the folks from IntelliJ working on the cubical HoTT proof assistant Arend. Is that the same notion of indexed? It seems to index contexts...

Henry Story (Sep 16 2020 at 05:11):

Henry Story said:

I just came across a paper Indexed Type Theories by the folks from IntelliJ working on the cubical HoTT proof assistant Arend. Is that the same notion of indexed?

David answered on Twitter https://twitter.com/DavidCorfield8/status/1305979965373132803
(The most unlikely place for mathematical discussions)

@bblfish @intellijidea @ArendLang Certainly related. That's looking at syntactic representations of indexed (∞,1)-categories, so a kind of fibration (https://ncatlab.org/nlab/show/Cartesian+fibration). Mike et al are looking at things like 2-bifibrations (https://ncatlab.org/nlab/show/bifibration#bifibration_of_bicategories).

- David Corfield (@DavidCorfield8)

Valeria de Paiva (Sep 18 2020 at 05:04):

Henry Story said:

The basic structure of RDF is $s,p,o: A \to N$ which allows one to express 2-graphs, and explains why reasoning happens in 2 categories as shown by Evan Patterson in bicategories of relations. But really in order to speak of where graphs come from on the web (who said what, when?, how?) one needs $s,p,o,g: A \to N$. The $g$ acts as an index.
Hence for example the relevance of Index Monads in the saying_that logic of Abadi, used for security reasoning Access Control in a Core Calculus of Dependency.
Knowing who said what is essential on the web, since as we all know, everyone can saying anything, and the quality is not always good (British understatement).

hi @Henry Story I think you don't need HoTT for this kind of modality of the style (principal) "P says_that" SOMETHING. I think simply lax logic (Fairtlough and Mendler) does it for you easily (I have some slides in https://www.slideshare.net/valeria.depaiva/constructive-access-control about it. But they were from before Deepak Garg did his work on that and I expect he did get all the low hanging fruit there. So yes, the categorical modelling uses monads, one for each principal and CCCs for the statements that the principals make. the level is not as sophisticated as HoTT and univalence stuff, but I thought it was plenty sophisticated enough for applications--but maybe I misremember.

Henry Story (Sep 18 2020 at 07:42):

Thanks for the pointer. In my second year report from a year and a half ago I described how Abadi's logic based on Indexed Monads seemed like the right fit, and my next todo was to tie this in with access control for Tim Berners-Lee's Solid project and OWL reasoning adapted to a Guard (So I am happy to see you confirm that I was in going in the right direction).

Henry Story (Sep 18 2020 at 08:09):

What I am currently looking to do is to get from first principles a way to show the continuity between $s,p: A \to N$ graphs, $s,p,o: A \to N$ 2-graphs, $s,p,o,g: A \to N$ (hyper-graphs?) to lax logic, in such a way that people with no Category Theory experience can follow the reasoning and so that Category Theorists can understand the semantic Web (I am looking to HoTT and Modal HoTT as guides).

Henry Story (Sep 18 2020 at 08:21):

There is this question that you bring up in your slides of constructive logic being perhaps more apt for security reasoning (RDF has a first order interpretation). James Trafford argues in Meaning in Dialogue that first order logic can be seen as specific coming together of constructive and co-contructive logics, so perhaps that is something that would help here: Someone wanting access to a resource constructs a proof, and the guard tries to disprove it? Perhaps RDF can be seen to be such a coming together of a constructive and co-constructive logic? And it would be useful to split that into two for security reasoning. I wonder what Pat Hayes would make of that ;-)

In your last slides you mention linear logic, temporal logic, etc... and perhaps this is where Modal HoTT can have a clarifying role, in that I think it may show how all these can be seen from the same framework. (But it may also take me too long to fully understand)

Valeria de Paiva (Sep 18 2020 at 13:51):

ok, glad to hear that Lax Logic was already part of the plan!

Henry Story (Sep 18 2020 at 14:38):

Indexed Lax Logic is very intriguing as it maps directly to indexed strong monads, for which there are simple libraries in Scala, and it seems to get to the quad structure I described above.