2.3 The structural hierarchy
We will now establish the hierarchy of types that our model will be built inside.
If \( \alpha , \beta \) are type indices, then a path \( \alpha \rightsquigarrow \beta \) is given by the constructors
\( \operatorname {\mathsf{nil}} : \alpha \rightsquigarrow \alpha \);
\( \operatorname {\mathsf{cons}} : (\alpha \rightsquigarrow \beta ) \to (\gamma {\lt} \beta ) \to (\alpha \rightsquigarrow \gamma ) \).
We define by recursion a \( \operatorname {\mathsf{snoc}} \) operation on the top of paths. We also prove the induction principle for \( \operatorname {\mathsf{nil}} \) and \( \operatorname {\mathsf{snoc}} \).
A path \( \alpha \rightsquigarrow \bot \) is called an \( \alpha \)-extended index. We write \( \operatorname {\mathsf{nil}}(\alpha ) \) for the path \( \{ \alpha \} : \alpha \rightsquigarrow \alpha \). If \( h \) is a proof of \( \beta {\lt} \alpha \), we write \( \operatorname {\mathsf{single}}(h) \) for the path \( \{ \alpha , \beta \} : \alpha \rightsquigarrow \beta \).
We have the inequality
Many of the objects in this construction have an associated type level \( \alpha : \lambda ^\bot \), and by application of a path of the form \( \alpha \rightsquigarrow \beta \) or \( \beta \rightsquigarrow \alpha \), we can often define a new object of type level \( \beta \). For this common task, we register the following notation typeclasses.
\( x \Downarrow A \) is the derivative of an object of type \( \beta \) along a path \( A : \beta \rightsquigarrow \gamma \), giving an object of type \( \gamma \);
\( x \downarrow h \) abbreviates \( x \Downarrow \operatorname {\mathsf{single}}(h) \); 1
\( x \underset {\bot }{\Downarrow } A \) is the base derivative of an object of type \( \beta \) along a path \( A : \beta \rightsquigarrow \bot \);
\( x \underset {\bot }{\downarrow } \) abbreviates \( x \underset {\bot }{\Downarrow } \operatorname {\mathsf{single}}(h) \) where \( h \) is the canonical proof of \( \bot {\lt} \beta \) whenever \( \beta : \lambda \);
\( x \Uparrow A \) is the coderivative of an object of type \( \beta \) along a path \( A : \alpha \rightsquigarrow \beta \), giving an object of type \( \alpha \);
\( x \uparrow h \) abbreviates \( x \Uparrow \operatorname {\mathsf{single}}(h) \).
When we say that an object has an associated type level in this context, we mean that the notation typeclass is registered in the following form.
class Derivative (X : Type _) (Y : outParam (Type _))
(β : outParam TypeIndex) (γ : TypeIndex) where
deriv : X → Path β γ → Y
This means that when inferring the type of the expression \( x \Downarrow A \), we first compute the type of \( x \), which gives rise to a unique type index \( \beta \), then the type of \( A \) is inferred to give \( \gamma \), then the output type \( Y \) is uniquely determined.
The reason that we distinguish \( \underset {\bot }{\Downarrow } \) from \( \Downarrow \) is that the associated type \( Y \) is allowed to differ between the two forms. We will give a brief example motivated by a definition we are about to make. For each type index \( \beta \), there is a type of \( \beta \)-structural permutation, comprised of many base permutations. If we have a path \( \beta \rightsquigarrow \gamma \), we can convert a \( \beta \)-structural permutation into a \( \gamma \)-structural permutation; this will be the derivative map. We will see that a given \( \bot \)-structural permutation contains exactly one base permutation, and so the types are in canonical isomorphism. If \( x \) is a \( \beta \)-structural permutation and \( A : \beta \rightsquigarrow \bot \), then \( x \Downarrow A \) is a \( \bot \)-structural permutation, and \( x \underset {\bot }{\Downarrow } A \) is the corresponding base permutation.
Because \( \uparrow , \downarrow \) and others are already used by Lean, we use slightly different notation in practice (e.g. \( \nearrow , \searrow \)). In this writeup, however, we will use subscripts for derivatives and superscripts for coderivatives. We will not distinguish typographically here between the single- and double-struck variants, or between \( \Downarrow \) and \( \underset {\bot }{\Downarrow } \); in the latter case, the syntax \( x_A \) always means \( x \underset {\bot }{\Downarrow } A \) whenever \( A \) has minimal element \( \bot \). We will also use \( x_\gamma \) to denote the derivative \( x_h \) where \( h \) is some proof of \( \gamma {\lt} \beta \), and use \( x^\alpha \) to denote \( x^h \) where \( h : \beta {\lt} \alpha \).
If \( A : \alpha \rightsquigarrow \beta \) and \( B : \beta \rightsquigarrow \gamma \), the derivative \( A_B \) is defined to be the union \( A \cup B : \alpha \rightsquigarrow \gamma \), and the coderivative \( B^A \) is defined to be \( A_B \).
Let \( \tau \) be any type, and let \( \alpha \) be a type index. An \( \alpha \)-tree of \( \tau \) is a function \( t \) that maps each \( \alpha \)-extended index \( A \) to an object \( t_A : \tau \); this defines its base derivatives. The type of \( \bot \)-trees of \( \tau \) is canonically isomorphic to \( \tau \). If \( t \) is an \( \alpha \)-tree and \( A : \alpha \rightsquigarrow \beta \), we define the derivative \( t_A \) to be the \( \beta \)-tree defined by \( (t_A)_B = t_{(A_B)} \). This derivative map is functorial: for any paths \( A : \alpha \rightsquigarrow \beta \) and \( B : \beta \rightsquigarrow \gamma \), we have \( t_{(A_B)} = (t_A)_B \). If \( \tau \) has a group structure, then so does its type of trees: \( (t \cdot u)_A = t_A \cdot u_A \) and \( (t^{-1})_A = (t_A)^{-1} \). If \( \tau \) acts on \( \upsilon \), then \( \alpha \)-trees of \( \tau \) act on \( \alpha \)-trees of \( \upsilon \): \( (t(u))_A = t_A(u_A) \).
If \( \# \tau \leq \# \mu \), there are at most \( \# \mu \)-many \( \alpha \)-trees of \( \tau \), since there are less than \( \operatorname {\mathsf{cof}}(\operatorname {\mathsf{ord}}(\# \mu )) \)-many \( \alpha \)-extended indices, allowing us to conclude by lemma A.6 as each such tree is a subset of \( (\alpha \rightsquigarrow \bot ) \times \tau \) of size less than \( \operatorname {\mathsf{cof}}(\operatorname {\mathsf{ord}}(\# \mu )) \). If \( \# \tau {\lt} \# \mu \), there are less than \( \# \mu \)-many \( \alpha \)-trees of \( \tau \), since there are less than \( \operatorname {\mathsf{cof}}(\operatorname {\mathsf{ord}}(\# \mu )) \)-many \( \alpha \)-extended indices and strong limits are closed under exponentials.
Let \( \alpha \) be a type index. Then an \( \alpha \)-structural permutation (or just \( \alpha \)-permutation) is an \( \alpha \)-tree of base permutations. The type of \( \alpha \)-permutations is written \( \mathsf{StrPerm}_\alpha \).
As an implementation detail, we create a typeclass \( \texttt{StrPermClass}_\alpha \) for permutations that ‘act like’ \( \alpha \)-permutations: they have a group structure and a canonical group embedding into \( \mathsf{StrPerm}_\alpha \). When we quantify over structural permutations in this paper, it should be formalised using an additional quantification over \( \texttt{StrPermClass}_\alpha \).
Let \( \tau \) be a type. An enumeration of \( \tau \) is a pair \( E = (i, f) \) where \( i : \kappa \) and \( f \) is a partial function \( \kappa \to \tau \), such that all domain elements of \( f \) are strictly less than \( i \). 2 If \( x : \tau \), we write \( x \in E \) for \( x \in \operatorname {\mathsf{ran}}f \). The set \( \{ y \mid y \in E \} \), which we may also loosely call \( E \), is small. We will write \( \varnothing \) for the empty enumeration \( (0, \varnothing ) \).
If \( g : \tau \to \sigma \), then \( g \) lifts to a direct image function mapping enumerations of \( \tau \) to enumerations of \( \sigma \):
Thus, \( x \in g(E) \leftrightarrow x \in g[E] \). In the same way, groups that act on \( \tau \) also act on enumerations of \( \tau \). 3 If \( g : \sigma \to \tau \) is injective, then \( g \) lifts to an inverse image function mapping enumerations of \( \tau \) to enumerations of \( \sigma \):
This operation may cause the domain of \( f \) to shrink, but we will keep \( i \) the same.
If \( E = (i, e) \) and \( F = (j, f) \) are enumerations of \( \tau \), we define their concatenation by
This operation commutes with the others: \( x \in E + F \leftrightarrow x \in E \vee x \in F \), \( g[E + F] = g[E] + g[F] \), and \( g^{-1}[E + F] = g^{-1}[E] + g^{-1}[F] \).
We define a partial order on enumerations by setting \( (i, e) \leq (j, f) \) if and only if \( f \) extends \( e \) as a partial function. We obtain various corollaries, such as \( E \leq F \to g(E) \leq g(F) \) and \( E \leq E + F \).
Every small subset of \( \tau \) is the range of some enumeration of \( \tau \).
If \( \# \tau \leq \# \mu \), then there are at most \( \# \mu \)-many enumerations of \( \tau \): enumerations are determined by an element of \( \kappa \) and a small subset of \( \kappa \times \tau \). If \( \# \tau {\lt} \# \mu \), then there are strictly less than \( \# \mu \)-many enumerations of \( \tau \): use the same reasoning and apply lemma A.6.
A base support is a pair \( S = (S^{\mathcal A}, S^{\mathcal N}) \) where \( S^{\mathcal A}\) is an enumeration of atoms and \( S^{\mathcal N}\) is an enumeration of near-litters. There are precisely \( \# \mu \) base supports.
A \( \beta \)-structural support (or just \( \beta \)-support) is a pair \( S = (S^{\mathcal A}, S^{\mathcal N}) \) where \( S^{\mathcal A}\) is an enumeration of \( (\beta \rightsquigarrow \bot ) \times {\mathcal A}\) and \( S^{\mathcal N}\) is an enumeration of \( (\beta \rightsquigarrow \bot ) \times {\mathcal N}\). The type of \( \beta \)-supports is written \( \mathsf{StrSupp}_\beta \). There are precisely \( \# \mu \) structural supports for any type index \( \beta \).
For a path \( A : \beta \rightsquigarrow \bot \), we write \( S_A \) for the base support \( T \) given by
More generally, for a path \( A : \beta \rightsquigarrow \gamma \), we write \( S_A \) for the \( \gamma \)-support \( T \) given by
For a path \( A : \alpha \rightsquigarrow \beta \), we write \( S^A \) for the \( \alpha \)-support \( T \) given by
Clearly, \( (S^A)_A = S \).
\( \beta \)-structural permutations act on pairs \( (A, x) \) by \( \pi (A, x) = (A, \pi _A(x)) \), where \( x \) is either an atom or a near-litter. Hence, structural permutations act on structural supports.
Let \( \tau \) be a type, and let \( G \) be a \( \texttt{StrPermClass}_\beta \)-group that acts on \( \tau \). We say that \( S \) supports \( x : \tau \) under the action of \( G \) if whenever \( \pi : G \) fixes \( S \), it also fixes \( x \), and moreover, if \( \beta = \bot \) then \( S_A^{\mathcal N}\) is empty for any \( A : \bot \rightsquigarrow \bot \) (and of course there is exactly one such path).
The type of \( \alpha \)-structural sets, denoted \( \mathsf{StrSet}_\alpha \), is defined by well-founded recursion on \( \lambda ^\bot \).
\( \mathsf{StrSet}_\bot :={\mathcal A}\);
\( \mathsf{StrSet}_\alpha :=\prod _{\beta : \lambda ^\bot } \beta {\lt} \alpha \to \operatorname {\mathsf{Set}}\mathsf{StrSet}_\beta \) where \( \alpha : \lambda \).
These equalities will in fact only be equivalences in the formalisation. We define the action of \( \alpha \)-permutations (more precisely, inhabitants of some type with a \( \texttt{StrPermClass}_\alpha \) instance) on \( \alpha \)-structural sets by well-founded recursion.
\( \pi (x) = \pi _{\operatorname {\mathsf{nil}}(\bot )}(x) \) if \( \alpha \equiv \bot \);
\( \pi (x) = (\beta , h \mapsto \pi _h[x(\beta , h)]) \) if \( \alpha : \lambda \).