=Paper=
{{Paper
|id=Vol-2756/paper26
|storemode=property
|title=A General Syntax for Nonrecursive Higher Inductive Types
|pdfUrl=https://ceur-ws.org/Vol-2756/paper_26.pdf
|volume=Vol-2756
|authors=Marco Girardi,Roberto Zunino,Marco Benini
|dblpUrl=https://dblp.org/rec/conf/ictcs/GirardiZB20
}}
==A General Syntax for Nonrecursive Higher Inductive Types==
https://ceur-ws.org/Vol-2756/paper_26.pdf
A General Syntax for Nonrecursive Higher
Inductive Types?
Marco Girardi1 Roberto Zunino1 and Marco Benini2
1
University of Trento, Italy
2
University of Insubria, Italy
Abstract. Higher Inductive Types are one of the most interesting fea-
tures of HoTT, as they let us define 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” definitions, 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.
1 Introduction
A Higher Inductive Type on HoTT is defined 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).
2 M. Girardi et al.
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 define its
structure, and to eliminate we have to recognize the same structure in some
fibration C : T → U. In the case of 0 and 1-HITs, this is done by looking for
“points” in the appropriate fibers, 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 =C
loop 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 fibration 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 =2,C h cl .
This suggests that a 2-pathover space cl =2,C h c l should be an abbreviation for
trspC C
2 (h, cl ) = cl , where trsp2 is some “higher transport along a 2-path” function
to be defined. This further suggests that if we were to define 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 definitions
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 finally 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 χ, Q ξ n-paths.
Q
Let C : A → U. Recall the definition of trsp : x,y:A p: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, reflx ) ≡ 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 define the type of pathovers over p with endopints
u : C(x) and v : C(y) as (u =C C
p v) :≡ (trsp (p, u) = v).
A General Syntax for Nonrecursive Higher Inductive Types 3
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 β.
Definition 1. Let n > 1. Given an n-path χ : α = β and a (n − 1)-pathover
cα : cp =n−1,C
α cq lying over α, we define the higher transport function by
n−1,C
trspn (χ, cα ) :≡ trspλγ:(p=q).cp =γ
C cq
(χ, cα ).
Notice again that we left most of the sequence of arguments implicit, as it can
be inferred by the last terms. Similarly:
Definition 2. For n ≥ 1, we define 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:
n,C C
(cα =χ cβ ) :≡ (trspn (χ, cα ) = cβ ).
This is a definition by mutual induction on n : N: in fact n-pathovers are defined
in terms of trspC C
n , and trspn is defined in terms of (n − 1)-pathovers. To have a
well founded definition, we state that trspC C
1 is the usual trsp and the type of
0-pathovers lying over x : A is simply C(x).
It is possible to define (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
−1 n,C
g to get a pathover g : v =g−1 u. We use different 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 define 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 defining may have formation parameters
of type F1 , . . . , Fw , to allow for parametric types like suspensions Q (section 6.5 of
[8]). The formation rule for a HIT T introduces a constant T : (f :F )w Ui , were
Q Q Q Q
(f :F )w abbreviates (f1 :F1 ) (f2 :F2 ) . . . (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
Q n constructor, its introduction rule is a rule introducing the constant
Ki : (f :F )0
Q
H ¯0
i where Hi is some n-path space in T f (defined below)
,
w (x:R)l
and each Rk is a type not involving T in any way.
4 M. Girardi et al.
(f : F )0w may be a subsequence of (f : F )w , as in the constructor refl 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
j
Pi1i1 · · · Piaia = Pj1j1 · · · Pjbb
where each of the Pw is Kh (t̄h ), 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 reflexivity path. If n = 0 the only path space is T f¯0 istelf. In
other words, only reflexivities and suitably instantiated previous constructors
can appear in the output type of a constructor.
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 : (f :F )w T f¯ → U on the
Q
Q Q
constructors of T . More precisely, for each constructor Ki : (f :F )0w (x:R)l Hi
Q Q
we have to provide a term ci : (f :F )0
w (x:R)l Hi where Hi is the lifted path space
of (Ki (fˆ0 , x̄) : Hi ), defined as:
j
– if Hi is a level n ≥ 1 path space Pi1i1 · · · Piaia = Pj1j1 · · · Pjbb , then Hi
ε ε ¯0 ε εj
is Pi1i1 ∗ · · · ∗Piaia =n,C f
P j1 ∗ · · · ∗Pjb b , where if Pw is Kh (t̄h ), then Pw is
K (fˆ0 x̄) j1
i
ch (t̄h ). 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
reflr for some (n − 1)-path r, then this gets lifted to reflr0 , 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ˆ0 x̄))
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:
Y Y Y Y
indT : C(f¯, x)
T f¯→U ) (ci : (f :F )0 κ ¯
Q Q
(x:R)l Hi )i=1 (x:T f )
Q
(f :F )w (C: (f :F )
w w
Computation rule It is possible to generalizeQ the notion of apd in [8] to higher
paths: if χ : α = β is an n-path and g : x:A C(x) is a dependent map, then
apdng (χ) : apdgn−1 (α) =n,C
χ apdn−1
g (β) is defined by path induction on χ.
g :≡ indTQ(f¯, C, c1 , . . . , cκ ) : x:T f¯ C(f¯, x). Let
Q
For the rest of the section let Q
us now consider constructor Ki : (f :F )0 (x:R)l Hi at level n.
w
A General Syntax for Nonrecursive Higher Inductive Types 5
– if n = 0 we get the usual judgmental computation rule, as in [1].
– if n = 1 we have a rule introducing a constant
Y Y
Ci : apd1g (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
j
typecheck: in fact, if Hi is Pi1i1 · · · Piaia = Pj1j1 · · · Pjbb we have
f¯0 j
apdng (Ki (f¯0 , x̄)) : apdgn−1 (Pi1i1 · · · Piaia ) =n,C
K (fˆ0 ,x̄)
apdgn−1 (Pj1j1 · · · Pjbb )
i
ε ε f¯0 ε εj
ci (f¯0 , x̄) : Pi1i1 ∗ · · · ∗Piaia =n,C P j1 ∗ · · · ∗Pjb b
Ki (fˆ0 ,x̄) j1
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
n,C f¯0
jb
n−1 j1
ΦKi (fˆ0 ,x̄) : apdn−1
g (Pi1i1 · · · Piaia ) =K ˆ0
apd g (P j · · · P j ) '
i (f ,x̄) 1 b
n,C f¯0
εjb
ε ε εj1
Pi1i1 ∗ · · · ∗Piaia =K P
(fˆ0 ,x̄) j1
∗ · · · ∗Pjb
i
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
Y Y
Ci : ΦKi (fˆ0 ,x̄) apdng (Ki (fˆ0 , x̄)) = ci (fˆ0 , x̄)
(f :F )0w (x:R)l
4 An example: the torus
Consider the torus T 2 as defined 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 =1,C
p cb ), and (cq : cb =1,C
q cb )
– A 2-pathover (csurf : cp ∗cq =2,C
surf cq ∗cp )
6 M. Girardi et al.
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 reflects the intuition of recognizing the structure of T 2 in the fibration
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 Q equivalent.
As for the computation rules, let g :≡ indT 2 (C, cb , cp , cq , csurf ) : x:T 2 C(x).
– At level 0 we have as usual the judgmental equality (g(b) ≡ cb ).
– At level 1 we have two propositional equalities: (Cp : apd1g (p) = cp ) and
(Cq : apd1g (q) = cq ).
– At level 2 let Φsurf : apd1g (p q) =2,C 1 2,C
surf apdg (q p) ' cp ∗ cq =surf cq ∗cp be
the equivalence given by theorem 1, which maps α to the following path:
A General Syntax for Nonrecursive Higher Inductive Types 7
α 2C
apd1g (p q) surf
apd1g (q p)
apd1g (p)∗apd1g (q) apd1g (q)∗apd1g (p)
Cp Cq Cq Cp
cp ∗cq cq ∗cp
There is an hidden application of trspC2 (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 (apd2g (surf)) = csurf , that amounts to the
commutativity of a square as in [7].
5 Conclusion
In this paper we have proposed a syntax for a broad class of HITs. This allows us
in the first 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, Università 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., Mörtberg, 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., Kovács, A.: Signatures and induction principles for higher inductive-
inductive 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)