Comment by p0llard | Hacker News Reader

Comment by p0llard | Hacker News Reader

I'll have to work through this when I get the time.

I started teaching myself Haskell for fun about a year and a half ago, and ended up going down a rabbit hole of formal logic, set theory, mathematical foundations etc. which I did not expect at all; I'm currently spending some time looking at algebraic topology to give me a grounding to go into homotopy type theory.

For anyone else with an interests in this area, I'd strong urge you to look at some of the work from Kevin Buzzard (Imperial College), perhaps better known as an algebraic number theorist, who leads the Xena [1] Project, which started as an attempt to completely formalise all the problem sheets for one of the undergraduate maths modules at Imperial in Lean. There's also a GitHub repo [2] with a lot of work to build on.

Adam Chlipala (MIT) also teaches a course in formal program verification in Coq based on his book [3] which is a valuable resource.

1: https://xenaproject.wordpress.com/

2: https://github.com/kbuzzard/xena

3: http://adam.chlipala.net/frap/

So is homotopic type theory just another way to look at the same thing or is it more expressive than type and set theory? In other words, does homotopic type theory really help theorem checkers/provers?

Yes. Also it includes topology.

Calling it topology can be misleading, as HoTT only considers types as spaces in the sense of homotopy equivalence.

Whether HoTT is a better foundation of mathematics (FOM) in the sense of being easier to use in practise is an open question. It's unclear even exactly what it means to be a better or worse FOM.

Note also that all well-known foundations, including HoTT are mutually relatively consistent, which amounts to being translatable into each other (so if you can derive a contradiction in one, then you can convert that into a contradiction in the other). However that is not so important in practice. Proof automation is most important for large scale reasoning. Indeed the Lean project was started with the explicit aim of bringing better proof automation to provers based on the Curry-Howard correspondence.

Homotopy Type Theory is based on Martin-Lof Type Theory (which is your standard dependent type theory), but reinterprets equality to mean homotopy equivalence. In vanilla MLTT, a = b is inhabited iff a and b share the same normal form, and its proof is refl (reflexivity). In HoTT, a = b may be inhabited by proofs other than refl. Namely, the univalence axiom states that types are equal when they are isomorphic, and function extensionality states that functions are equal when they map the same inputs to the same outputs. You also get higher inductive types, which allow you to define constructors of equalities on inductive types. So, HoTT allows you to prove things that you can't prove under ordinary MLTT.

> So, HoTT allows you to prove things that you can't prove under ordinary MLTT.

Well, adding consistent axioms often allows proving more thing, but that in itself does not necessarily mean it's more useful, and certainly not that proofs are easier -- that, I believe, was the question. For example, adding the axiom 1/0 = 0 is consistent with ordinary arithmetics, and also allows you to prove more things (e.g. that 1/0 = 0), but is not necessarily useful and not necessarily helpful.

Reply on news.ycombinator.com