Hacker News new | past | comments | ask | show | jobs | submit login
Homotopy Type Theory (wikipedia.org)
64 points by yagizdegirmenci 3 months ago | hide | past | favorite | 22 comments



Here is a lecture series on HoTT from CMU. The video recordings are abysmal, but I still find the lectures very interesting because of how the instructor motivates everything.

https://www.youtube.com/watch?v=u92V0OMgvhM&list=PL1-2D_rCQB...


I was lucky to see have had this instructor for a couple of lessons. Bob is a total legend.


Wow, you weren't kidding. I don't know how recently these were recorded but it's to cheap these days to get good video I get really annoyed seeing good material wasted by bad AV


Very good indeed!


A consequence of HOT in relation to programs is that you can compare programs for equality without running them. I rediscovered this a few years ago. It means that e.g. certain physical simulations could be known to not complete without running them to assumed termination. Currently we are wasting millions of dollars running simulations that we could show will not produce valid results.

HOT is an interesting development. You can fit all existing mathematics within it, in addition to mathematics we have not explored, such as systems where you do not accept the axiom of choice or, more interestingly, disregard it entirely.

It is constructive. This is interesting because it means real numbers "do not exist" as you can not write them down. Specific transcendental constants can be written down because you hold them by their relationship to other numbers.

I had hoped to study it and its application to number theory and computation but it is nearly impossible to get back into school.


> A consequence of HOT in relation to programs is that you can compare programs for equality without running them. I rediscovered this a few years ago. It means that e.g. certain physical simulations could be known to not complete without running them to assumed termination. Currently we are wasting millions of dollars running simulations that we could show will not produce valid results.

I'm curious where you got this idea. Even if you express programs in HoTT so that equality of these programs corresponds to (say) identical outputs, there's no reason that this equality should be decidable any more than it is in ordinary mathematics.

You might be confused by the fact that HoTT is (by default) constructive, but just because you can define something in HoTT does not mean that its equality is decidable. In fact, that's a defining property of constructivity in this context: if every type has decidable equality, then the law of excluded middle holds. The proof isn't too hard: simply apply the decidability of equality to the type of propositions and for a given proposition P, check if P = True is true or false.

> systems where you do not accept the axiom of choice or, more interestingly, disregard it entirely.

I'm wondering what the difference between those two is. "not accept" and "disregard" are synonyms to me, but maybe you have something more precise in mind. There's a distinction between not accepting an axiom (so that you're agnostic on the question of whether it holds) and accepting its negation. Maybe that's what you're thinking of.

> it means real numbers "do not exist" as you can not write them down.

In light of your other comment, I'd phrase this as "there are particular real numbers that don't exist" or "some real numbers don't exist". As written, it reads as if the set of real numbers doesn't exist.

Even so, keep in mind the difference between not being able to prove something and being able to prove its negation. HoTT is consistent with adding in more axioms (as you alluded to above) which do imply that Chaitin's constant exists. So that means that the base theory can't prove that such constants don't exist (unless the base theory is inconsistent).


> You can fit all existing mathematics within it...

...

> It is constructive. This is interesting because it means real numbers "do not exist" as you can not write them down.

Didn't you just contradict yourself? If real numbers do not exist within HTT, then you cannot fit all of existing mathematics in HTT.


It's not a contradiction. In the constructive sense, we don't know the real numbers except the ones that can be talked about using concepts that are more intrinsic to our reality such as rational numbers or circles.

You can express the idea that a sequence converges to a limit in constructive mathematics (if not, I'd like to know why) and you can prove that that limit is not rational, nor is it algebraic. That is to say, real analysis works in a constructive setting. At least that's my math-enthusiast understanding of it.

Traditional mathematics even asserts the existence of numbers whose concrete properties we can't even possibly know, such as Chaitin's constant: https://en.wikipedia.org/wiki/Chaitin%27s_constant

My understanding is that these are the kinds of numbers you lose out on when you switch to being a constructivist. I guess you could say that means you can't fit "all of existing mathematics" in it, but to me that feels a bit vacuous.


Well, I guess I think the same about the constructivist position.

> In the constructive sense, we don't know the real numbers except the ones that can be talked about using concepts that are more intrinsic to our reality such as rational numbers or circles.

I accept that as being true.

But then, to say that you can fit "all of existing mathematics" feels like you're saying that you can fit everything that fits, and everything that doesn't fit is defined to not be "real" in some sense. That is, it feels circular - like you're so far down the rabbit hole that you can't remember that there's a world above ground that also exists and has validity.


I guess strictly, it is a contradiction because indeed "all of existing mathematics" cannot be derived purely constructively.

The way I choose to see it, however, is constructivism is the activity of seeing how far you can go with the least possible axiomatic foundation. If, at some point, you need something like the Law of Excluded Middle, you just assert the specific instance that you need as an axiom (and not as a structural rule).

In this sense, then all of mathematics is valid from a constructivist viewpoint, what changes is that now you care about where you assert certain axioms.


You don't lose out on the fields you mentioned when you switch to constructivism. Your assertions become more precise. If anything is lost the mainstream thinking is it was not consistent to begin with.


HoTT describes any infinity-topos. When folks say "all of mathematics can be rederived constructively", they mean that all of constructive mathematics can be described relative to any topos. Classical mathematics is retrieved either by choosing a Boolean topos, or by developing Boolean algebras inside topos theory.

It is a standard theorem that all constructive results are classical, and that all classical results are either constructively true or not-false. A not-false theorem can't be proven true, but it definitely would lead to a contradiction if it were false.

To get a taste of what's constructive, imagine taking a subset of the finite set {0,1}. We construct the subset by enumerating its elements; a computer program might print out elements one-by-one. So, if we start a program and it prints 0, 1, ...; we know that the subset contains all of the elements and we're done. But if we start a program and it prints 0, 0, 0, ...; only printing zeros, then we have to prove that it halts in order to prove that the subset is finite. Constructively, subsets of finite sets aren't necessarily finite.


Strictly speaking, there are a variety of embeddings ("translations") of classical into constructive logic and while different in their minute details, they all share the feature that non-constructive theorems are embedded as negative statements. Conversely, a proof of a negative statement in constructive logic can use proof by contradiction, hence the full power of a "classical" proof. (NOT NOT NOT p) <-> (NOT p) is a theorem in constructive logic, even though (NOT NOT p) -> p isn't.


It is more precise to say you can fit all of existing mathematics that you can actually check.

A number whose only classification is that it is real is a nonphysical entity. In constructive systems it can not be reasoned about because it can not exist. Something very close to real numbers exists, but situationally. Pi exists because I can describe a procedure to construct it, same for Euler's number.


I'm wondering how the absence of Voevodsky affect the research of HoTT related field?



"the development of mathematics within a type-theoretic foundation (including both previously existing mathematics and new mathematics that homotopical types make possible)"

I'm sure Mr Hilbert would approve.

"and the formalization of each of these in computer proof assistants."

Aah, loosely IT related (hence the post) and surely Lean and co can't be far away from the discussion.

"As such, this article may not represent the views of all researchers in the fields equally. This kind of variability is unavoidable when a field is in rapid flux."

The WP article is quite dense for a civilian to get through so I hope something cool is on the horizon.

Is a result on the way or has Lean blue screened?


HoTT is somewhat independent of the choice of proof assistant.

Coq: https://github.com/HoTT/HoTT

Lean: https://github.com/gebner/hott3

idk what you mean by "blue screened", or results being on the way. afaict most of the non-foundational work present (what I assume you mean by "results") in these libraries are basic properties of basic mathematical concepts being rebuilt on HoTT.


cubical Agda : https://github.com/agda/cubical is also worth mentioning int this context


IT? WP?

Lean?


IT = Information Technology

WP = Wikipedia

Lean -> https://leanprover.github.io


Here I think IT more likely means Intuitionistic Type Theory.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: