paper: polish Future Work

paper/paper.tex

@@ -837,7 +837,7 @@ \subsection{Dependencies in inequality proofs\label{sec:le}}
 leR_trans ?p leR_refl = ?p
 leR_trans leR_refl ?p = ?p
 \end{minted}
-%
+
 where \texttt{leR\_trans} is transitivity, \texttt{leR\_refl} is reflexivity, and \texttt{?p} is an existential variable. These two problems definitionally hold in \SProp, but equating them does not solve the existential. For unification to be useful in inferring existentials, we present our first variant of $\leq$, which we dub as the ``Yoneda variant'':
 
 \begin{minted}{coq}
@@ -864,11 +864,11 @@ \subsection{Groupoid properties of equality and basic type isomorphisms\label{se
 As a final remark, note that as a consequence of $\eta$-conversion for finite enumerated types, the requirement of functional extensionality disappears when $\nu$ is finite. However, this is a conversion which Coq does not implement, and the alternative would be to replace $\Pi a: \nu.\, B$ by a ``flat'' iterated product $B(1) \times B(2) \times \ldots \times B(\nu)$.
 
 \section{Future work}
-The construction could be extended with degeneracies as well as with permutations~\citep{grandis03}. Dependent $\nu$-sets could also be defined, opening the way to construct $\Pi$-types and $\Sigma$-types of $\nu$-sets. A $\nu$-set of $\nu$-sets representing a universe could also be defined (as sketched e.g. in a talk by Herbelin at the HoTT-UF workshop for the bridge case~(\citeyear{herbelin-hott-uf})). More generally, we believe these lines of work to eventually provide alternative models to parametric type theories~\citep{nuyts17,cavallo19}.
+The construction could be extended with degeneracies as well as with permutations~\citep{grandis03}. Dependent $\nu$-sets could also be defined, opening the way to construct $\Pi$-types and $\Sigma$-types of $\nu$-sets. A $\nu$-set of $\nu$-sets representing a universe could also be defined (as sketched e.g. in a talk at the HoTT-UF workshop for the bridge case~(\citeyear{herbelin-hott-uf})). More generally, we believe these lines of work to eventually provide alternative models to parametric type theories~\citep{nuyts17,cavallo19} where equality of types, now a family rather than the total space of a fibration, is not only definitionally isomorphic to bridges~\cite{bernardy15} but definitionally the same as bridges.
 
 By equipping the universe construction with a structure of equivalences, as suggested along the lines of \cite{altenkirch15}, we also suspect the construction to be able to serve as a basis for syntactic models of various versions of cubical type theory~\citep{bezem13,cohen16,angiuli21}, saving the detour via the fibered approach inherent to usual presheaf models. In particular, we wonder whether the indexed approach might provide definitional properties which are otherwise lost when detouring via presheaves. In particular, we conjecture being able to justify univalence holding definitionally. Our approach would also definitively ground cubical type theory in iterated parametricity.
 
-Another direction for future work would also be to generically construct the indexed form of any presentation of presheaves over a direct category and to show the equivalence between the two presentations.
+Another direction for future work is to give a general definition of presheaf in indexed form over a direct category and to show the equivalence with the standard definition of presheaf.
 
 \newpage
 \bibliographystyle{msclike}