8 ms·

Homotopy Type Theory

gerdesj 5y ago
"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?
- nixpulvis 5y ago
  IT? WP? Lean?
  - semigroupoid 5y ago
    IT = Information Technology WP = Wikipedia Lean -> https://leanprover.github.io https://leanprover.github.io
    - darzu 5y ago
      Here I think IT more likely means Intuitionistic Type Theory.
- jhanschoo 5y ago
  HoTT is somewhat independent of the choice of proof assistant. Coq: https://github.com/HoTT/HoTT https://github.com/HoTT/HoTT Lean: https://github.com/gebner/hott3 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.
  - m_j_g 5y ago
    cubical Agda : https://github.com/agda/cubical https://github.com/agda/cubical is also worth mentioning int this context
R0b0t1 5y ago
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.
- AnimalMuppet 5y ago
  > 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.
  - skulk 5y ago
    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 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.
skulk 5y ago
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_rCQBarjdqnM21sOsx09CtFSVO6Z https://www.youtube.com/watch?v=u92V0OMgvhM&list=PL1-2D_rCQB...
- fezzez 5y ago
  I was lucky to see have had this instructor for a couple of lessons. Bob is a total legend.
- mhh__ 5y ago
  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
- abss 5y ago
  Very good indeed!
doall 5y ago
I'm wondering how the absence of Voevodsky affect the research of HoTT related field?
Koshkin 5y ago
Here's the shortest intro I know of: https://math.uchicago.edu/~may/REU2015/REUPapers/Macor.pdf https://math.uchicago.edu/~may/REU2015/REUPapers/Macor.pdf

"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?

nixpulvis 5y ago
IT? WP? Lean?
- semigroupoid 5y ago
  IT = Information Technology WP = Wikipedia Lean -> https://leanprover.github.io https://leanprover.github.io
  - darzu 5y ago
    Here I think IT more likely means Intuitionistic Type Theory.
jhanschoo 5y ago
HoTT is somewhat independent of the choice of proof assistant. Coq: https://github.com/HoTT/HoTT https://github.com/HoTT/HoTT Lean: https://github.com/gebner/hott3 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.
- m_j_g 5y ago
  cubical Agda : https://github.com/agda/cubical https://github.com/agda/cubical is also worth mentioning int this context

R0b0t1 5y ago

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.

AnimalMuppet 5y ago
> 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.
- skulk 5y ago
  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 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.

skulk 5y ago

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_rCQBarjdqnM21sOsx09CtFSVO6Z https://www.youtube.com/watch?v=u92V0OMgvhM&list=PL1-2D_rCQB...

fezzez 5y ago
I was lucky to see have had this instructor for a couple of lessons. Bob is a total legend.
mhh__ 5y ago
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
abss 5y ago
Very good indeed!

doall 5y ago

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

Koshkin 5y ago

Here's the shortest intro I know of: https://math.uchicago.edu/~may/REU2015/REUPapers/Macor.pdf https://math.uchicago.edu/~may/REU2015/REUPapers/Macor.pdf