A General Syntax for Nonrecursive Higher Inductive Types?

Abstract

Higher Inductive Types are one of the most interesting features of HoTT, as they let us de ne geometrical objects into the theory. However, unlike inductive types, there is not yet a general schema telling us what exacly an HIT is, or what its corresponding rules in the calculus are. In fact, HITs are often given via \ad hoc" de nitions, as in [7, 8]. In this paper we propose a general syntax schema that encapsulates a broad family of nonrecursive HITs. We generalize the concepts of transport and dependent application to higher paths, which we use to give a procedure to extract the elimination rule and the related computation rules.

Keywords

• Homotopy Type Theory Higher Inductive Types

Introduction

A Higher Inductive Type on HoTT is de ned by giving constructors not only for points (level 0 constructors), but also for (higher) paths in the type (higher level constructors). Many examples of HITs can be found in the current literature [ 8 ], however, given the constructors, there is no general rule telling us what the associated induction principle should be. Indeed one might wonder why the torus in [ 7 ] has the described induction principle, and why it is sensible. In general how to obtain the induction principle of a HIT with level 3 constructors is still a craft. The reason why these questions are hard to address at this moment is that we do not have a formal description of what an HIT is and what its corresponding induction principle should be.

HITs have been formalized in Cubical Type Theory (for example [ 2, 3 ]), but our goal is to formalize them inside HoTT so to study its proof theory. Some work towards a syntactic formulation of HITs in HoTT has been done, for example [ 6, 5 ]; these approaches involve either categorical models of the theory or some other external type theory. It is clear that using these tools brings out of the syntax of HoTT, which prevents the use of the existing knowledge of the related proof theory. In this work we propose, at least in the nonrecursive case, a more direct approach, which is similar to the one used in [ 4 ], but extends to higher ? Copyright c 2020 for this paper by its authors. Use permitted under Creative

Commons License Attribution 4.0 International (CC BY 4.0). level constructors and accounts for propositional computation rules, with the aim of extending the proof techniques used in [ 1 ] to HoTT with HITs.

These questions seem to be solved in the case of HITs with only level 0 and level 1 constructors. The idea is that constructors of a HIT T de ne its structure, and to eliminate we have to recognize the same structure in some bration C : T ! U . In the case of 0 and 1-HITs, this is done by looking for \points" in the appropriate bers, and for \paths" in path spaces that \lie over" the appropriate paths in the type T . For example, to perform S1 induction on C : S1 ! U : { we need a \proof" for base : S1, which is a point cb : C(base). { we need a \proof" for loop : base =S1 base, which is a path that \lies over" loop whose endpoints are the proofs of base. Following the notation of [ 8 ], this is a \pathover" cl : cb =lCoop cb.

Recall from [ 8 ] that the type of the pathover above abbreviates trspC (loop; cb) = cb. This notion is exactly the counterpart to paths in the bration C we want to perform induction on. We will generalize this idea to get a reasonable concept of \higher pathover".

Suppose we have a HIT T that has the same constructors as S1 and an additional level 2 constructor h : loop = loop. The induction principle would require now an additional \proof" corresponding to h, that is a \2-pathover" between the proof for the starting point of h and the proof of its endpoint. Mimicking the notation for 1-pathovers, we could write this as ch : cl =2h;C cl. This suggests that a 2-pathover space cl =2;C cl should be an abbreviation for h trsp2C (h; cl) = cl, where trsp2C is some \higher transport along a 2-path" function to be de ned. This further suggests that if we were to de ne a general n-transport function, its \natural" argument, besides the n-path, would be a (n 1)-pathover.

Once we generalize pathovers, we illustrate how to extract the induction principle of a HIT from the constructors. The computation rules associated turn out to be slightly trickier, as equalities at higher levels are only propositional. However, there are some canonical equivalences to solve this problem. 2

Preliminary de nitions

We will adopt the notation used in [ 8 ]. For the rest of the section, let A : U . When dealing with paths at level n we have to give two 0-paths x; y : A, two 1-paths in x = y, and so on until we get to two (n 1)-paths ; and nally a n-path in = . We will generally omit most of the declarations, and denote by p; q (n 2)-paths, by ; (n 1)-paths, and by ; n-paths.

Let C : A ! U . Recall the de nition of trsp : Qx;y:A Qp:x=y C(x) ! C(y) given in [ 8 ] of the \transport function along a 1-path". It is given by path induction on p, stating that trspC (x; x; re x) idC (x). When using trsp, in the sequence of arguments we usually only write the path p, leaving the endpoints x; y to be inferred. From this, we de ne the type of pathovers over p with endopints u : C(x) and v : C(y) as (u =pC v) : (trspC (p; u) = v).

We want to generalize these two notions to higher paths. The idea is that level n transport takes as input an n-path : = , an (n 1)-pathover that lies over and outputs a (n 1)-pathover lying over .

De nition 1. Let n > 1. Given an n-path : = and a (n 1)-pathover c : cp =n 1;C cq lying over , we de ne the higher transport function by trspnC ( ; c ) : trsp :(p=q):cp=n 1;Ccq ( ; c ).

Notice again that we left most of the sequence of arguments implicit, as it can be inferred by the last terms. Similarly: De nition 2. For n 1, we de ne the type of n-pathovers over : = with endpoints c : cp =n 1;C cq and c : cp =n 1;C cq as the following abbreviation: (c =n;C c ) : (trspnC ( ; c ) = c ).

This is a de nition by mutual induction on n : N: in fact n-pathovers are de ned in terms of trspnC , and trspnC is de ned in terms of (n 1)-pathovers. To have a well founded de nition, we state that trsp1C is the usual trspC and the type of 0-pathovers lying over x : A is simply C(x).

It is possible to de ne (by path induction) pathover operations corresponding to the usual operations on paths. If ; are n-paths that can be concatenated, g : u =n;C v and h : v =n;C w are n-pathovers over and respectively, then we can concatenate them to get a pathover g h : u =n;C w. Similarly we can invert g to get a pathover g 1 : v =gn;C1 u. We use di erent symbols to distinguish these operations from the usual on paths. 3

Rules for a general nonrecursive higher inductive type

In this section we describe the inference rules to de ne a general nonrecursive HIT T . The rules will mimic the style of [ 1 ], so most of the rules will be introduce a constant in the calculus, so that they are easier to handle when tackling proof theoretic results.

Formation rule The the type T we are de ning may have formation parameters of type F1; : : : ; Fw, to allow for parametric types like suspensions (section 6.5 of [ 8 ]). The formation rule for a HIT T introduces a constant T : Q(f:F )w Ui, were Q(f:F )w abbreviates Q(f1:F1) Q(f2:F2) : : : Q(fw:Fw). This sequence can possibly be empty. Similar abbreviations will be used in the rest of the paper. Introduction rules Introduction rules are given by a list of constructors. We allow each constructor to only refer to previous ones. If the i-th constructor Ki is a level n constructor, its introduction rule is a rule introducing the constant Ki : Q(f:F )0w Q(x:R)l Hi, where Hi is some n-path space in T f 0 (de ned below) and each Rk is a type not involving T in any way.

(f : F )0w may be a subsequence of (f : F )w, as in the constructor re for the type =. Also, f 0 is a sequence of formation parameters taken from (f : F )0w (hence, with possibly duplicates).

If n 1, an n-path space in T f 0 is a type of the form

Pi1i1

Piaia = Pj1j1

Pjbjb where each of the Pw is Kh(th), with Kh some previous level (n 1) constructor. w can be ( 1) denoting path inversion, or nothing. If n is 1, then we have no concatenation operator for 0-paths (i.e. points), hence, both a and b are equal to 1. If a (resp b) is 0, then the path on the left- (resp. right-)handside is an appropriate re exivity path. If n = 0 the only path space is T f 0 istelf. In other words, only re exivities and suitably instantiated previous constructors can appear in the output type of a constructor. of (Ki(f^0; x) : Hi), de ned as: Elimination rule The elimination rule states the existence of an inductor (again via a constant introduction rule). The idea is that the inductor recieves as input the \proofs" (induction methods) of some property C : Q(f:F )w T f ! U on the constructors of T . More precisely, for each constructor Ki : Q(f:F )0w Q(x:R)l Hi we have to provide a term ci : Q(f:F )0w Q(x:R)l Hi where Hi is the lifted path space { if Hi is a level n 1 path space Pi1i1 Piaia = Pj1j1 Pjbjb , then Hi is Pi"1i1 Pi"aia =nK;iC(f^f00x) Pj"1j1 Pj"bjb , where if Pw is Kh(th), then Pw is ch(th). In other words, constructors are replaced by their induction methods. Moreover, " is 1 whenever is 1. If either the LHS or the RHS in H are re r for some (n 1)-path r, then this gets lifted to re r0 , where r0 is r with the constructors replaced by their induction methods again. { if Hi is a level 0 path space (i.e. Ki is a point constructor), then Hi is

C(f 0; Ki(f^0x)) Above, f^0 denotes the sequence of formation parameters of Ki. Note that the induction method for Ki can depend on any of the preceding induction methods. In conclusion, the elimination rule introduces the following constant in the calculus: indT : Y

Y

Y

Y C(f ; x) (f:F )w (C:Q(f:F)w T f!U) (ci:Q(f:F)0w Q(x:R)l Hi)i=1 (x:T f) Computation rule It is possible to generalize the notion of apd in [ 8 ] to higher paths: if : = is an n-path and g : Qx:A C(x) is a dependent map, then apdgn( ) : apdgn 1( ) =n;C apdgn 1( ) is de ned by path induction on .

For the rest of the section let g : indT (f ; C; c1; : : : ; c ) : Qx:T f C(f ; x). Let us now consider constructor Ki : Q(f:F )0w Q(x:R)l Hi at level n. { if n = 0 we get the usual judgmental computation rule, as in [ 1 ]. { if n = 1 we have a rule introducing a constant

Ci :

Y

Y apdg1(Ki(f^0; x)) = ci(f^0; x) (f:F )0w (x:R)l { if n > 1 we would like to give the same rule, however the equality does not typecheck: in fact, if Hi is Pi1i1 Piaia = Pj1j1 Pjbjb we have apdgn(Ki(f 0; x)) : apdgn 1(Pi1i1

"i1 ci(f 0; x) : Pi1

Piaia ) =n;Cf0

Ki(f^0;x) "ia =n;Cf0 "j1 Pia Ki(f^0;x) Pj1 apdgn 1(Pj1j1

Pjbjb )

"jb Pjb

These types are not judgmentally equal. However, thanks to the computation rules of the previous constructors, it is possible to prove: Theorem 1. In the setting above, we have

Ki(f^0;x) : apdgn 1(Pi1i1

Piaia ) =n;Cf0

Ki(f^0;x) "i1 Pi1 apdgn 1(Pj1j1

Pjbjb )

"ia =n;Cf0 "j1 Pia Ki(f^0;x) Pj1 '

"jb Pjb Moreover, this equivalence does not depend on the particular path Ki(f^0; x). Thanks to this equivalence, we can now write the computation rule for constructors of level greater than 1 as a rule introducing the constant

Ci :

Y

Y (f:F )0w (x:R)l

Ki(f^0;x) apdgn(Ki(f^0; x)) = ci(f^0; x) 4

An example: the torus

Consider the torus T 2 as de ned in [ 8 ], which is a HIT without any formation parameter with the following constructors: { A 0-constructor b : T 2 { Two 1-constructors: (p : b = b) and (q : b = b) { A 2-constructor (surf : p q = q p) Given C : T 2 ! U , the corresponding induction methods for the eliminator are: { A 0-pathover cb : C(b) { Two 1-pathovers: (cp : cb =1p;C cb), and (cq : cb =q1;C cb) { A 2-pathover (csurf : cp cq =s2u;Crf cq cp)

In practice, what happens is that the paths given by the constructors are replaced by their induction method in the eliminator. Note how this elimination principle better re ects the intuition of recognizing the structure of T 2 in the bration C when compared to the one used in [ 7 ]. This is because the latter one states explicitly every transport involved, while our schema hides them behind the scene. It can be proven that in fact the two induction principles are equivalent.

As for the computation rules, let g : indT 2 (C; cb; cp; cq; csurf ) : Qx:T 2 C(x). (Cq : apdg1(q) = cq). { At level 0 we have as usual the judgmental equality (g(b) cb). { At level 1 we have two propositional equalities: (Cp : apdg1(p) = cp) and { At level 2 let surf : apdg1(p q) =s2u;Crf apdg1(q p) ' cp cq =s2u;Crf cq cp be the equivalence given by theorem 1, which maps to the following path: There is an hidden application of trsp2C (surf) on the paths on the left to make everything typecheck. So the computation rule for surf states that there is a propositional equality Csurf : surf (apdg2(surf)) = csurf , that amounts to the commutativity of a square as in [ 7 ]. 5 In this paper we have proposed a syntax for a broad class of HITs. This allows us in the rst place to tackle some proof theoretic questions about HoTT with HITs: for example, it should be easy to prove normalization of the calculus (meaning that every reduction sequence of a judgment terminates) by extending the proof in [ 1 ]. Moreover it is also possible to use the elimination principle proposed here to prove in the theory some properties we would expect, such as the contractibility of the k-dimensional disk.

Moreover, it seems possible to extend the eliminator to HITs with recursive constructors, so to include e.g. truncations, which we are currently working on. Dealing with computation rules is harder in the recursive case.

References

1. Bonacina , R.: Semantics for Homotopy Type Theory . Ph.D. thesis, Universita degli Studi dell'Insubria ( 2019 )

2. Cavallo , E. , Harper , R.: Higher inductive types in cubical computational type theory . Proceedings of the ACM on Programming Languages 3(POPL) , 1 { 27 ( 2019 )

3. Coquand , T. , Huber , S. , Mortberg, A.: On higher inductive types in cubical type theory . In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science . pp. 255 { 264 ( 2018 )

4. Dybjer , P. , Moeneclaey , H.: Finitary higher inductive types in the groupoid model . Electronic Notes in Theoretical Computer Science 336 , 119 { 134 ( 2018 )

5. Kaposi , A. , Kovacs , A. : Signatures and induction principles for higher inductiveinductive types . arXiv preprint arXiv: 1902 . 00297 ( 2019 )

6. Lumsdaine , P.L. , Shulman , M. : Semantics of higher inductive types . In: Mathematical Proceedings of the Cambridge Philosophical Society . pp. 1 { 50 . Cambridge University Press ( 2019 )

7. Sojakova , K. : The equivalence of the torus and the product of two circles in homotopy type theory . ACM Transactions on Computational Logic 17 ( 4 ), 1 { 19 ( 2016 )

8. The Univalent Foundations Program: Homotopy Type Theory: Univalent Foundations of Mathematics . https://homotopytypetheory.org/book, Institute for Advanced Study ( 2013 )