Homotopy Type Theory (2012) [pdf]

Re:Homotopy Type Theory (2012) [pdf] by boyobo on Tuesday October 27, 2020 @05:20PM (#24912060)

That's a flawed analogy. Mathematicians do use 'higher level languages', that's precisely why most of them don't care about HoTT vs set theory. Just like a web dev usually does not care about the instruction set of the processor.

[ Parent | on HN ]

Re:Homotopy Type Theory (2012) [pdf] by voxl on Tuesday October 27, 2020 @05:54PM (#24912393)

Its not flawed because the correct analogy is: pen and paper Turing machines versus Python.

[ Parent | on HN ]

Re:Homotopy Type Theory (2012) [pdf] by boyobo on Tuesday October 27, 2020 @09:47PM (#24914140)

Now I'm not sure what your point is. Are you suggesting that HoTT is to python as ZFC is to turing machine tape?

[ Parent | on HN ]

Re:Homotopy Type Theory (2012) [pdf] by zrkrlc on Wednesday October 28, 2020 @05:08AM (#24916745)

Nitpick, but I think what you meant to say what "HoTT is to ZFC as Python is to Turing machine tape". Hope it helps.

[ Parent | on HN ]