abstract and how-to

includes knowledgification of all notations

Author: MevenBertrand

Manuscript/beyond-gcic.tex

@@ -53,7 +53,7 @@ \subsection{The discrete model}
 analysis} in order to resolve casts. For the former, we build upon the work of
 \sidetextcite{Pedrot2018} on the exceptional type theory \kl{ExTT}.
 For the latter, we reuse the technique of \textcite{Boulier2017} to equip the universe with
-an elimination principle $\typerec$%
+an elimination principle $\intro*\typerec$%
 \sidenote{Corresponding to a form of ad-hoc polymorphism.},
 which requires induction-recursion to be implemented.
 %
@@ -117,7 +117,7 @@ \subsection{The monotone model}
 
 \AP The precision order of the monotone model can be reflected back to
 \kl{CCIC}, giving rise to the \intro{propositional precision} judgment
-$\tcol{\Gamma} \vdash \tcol{t} \precision{\tcol{T}}{\tcol{U}} \tcol{u}$, where
+$\tcol{\Gamma} \vdash \tcol{t} \intro*\precision{\tcol{T}}{\tcol{U}} \tcol{u}$, where
 $\tcol{T}$ and $\tcol{U}$ are the respective types of $\tcol{t}$ and $\tcol{u}$.
 Type dependency naturally demands such a notion of inhomogeneous precision,
 rather than a simpler notion relating only terms of the same type.
@@ -133,7 +133,7 @@ \subsection{The monotone model}
 a judgment that does not hold for \kl{definitional precision}.
 %
 In particular, \kl{propositional precision} is invariant by \kl{conversion}: if
-$\tcol{t} \conv \tcol{t'}$, $\tcol{u} \conv \tcol{u'}$ and
+$\tcol{t} \aconv \tcol{t'}$, $\tcol{u} \aconv \tcol{u'}$ and
 $\tcol{\Gamma} \vdash \tcol{t} \precision{\tcol{T}}{\tcol{U}} \tcol{u}$
 then
 $\tcol{\Gamma} \vdash \tcol{t'} \precision{\tcol{T}}{\tcol{U}}
@@ -180,10 +180,10 @@ \subsection{The monotone model}
     \tcol{\Gamma} \vdash \tcol{\cast{T}{U}{t}} \precision{\tcol{U}}{\tcol{U}} \tcol{u}
     \Leftrightarrow  \tcol{\Gamma} \vdash \tcol{t} \precision{\tcol{T}}{\tcol{U}} \tcol{u}
     \Leftrightarrow  \tcol{\Gamma} \vdash \tcol{t}
-    \precision{\tcol{T}}{\tcol{T}} \tcol{\cast{U}{T} u}
+    \precision{\tcol{T}}{\tcol{T}} \tcol{\cast{U}{T}{u}}
   \end{align*}
   And furthermore,
-    $\tcol{\Gamma} \vdash \tcol{{\cast{U}{T}{\cast{T}{U}{t}}} \precision{\tcol{T}}{\tcol{T}} \tcol{t}}$ – this is the retraction property.
+    $\tcol{\Gamma} \vdash \tcol{\cast{U}{T}{\cast{T}{U}{t}}} \precision{\tcol{T}}{\tcol{T}} \tcol{t}$ – this is the retraction property.
 \end{theorem}
 
 
@@ -224,7 +224,7 @@ \subsection{The issue with propositional equality}
 but are no longer equivalent in \kl{CCIC}. 
 Consider the two functions $\tcol{\id_{\Nat}}$ and $\tcol{\addz}$ defined respectively as
 $\tcol{\id_{\Nat}} \coloneqq \tcol{\l x : \Nat.\ n}$ and
-$\tcol{\addz} \coloneqq \tcol{\l x : \Nat.\ x + 0}$.
+$\tcol{\addz} \coloneqq \tcol{\l x : \Nat.\ x + \z}$.
 In \kl{CIC}, these functions are not convertible, but they are pointwise equal,
 and observationally equivalent.
 However, they would not be observationally equivalent in \kl{GCIC} under our assumptions.
@@ -305,7 +305,7 @@ \subsection{Solutions for vectors}
       -> Vectf A m -> Vectf A n.
 \end{coqcode}
 Here, \coqe{eq_nat} is the type of \emph{decidable} equality proofs between natural numbers,
-expressing the constraints on $n$ – \eg $\eqty{n}{0}$ – but avoiding the use of the unavailable propositional equalities –, which can be defined like this:
+expressing the constraints on $n$ – \eg $\eqty{n}{\z}$ – but avoiding the use of the unavailable propositional equalities –, which can be defined like this:
 \begin{coqcode}
   Fixpoint eq_nat (m n : ℕ) : Type :=
   match m, n with
@@ -356,14 +356,14 @@ \subsection{Solutions for vectors}
   }}[V-cons-s]\label{red:v-S}
   \and
   \redrule{\tcol{
-    \castrev{\left(\vcons[A][k]{a}{v}\right)}{\GVect(A,\S n)}{\GVect(B,0)} 
+    \castrev{\left(\vcons[A][k]{a}{v}\right)}{\GVect(A,\S n)}{\GVect(B,\z)} 
   }}{\tcol{
-    \err[\GVect(B,0)]
+    \err[\GVect(B,\z)]
   }}[V-cons-0]\label{red:v-S0} \and
   \redrule{\tcol{
-    \castrev{\left(\gvcons[A][k]{a}{v}\right)}{\GVect(A,\?[\Nat])}{\GVect(B,0)} 
+    \castrev{\left(\gvcons[A][k]{a}{v}\right)}{\GVect(A,\?[\Nat])}{\GVect(B,\z)} 
   }}{\tcol{
-    \err[\GVect(B,0)]
+    \err[\GVect(B,\z)]
   }}[V-cons?-0]\label{red:v-S?0}
 \end{mathpar}
 \caption{Casts between gradual vector types (excerpt)}
@@ -384,7 +384,7 @@ \subsection{Solutions for vectors}
 %
 Finally, as expected, \ruleref{red:v-S0} raises an error when the indices do not match.
 Similarly, \ruleref{red:v-S?0} also raises an error when trying to create a vector of length
-$0$ from one with an unknown index, but whose underlying vector is non-empty.
+$\z$ from one with an unknown index, but whose underlying vector is non-empty.
 
 \begin{figure}[ht]
 \ContinuedFloat
@@ -393,7 +393,7 @@ \subsection{Solutions for vectors}
 \redrule{\tcol{
   \ind{\Vect}{\gvnil[A]}{y.z.P}{b_{\vnil},y_1.y_2.y_3.p_{y_3}.b_{\vconsop}}
 }}
-{\tcol{\castrev{b_{\vnil}}{\mathop{P}0}{\mathop{P} \?[\Nat]}
+{\tcol{\castrev{b_{\vnil}}{\mathop{P}\z}{\mathop{P} \?[\Nat]}
 }}[V-rect-nil?]\label{red:v-rect-unk-0}
 
 \end{mathpar}
@@ -409,7 +409,7 @@ \subsection{Solutions for vectors}
 Intuitively, they transfer the cast on vectors to a cast on the reduct.
 
 Note that all of these rules crucially use the fact that it is possible to discriminate between
-$\tcol{0}$, $\tcol{\S n}$ and $\tcol{\?[\Nat]}$,
+$\tcol{\z}$, $\tcol{\S n}$ and $\tcol{\?[\Nat]}$,
 which is a specificity of the vector type and explains why
 this solution is not possible for \eg the equality.
 
@@ -511,7 +511,7 @@ \section{A Reasonably Gradual Type Theory}
 Technically, the two layers are defined using two distinct universe hierarchies.
 %
 Second, based on the seminal work on Observational Type Theory \sidecite{Altenkirch2007}, 
-\kl{TTOBS} provides a setoidal equality in a specific universe $\SProp$
+\kl{TTOBS} provides a setoidal equality in a specific universe $\intro*\SProp$
 of definitionally proof-irrelevant propositions. 
 This universe of strict propositions, introduced by \sidecite{Gilbert2019}
 and supported in recent versions of \kl{Coq} and \kl{Agda}, 

Manuscript/biblio.bib

@@ -3683,6 +3683,16 @@ @Book{Curry1958
   priority  = {prio3},
 }
 
+@Article{QuantaPA,
+  author       = {Kevin Hartnett},
+  date         = {2020-10-01},
+  journaltitle = {Quanta Magazine},
+  title        = {Building the Mathematical Library of the Future},
+  url          = {https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/},
+  urldate      = {2022-04-20},
+  priority     = {prio3},
+}
+
 @Comment{jabref-meta: databaseType:biblatex;}
 
 @Comment{jabref-meta: grouping:

Manuscript/bidir-ccw.tex

@@ -25,14 +25,14 @@ \subsection{McBride’s discipline}
 we mean:
 \begin{itemize}
   \item $\vdash \Gamma$ in the case of a context $\Gamma$,
-  \item $\Gamma \vdash T : \uni$ in the case of a type $T$,
+  \item $\Gamma \vdash T \ty \uni$ in the case of a type $T$,
   \item the existence of some $T$ such that $\Gamma \vdash t \ty T$ in the case of a term $t$.
 \end{itemize}
 We also use \reintro{well-typed} for a term, with the same meaning as \kl{well-formed}.
 
-\AP In the case of \intro{inference} $\inferty{\Gamma}{t}{T}$, the subject is $t$,
+\AP In the case of \intro{inference} $\intro*\inferty{\Gamma}{t}{T}$, the subject is $t$,
 $\Gamma$ is an input and $T$ is an output.
-On the contrary, in \intro{checking} $\checkty{\Gamma}{t}{T}$, $t$ is still the subject
+On the contrary, in \intro{checking} $\intro*\checkty{\Gamma}{t}{T}$, $t$ is still the subject
 and $\Gamma$ is an input, but this time $T$ is an input as well.
 This means that one should consider whether $\inferty{\Gamma}{t}{T}$
 only in cases where $\vdash \Gamma$ is already known,
@@ -73,7 +73,7 @@ \subsection{McBride’s discipline}
 
 \AP Beyond the already mentioned inference and checking judgements,
 we need to introduce a third one: \intro{constrained inference}, written
-$\pinferty{h}{\Gamma}{t}{T}$, where $h$ is either $\Pi$ or $\uni$.%
+$\intro*\pinferty{h}{\Gamma}{t}{T}$, where $h$ is either $\Pi$ or $\uni$.%
 \sidenote{These are the only type formers in \kl{CCω}, but
 in \kl{PCUIC}, $h$ can also be \eg an inductive type.}
 Constrained inference is a judgement – or, rather, a family of judgements indexed by $h$ –
@@ -236,7 +236,7 @@ \subsection{Constrained inference in disguise}
 and the other judgements are inlined.
 Once again, reduction is not enough to perform constrained inference, this time
 because type constructors can be hidden in subsets:
-an inhabitant of a type such as $\{f : \Nat \to \Nat \mid f\ 0 = 0 \}$
+an inhabitant of a type such as $\{f : \Nat \to \Nat \mid f\ \z = \z \}$
 should be usable as a function of type $\Nat \to \Nat$.
 An erasure procedure is therefore required on top of reduction to remove subsets in the places where we use constrained inference.
 

Manuscript/bidir-intro.tex

@@ -46,7 +46,7 @@
 bidirectional structure for itself. Moreover, in the case of
 \textcite{Coquand1996} and \textcite{Norell2007}, they concentrate on bidirectional typing
 as a way to remedy for the lack of annotations on their \kl{Curry-style} λ-abstractions.
-This is sensible when looking for lightness of the input syntax, but poses an inherent completeness problem: a term such as $(\l x . x)~0$ is not typeable in those systems.%
+This is sensible when looking for lightness of the input syntax, but poses an inherent completeness problem: a term such as $(\l x . x)~\z$ is not typeable in those systems.%
 \sidenote{They are actually only able to give types to normal forms.}
 In the context of \kl{Church-style} abstraction, the closest there is to a description of
 bidirectional typing for \kl{CIC} is probably the one given by the

Manuscript/gradual-dependent.tex

@@ -231,10 +231,10 @@ \section{Safety and Normalization, Endangered}[Safety and Normalization]
 %
 
 First, any \kl{closed term} can be ascribed the unknown type $\?$
-and then any other type: for instance, $0 \ascop \? \ascop \Bool$ is a
+and then any other type: for instance, $\z \ascop \? \ascop \Bool$ is a
 well-typed closed term of type $\Bool$.%
 \sidenote{
-  We write $a \ascop A$ for a type \intro{ascription}, which we define as syntactic sugar
+  We write $\intro*\asc{a}{A}$ for a type \intro{ascription}, which we define as syntactic sugar
   for $(\l x:A.\ x)\ a$ \cite{Siek2006}; in
   other systems, it is taken as a primitive notion \cite{Garcia2016}.}%
 \margincite{Siek2006}%
@@ -274,7 +274,7 @@ \subsection{Axioms}
 why would one want to gradualize \kl{CIC} instead of simply postulating
 an axiom for any term (be it a program or a proof) that one does not feel like providing (yet)?
 
-\AP Indeed, we can augment \kl{CIC} with a wildcard axiom $\axiom \ty \P A : \uni.\ A$.
+\AP Indeed, we can augment \kl{CIC} with a wildcard axiom $\intro*\axiom \ty \P A : \uni.\ A$.
 The resulting system, called \intro{CICax}, has an obvious practical benefit: we can use
 $\axiom A$%
 %\sidenote{Hereafter written $\axiom[A]$.}
@@ -335,13 +335,13 @@ \subsection{Exceptions}
 which coincides with that of programming languages with exceptions.
 
 \kl{ExTT} is essentially \kl{CICrai}, that is, it
-extends \kl{CIC} with an indexed exceptional term $\rai[A]$ that can inhabit any type $A$.
+extends \kl{CIC} with an indexed exceptional term $\intro*\rai[A]$ that can inhabit any type $A$.
 But instead of being treated as a computational black box like $\axiom A$,
 $\rai[A]$ is endowed with computational content
 emulating exceptions in programming languages, which propagate instead of being stuck.
 %
 For instance, in \kl{ExTT} the following conversion holds:
-\[\ind{\Bool}{\rai[\Bool]}{\Nat}{0,1} \conv \rai[\Nat]\]
+\[\ind{\Bool}{\rai[\Bool]}{\Nat}{\z,1} \conv \rai[\Nat]\]
 
 \AP Notably, such exceptions are \intro{call-by-name} exceptions, so one can only
 discriminate exceptions on positive types – \ie inductive types –, not on negative
@@ -490,7 +490,7 @@ \subsection{Gradual guarantees}
 possibilities for the impact of type information on program behaviour,
 compared to what was originally intended \sidecite{Siek2006}.
 %
-Consequently, \textcite{Siek2015} brought forth type \intro{precision} – denoted $\pre$ –
+Consequently, \textcite{Siek2015} brought forth type \intro{precision} – denoted $\intro*\pre$ –
 as the key notion, from which consistency can be derived: two types $A$ and $B$
 are consistent if and only if there exists $T$ such that $T \pre A$ and $T \pre B$.
 The \kl{unknown type} $\?$ is the most imprecise type of all,
@@ -546,15 +546,15 @@ \subsection{Gradual guarantees}
 \label{def:obsapprox}
   A term $\Gamma \vdash t \ty T$ \kl{observationally error-approximates}
   a term $\Gamma \vdash t' \ty T'$, noted $ t
-  \obsApprox t'$, if for all boolean-valued observation contexts
+  \intro*\obsApprox t'$, if for all boolean-valued observation contexts
   $\mathcal{C} : (\Gamma \vdash T) \Rightarrow (\vdash \Bool)$
   closing over all free variables, either
   \begin{itemize}
   \item $\mathcal{C}[t]$ and $\mathcal{C}[t']$ both diverge; 
   \item otherwise if $\mathcal{C}[t'] \red \err[\Bool]$, then $\mathcal{C}[t] \red \err[\Bool]$.
   \end{itemize}
 
-  Two terms $t$ and $t'$ are \intro{observationally equivalent}, written $t \obsEquiv t'$,
+  Two terms $t$ and $t'$ are \intro{observationally equivalent}, written $t \intro*\obsEquiv t'$,
   if they are related by \kl{observational error-approximation} in both directions.
 \end{definition}
 
@@ -610,7 +610,7 @@ \subsection{Graduality}
 %
 \AP The retraction part further states that $a$ is not only more \kl{precise}
 than$\asc{\asc{a}{B}}{A}$ – which is given by the unit of the adjunction –
-but is \reintro{equi-precise} to it – noted $t \equiprecise \asc{\asc{t}{B}}{A}$.
+but is \reintro{equi-precise} to it – noted $t \intro*\equiprecise \asc{\asc{t}{B}}{A}$.
 Because the \kl{DGG} dictates that precision implies \kl{observational error-approximation},
 \kl{equi-precision} implies \kl{observational equivalence},
 and so losing and recovering precision must produce a term that is \kl{observationally
@@ -840,7 +840,7 @@ \subsection{Observational refinement}
 \begin{definition}[\intro{Observational refinement}]
 \label{def:obsref}
   A term $\Gamma \vdash t \ty A$ \kl{observationally refines} a term
-  $\Gamma \vdash u \ty A$, noted $t \obsRef u$, if for all boolean-valued observation context
+  $\Gamma \vdash u \ty A$, noted $\intro* t \obsRef u$, if for all boolean-valued observation context
   $\mathcal{C} \ty (\Gamma \vdash A) \Rightarrow (\vdash \Bool)$ closing over all
   free variables, if $\mathcal{C}[u] \red \err[\Bool]$ or diverges,
   then either $\mathcal{C}[t] \red \err[\Bool]$ or $\mathcal{C}[t]$ diverges.
@@ -1254,9 +1254,9 @@ \subsection{Typing, Conversion and Bidirectional Elaboration}
 In order to satisfy \kl{conservativity} with respect to \kl{CIC}, ascriptions in \kl{GCIC}
 are required to satisfy \kl(grad){consistency}. For instance, $\asc{\asc{\true}{\?}}{\Nat}$ is well-typed by \kl(grad){consistency} – used twice –, but $\asc{\true}{\Nat}$ is ill-typed.
 Such ascriptions in \kl{CastCIC} are realized by casts.
-For instance $\asc{\asc{0}{\?}}{\Bool}$ in \kl{GCIC} elaborates
+For instance $\asc{\asc{\z}{\?}}{\Bool}$ in \kl{GCIC} elaborates
 – up to desugaring and reduction – to
-$\castrev{\castrev{0}{\Nat}{\?[\uni]}}{\?[\uni]}{\Bool}$ in \kl{CastCIC}.
+$\castrev{\castrev{\z}{\Nat}{\?[\uni]}}{\?[\uni]}{\Bool}$ in \kl{CastCIC}.
 A major difference between ascriptions in \kl{GCIC} and casts in \kl{CastCIC} is
 that casts are not required to satisfy \kl(grad){consistency}: a cast between any
 two types is well-typed, although of course it might produce an