paper: minor polish

paper/paper.tex

@@ -874,16 +874,14 @@ \subsection{Dependencies in inequality proofs\label{sec:le}}
 Compared to \texttt{leY}, \texttt{leI} has no proof-irrelevance properties. This definition is specially crafted for $\painting$, where we have to reason inductively from $p \leq n$ to $n$. In our usage, we have lemmas \texttt{leY\_of\_leI} and \texttt{leI\_of\_leY} in order to equip \texttt{leY} with the induction scheme of \texttt{leI}. The resulting induction scheme has computational rules holding propositionally.
 
 \subsection{Groupoid properties of equality and basic type isomorphisms\label{sec:eqproperties}}
-The construction relies on the groupoid properties of equality in some places, which have to be made explicit in the formalization.
-
-Notice that in table~\ref{fulltab:coh}, the use of the isomorphism between $u = v$ and $\Sigma (p:u.\hd = v.\hd). (u.\tl = v.\tl)$ for $u$ and $v$ in a $\Sigma$-type is left implicit. Also implicit is the use of the isomorphism between $f = g$ and $\Pi a: A.\, f(a) = g(a)$ for $f$ and $g$ in $\Pi a: A.\, B$, where it should be recalled that the right-to-left map, or functional extensionality, holds by default in extensional type theory.
+The construction relies on the groupoid properties of equality which are left implicit in table~\ref{fulltab:coh}. The use of the equivalence between $u = v$ and $\Sigma (p:u.\hd = v.\hd). (u.\tl = v.\tl)$ for $u$ and $v$ in a $\Sigma$-type is left implicit in the same table. Also implicit is the use of the equivalence between $f = g$ and $\Pi a: A.\, f(a) = g(a)$ for $f$ and $g$ in $\Pi a: A.\, B$, where it should be recalled that the right-to-left map, or functional extensionality, holds by default in extensional type theory. These have to be made explicit in the formalization.
 
 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$-set 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}.
 
-By equipping the universe construction with a structure of equivalences, as suggested along the lines of Altenkirch and Kaposi~(\citeyear{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.
+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.