[FOM] A Meaning Explanation for HoTT

[Dimitris Tsementzis]

Hello,

A while ago, in response to an ongoing public discussion on HoTT and Univalent Foundations, I began (but did not finish, due to certain constraints) a sketch of an intuitive justification of the rules of HoTT. This idea that I sketched back then is now available under the title “A Meaning Explanation for HoTT” at the following location:

http://philsci-archive.pitt.edu/id/eprint/12824 <http://philsci-archive.pitt.edu/id/eprint/12824>

Let me summarize the contents of the paper, by way of completing the thread began last year. A meaning explanation for a formal system as I understand it is the process where (i) you give meaning to the syntax of the system and (ii) you justify the rules of the system based on the meaning given in (i). There are pre-formal and formal meaning explanations. A formal meaning explanation gives a formal meaning to the syntax, through an interpretation into another formal system. A pre-formal meaning explanation gives a pre-formal meaning of the syntax of the system, relying on primitive notions comprehensible to the human mind. A pre-formal meaning explanation for ZFC, for example, is given by Boolos [1]. A formal meaning explanation of HoTT is given in [2] using the category of simplicial sets. What I try to do in this paper is give a pre-formal meaning explanation to HoTT. It goes as follows:

(i) Meaning of Syntax: There are four basic syntactic entities in MLTT, the so-called four forms of judgement. They are given meaning as follows:

a : A		 —>		“a is a point on the shape A”
A Type      —>   	“A is a shape”
a=a’ : A     —>		“a and a’ are equal points on A”
A=A Type  —>		“A and A’ are equal shapes”

There are therefore three main notions: “shape”, “point”, “equality”. By “equality” (which in the paper I call “symmetry”) we understand the usual strict notion of equality between entities. By “shape” we understand a spatial entity composed of points and paths between points satisfying a list of properties that are listed in the paper (and which are phrased in terms of a few more primitive notions, e.g. “contractibility”, “void” etc.) Overall, the “judgments” of MLTT are now understood as “observations” so that where in MLTT we would say  “We judge that a is proof of the proposition A” now we say “We observe that a is a point on A”.

(ii) Justification of Rules: Given the above meaning, the rules are justified by basic spatial intuition, subject to the constraints of the listed properties of the particular notion of shape. Namely, we use spatial intuition to argue that if certain observations have already been made, then certain more observations can be made. For example, if we can observe points a and b on a shape A, then we can also observe a shape of paths between a and b (Id-Formation); if we can observe from any point x of a shape A a portion B(x) of another shape B then we can observe the shape formed by attaching to each point x the portion B(x) observable from it (Sigma-Formation). Etc. 

I conclude by discussing objections and limitations. One key objection, of course, is whether the notion of a “shape” is primitive enough to be called “intuitive”. Another consideration is whether there could be alternative formal systems that formalize UF that could receive a pre-formal meaning explanation, e.g. Cubical Type Theory [3]. Another objection is whether the talk of “maps” and “one-to-one correspondences” that I employ depends on set-theoretic intuition. Finally, one could also imagine carrying out a pre-formal meaning explanation in a different way, e.g. instead of “shape” and “path” we could have primitive notions of “structure” and “isomorphism”, perhaps in terms of a “first-order logic with isomorphism”. For example, this could be done in terms of the system I have outlined in [4] but it would first require a “first-order” axiomatization of UF which does not yet exist (but which is certainly conceivable).

Best,

Dimitris

REFERENCES

[1] Boolos, “The Iterative Conception of Set” https://philpapers.org/rec/BOOTIC <https://philpapers.org/rec/BOOTIC> 
[2] Kapulkin and Lumsdaine, “ The Simplicial Model of Univalent Foundations (after Voevodsky)” https://arxiv.org/abs/1211.2851 <https://arxiv.org/abs/1211.2851>
[3] Cohen, Coquand, Huber, Mörtberg, “Cubical Type Theory” https://www.math.ias.edu/~amortberg/papers/cubicaltt.pdf <https://www.math.ias.edu/~amortberg/papers/cubicaltt.pdf>
[4] Tsementzis, “Homotopy Model Theory I: Syntax and Semantics” https://arxiv.org/abs/1603.03092 <https://arxiv.org/abs/1603.03092>











-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20170216/baaeaf36/attachment.html>