A syntax for cubical type theory (draft)

In this paper we provide a syntax for the cubical set model of type theory [3]. We start by defining a heterogeneous equality as a logical relation in an extended context (section 1.1). This can be seen as a different presentation of parametricity for dependent types [1]. We investigate the higher dimensional structure induced by the logical relation in section 1.2. The relation defined so far is a very weak equality which is not even reflexive, so as a first step, we add reflexivity (section 1.3). This can be seen as a different presentation of the in-ternalisation of parametricity [2]. To add symmetry and transitivity of equality, and in general, to prove the J eliminator, we modify our theory in one more step by adding Kan fillers to the universe (1.4). This makes our construction an internalisation of the presheaf model given by cubical sets (section 2). Finally we prove some metatheoretic properties of the system 3. The parts which are missing: • We haven’t yet defined uncoe and uncoh for each type former, see end of section 1.4.1. • It is not clear how to swap the universe with the new definition of U∗, see section 1.4.5. • All the numbered equations should be proven in section 3. • Prove decidability of definitional equality, canonicity