>>11647423I think it's a good discussion to have.
As a type theoretical frameworks, not only are proofs mathematical objects, so are there expressions (judgements) that aren't propositions (statements that can be false.)
Homotopy Type Theory is all about adopting a groupoid view on equality, as oppose to the extensional e.g. set theoretical one. I.e. isomorphisms vs. nested bags comparisons.
And they discuss and wrestle with the fact that traditionally, in math you don't distinguish between equality and identity. In German: "das gleiche" vs. "das selbe".
>Der iPad, den du gestohlen hast ist der gleiche, den ich vor 2 Wochen gekauft habe.>Der iPad, den du gestohlen hast ist der selbe, den ich vor 2 Wochen gekauft habe.In English I guess that's
>The ipad you stole is the same that I bought 2 weeks ago.and I don't know if you can quickly make the distinction if this situation now means I don't have my iPad anymore or not.
They give the common language example
>In an equilateral triangle, any two sides are equalwhere, in any case, the meaning is not that all sides of a triangle are the the same (in the identity sense) triangle.
The issue comes up in relation to the fact that type theory has definitional judgements of equality b:=a+1 as part of the theory (unlike first and higher order logic, whether definitions are a matter of the meta-theory) and they discuss if they made misleading choices when writing their HoTT book.
Which brings us back to
>>11647427>>11647091given the motivation of Vodovosky for the HoTT program was to come up with mathematical foundations that could be implemented on a computer ... As opposed to set theory, which falls back to model theory, not equating isomorphic structures by design, and which has super-exponential ballast as soon as you discuss anything resembling geometry.
