You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
If \(\alpha, \beta\) are type indices, then a \emph{path} \(\alpha\tpath\beta\) is a nonempty finite subset of \(\lambda^\bot\) with maximal element \(\alpha\) and minimal element \(\beta\).\footnote{In previous versions, we used ordered lists (more precisely, a quiver structure) to represent paths. This had the effect that editing paths at the bottom was much easier than editing paths at the top. In this implementation, we are making the decision to put both types of edit on equal footing (and neither will definitionally reduce).}
103
+
If \(\alpha, \beta\) are type indices, then a \emph{path} \(\alpha\tpath\beta\) is a nonempty finite subset of \(\lambda^\bot\) with maximal element \(\alpha\) and minimal element \(\beta\).\footnote{In previous versions, we used ordered lists (more precisely, a quiver structure) to represent paths. This had the effect that editing paths at the bottom was much easier than editing paths at the top. In this implementation, we are making the decision to put both types of edit on equal footing (and neither will definitionally reduce). TODO: It might be cleaner to still use a cons-list format but encapsulate it lots.}
104
104
A path \(\alpha\tpath\bot\) is called an \emph{\(\alpha\)-extended index}.
105
105
We write \(\nil(\alpha) \) for the path \(\{\alpha\} : \alpha\tpath\alpha\).
106
106
If \( h \) is a proof of \(\beta < \alpha\), we write \(\single(h) \) for the path \(\{\alpha, \beta\} : \alpha\tpath\beta\).
Then an \emph{\(\alpha\)-structural permutation} is an \(\alpha\)-tree of base permutations.
185
-
The type of \(\alpha\)-structural permutations is written \(\StrPerm_\alpha\).
184
+
Then an \emph{\(\alpha\)-structural permutation} (or just \emph{\(\alpha\)-permutation}) is an \(\alpha\)-tree of base permutations.
185
+
The type of \(\alpha\)-permutations is written \(\StrPerm_\alpha\).
186
186
\end{definition}
187
-
As an implementation detail, we create a typeclass \texttt{StrPermClass}\(_\alpha\) for permutations that `act like' \(\alpha\)-structural permutations: they have a group structure and a canonical group homomorphism to\(\StrPerm_\alpha\).
188
-
When we quantify over structural permutations in this paper, it should be formalised using an additional quantification over \texttt{StrPermClass}\(_\alpha\).
187
+
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\(\StrPerm_\alpha\).
188
+
When we quantify over structural permutations in this paper, it should be formalised using an additional quantification over \(\texttt{StrPermClass}_\alpha\).
A \emph{base support} is a pair \( S = (S^\Atom, S^\NearLitter) \) where \( S^\Atom\) is an enumeration of atoms and \( S^\NearLitter\) is an enumeration of near-litters.
222
222
There are precisely \(\#\mu\) base supports.
223
223
224
-
A \emph{\(\beta\)-structural support} is a \(\beta\)-tree of base supports.
224
+
A \emph{\(\beta\)-structural support} (or just \emph{\(\beta\)-support}) is a \(\beta\)-tree of base supports.
225
+
The type of \(\beta\)-supports is writte \(\StrSupp_\beta\).
225
226
There are precisely \(\#\mu\) structural supports for any type index \(\beta\).
226
-
Following \cref{def:Tree}, structural supports have derivatives, structural permutations act on structural supports, and there is a group action of \(\beta\)-structural permutations on \(\beta\)-structural supports.
227
-
If \( S \) is a \(\beta\)-structural support and \( A : \alpha\tpath\beta\), the coderivative \( S^A \) is the \(\alpha\)-support given by
227
+
Following \cref{def:Tree}, structural supports have derivatives, structural permutations act on structural supports, and there is a group action of \(\beta\)-permutations on \(\beta\)-supports.
228
+
If \( S \) is a \(\beta\)-support and \( A : \alpha\tpath\beta\), the coderivative \( S^A \) is the \(\alpha\)-support given by
228
229
\[ (S^A)_B = \begin{cases}
229
230
S_C & \text{if } B = A_C \text{ for some } C \\
230
231
\varnothing & \text{otherwise}
231
232
\end{cases} \]
232
233
Thus \( (S^A)_A = S \).
234
+
235
+
Let \(\tau\) be a type, and let \( G \) be a \(\texttt{StrPermClass}_\beta\)-group that acts on \(\tau\).
236
+
We say that \( S \)\emph{supports} \( x : \tau\) under the action of \( G \) if whenever \(\pi : G \) fixes \( S \), it also fixes \( x \).
\item\(\StrSet_\alpha\coloneq\prod_{\beta : \lambda^\bot} \beta < \alpha\to\StrSet_\beta\) where \(\alpha : \lambda\).
241
245
\end{itemize}
242
246
These equalities will in fact only be equivalences in the formalisation.
243
-
We define the action of \(\alpha\)-structural permutations (more precisely, inhabitants of some type with a \texttt{StrPermClass}\(_\alpha\) instance) on \(\alpha\)-structural sets by well-founded recursion.
247
+
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.
244
248
\begin{itemize}
245
249
\item\(\pi(x) = \pi_{\nil(\bot)}(x) \) if \(\alpha\equiv\bot\);
246
250
\item\(\pi(x) = (\beta, h \mapsto\pi_h(x(\beta, h))) \) if \(\alpha : \lambda\).
247
251
\end{itemize}
248
252
\end{definition}
253
+
254
+
\section{Position functions}
255
+
\begin{definition}[position function]
256
+
\label{def:Position}
257
+
\uses{def:Params}
258
+
Let \(\tau\) be a type.
259
+
A \emph{position function} for \(\tau\) is an injection \(\iota : \tau\to\mu\).
260
+
This is a typeclass.
261
+
\end{definition}
262
+
\begin{proposition}[injective functions from denied sets]
263
+
\label{prop:funOfDeny}
264
+
\uses{def:Params}
265
+
Let \(\tau\) be a type such that \(\#\tau\leq\#\mu\).
266
+
Let \( D : \tau\to\Set(\mu) \) be a function such that for each \( x : \tau\), the set \( D(x) \), called the \emph{denied set} of \( x \), has size less than \(\cof(\ord(\#\mu)) \).
267
+
Then there is an injective function \( f : \tau\to\mu\) such that if \(\nu\in D(x) \), then \(\nu < f(x) \).
268
+
\end{proposition}
269
+
\begin{proof}
270
+
Pick a well-ordering \(\prec\) of \(\tau\) of length at most \(\ord(\#\mu) \).
271
+
Define \( f \) by well-founded recursion on \(\prec\).
272
+
Suppose that we have already defined \( f \) for all \( y \prec x \).
273
+
Then let
274
+
\[ X = \{ f(y) \mid y \prec x \}\cup D(x) \]
275
+
This set has size less than \(\cof(\ord(\#\mu)) \), so it is not cofinal in \(\mu\).
276
+
So there is some \(\nu : \mu\) such that \(\forall\nu' \in X,\,\nu > \nu' \).
277
+
Set \( f(x) = \nu\).
278
+
\end{proof}
279
+
\begin{proposition}[base positions]
280
+
\label{prop:BasePositions}
281
+
\uses{def:Position}
282
+
There are position functions on \(\Atom, \NearLitter\) that are jointly injective and satisfy
283
+
\begin{itemize}
284
+
\item\(\iota(\NL(a^\circ)) < \iota(a) \) for every atom \( a \);
285
+
\item\(\iota(\NL(N^\circ)) \leq\iota(N) \) for every near-litter \( N \);
286
+
\item\(\iota(a) < \iota(N) \) for every near-litter \( N \) and atom \( a \in N \symmdiff\LS(N^\circ) \).\footnote{TODO: Make syntax for \( N \symmdiff\LS(N^\circ) \).}
287
+
\end{itemize}
288
+
We register these position functions as instances for use in typeclass inference.
289
+
We also define \(\iota(L) = \iota(\NL(L)) \) for litters.
290
+
\end{proposition}
291
+
\begin{proof}
292
+
\uses{prop:funOfDeny}
293
+
First, establish an equivalence \( f_\Litter : \Litter\simeq\mu\).
294
+
Use \cref{prop:funOfDeny} to obtain an injective map \( f_\Atom : \NearLitter\to\mu\) such that \( f_\Litter(a^\circ) < f_\Atom(a) \) for each atom \( a \).
295
+
Now use \cref{prop:funOfDeny} again to obtain an injective map \( f_\NearLitter : \NearLitter\to\mu\) such that
296
+
\[ f_\Litter(N^\circ) < f_\NearLitter(N);\quad f_\Atom(a) < f_\NearLitter(N) \text{ for } a \in N \symmdiff\LS(N^\circ) \]
297
+
Endow \( 3 \times\mu\) with its lexicographic order, of order type \(\ord(\#\mu) \), giving an order isomorphism \( e : 3 \times\mu\simeq\mu\).
e(0, f_\Litter(N^\circ)) & \text{if } N = \NL(N^\circ) \\
301
+
e(2, f_\NearLitter(N)) & \text{otherwise}
302
+
\end{cases} \]
303
+
\end{proof}
304
+
305
+
\section{Hypotheses of the recursion}
306
+
\begin{definition}[model data]
307
+
\label{def:ModelData}
308
+
\uses{def:StrSupport,def:StrSet}
309
+
Let \(\alpha\) be a type index.
310
+
\emph{Model data} at type \(\alpha\) consists of:
311
+
\begin{itemize}
312
+
\item a \(\TSet_\alpha\) called the type of \emph{tangled sets} or \emph{t-sets}, which will be our type of model elements at level \(\alpha\), with an embedding \( U_\alpha : \TSet_\alpha\to\StrSet_\alpha\);
313
+
\item a group \(\AllPerm_\alpha\) called the type of \emph{allowable permutations}, with a \(\texttt{StrPermClass}_\alpha\) instance and a specified action on \(\TSet_\alpha\),
314
+
\end{itemize}
315
+
such that
316
+
\begin{itemize}
317
+
\item if \(\pi : \AllPerm_\alpha\) and \( x : \TSet_\alpha\), then \(\pi(U_\alpha(x)) = U_\alpha(\pi(x)) \);
318
+
\item every t-set of type \(\alpha\) has an \(\alpha\)-support (\cref{def:StrSupport}) for its action under the \(\alpha\)-allowable permutations;
319
+
\end{itemize}
320
+
\end{definition}
321
+
\begin{definition}[tangle]
322
+
\label{def:Tangle}
323
+
\uses{def:ModelData}
324
+
Let \(\alpha\) be a type index with model data.
325
+
The type \(\Tang_\alpha\) of \emph{\(\alpha\)-tangles}, as well as the operations \(\set : \Tang_\alpha\to\TSet_\alpha\) and \(\supp : \Tang_\alpha\to\StrSupp_\alpha\) are defined by cases.
326
+
\begin{itemize}
327
+
\item If \(\alpha : \lambda\), an \(\alpha\)-tangle is a pair \( t = (x, S) \) where \( x \) is a tangled set of type \(\alpha\) and \( S \) is a support for \( x \).
328
+
We define \(\set(t) = x \) and \(\supp(t) = S \).
329
+
\item A \(\bot\)-tangle is a t-set \( x : \TSet_\bot\).\footnote{This is not the same as an atom: given arbitrary model data at type \(\bot\), we have no way of knowing if its \(\TSet\) is the same as \(\Atom\), all that we know is that \(\TSet_\bot\) embeds into \(\Atom\).}
330
+
We define \(\set(x) = x \), and make \(\supp(x) \) be the \(\bot\)-support corresponding to the base support \( (1, f) \) where \( (0, a) \in f \) and \( a \) is the atom corresponding to the type-\(\bot\) t-set \( U_\bot(x)\).
331
+
\end{itemize}
332
+
Allowable permutations \(\pi\) act on tangles \( t \) in the following way.
333
+
\begin{itemize}
334
+
\item If \(\alpha : \lambda\), then \(\pi((x, S)) = (\pi(x), \pi(S)) \).
335
+
\item If \(\alpha\equiv\bot\), then \(\pi(x) \) is already defined.
336
+
\end{itemize}
337
+
In each case, \(\supp(t) \) supports \( t \) for its action under the allowable permutations.
Let \(\alpha\) be a proper type index with model data, and suppose that \(\Tang_\alpha\) has a position function.
343
+
We say that \(\alpha\) has \emph{typed near-litters} if there is a function \(\typed_\alpha : \NearLitter\to\TSet_\alpha\) such that
344
+
\begin{itemize}
345
+
\item if \(\pi : \AllPerm_\alpha\) and \( N : \NearLitter\), then \(\pi(\typed_\alpha(N)) = \typed_\alpha(\pi_\bot(N)) \); and
346
+
\item if \( N \) is a near-litter and \( t \) is an \(\alpha\)-tangle such that \(\set(t) = \typed_\alpha(N) \), we have \(\iota(N) \leq\iota(t) \).
347
+
\end{itemize}
348
+
Objects of the form \(\typed_\alpha\) are called \emph{typed near-litters}.
349
+
\end{definition}
350
+
\begin{definition}[coherent data]
351
+
\label{def:CoherentData}
352
+
\uses{def:TypedNearLitter,prop:Path.rec}
353
+
Let \(\alpha\) be a proper type index.
354
+
Suppose that we have model data for all type indices \(\beta\leq\alpha\), position functions for \(\Tang_\beta\) for all \(\beta < \alpha\), and typed near-litters for all \(\beta < \alpha\).
355
+
We say that the model data is \emph{coherent} below level \(\alpha\) if the following hold.
356
+
\begin{itemize}
357
+
\item For \(\gamma < \beta\leq\alpha\), there is a map \(\AllPerm_\beta\to\AllPerm_\gamma\) that commutes with the coercions from \(\AllPerm_{(-)} \) to \(\StrPerm_{(-)} \).
358
+
We can use this map to define arbitrary derivatives of allowable permutations by \cref{prop:Path.rec}.
359
+
\item If \( (x, S) \) is a \(\beta\)-tangle for \(\beta < \alpha\), and \( y \) is an atom or near-litter\footnote{We might want to encapsulate atoms and near-litters somehow. We could make a typeclass, or write theorems in terms of the coproduct \(\Atom\oplus\NearLitter\).} that occurs in the range of \( S_A \), then \(\iota(y) < \iota(x, S) \).
0 commit comments