Preparatory work for unification

Author: v--

text/dependent_types.tex

@@ -11,7 +11,7 @@ \section{Dependent types}\label{sec:dependent_types}
   \begin{thmenum}
     \thmitem{rem:dependent_type_rule_formalization/context} \hyperref[def:type_context]{Type contexts} must be well-formed as per \cref{rem:well_formed_context}. This requires us to implement a mechanism for finding, for any type used, a derivation tree demonstrating that it is well-formed.
 
-    \thmitem{rem:dependent_type_rule_formalization/relations} We need to allow defining binary relations as per \fullref{thm:recursively_defined_relations}. This complicates \hyperref[con:unification]{unification} for the two sides of a transitive binary relation, which should be allowed to match arbitrarily complicated expressions.
+    \thmitem{rem:dependent_type_rule_formalization/relations} We need to allow defining binary relations in analogy with \fullref{thm:recursively_defined_relations}. This complicates \hyperref[con:unification]{unification} for the two sides of a transitive binary relation, which should be allowed to match arbitrarily complicated expressions.
 
     \thmitem{rem:dependent_type_rule_formalization/equality} The main binary relation we will use is \hyperref[con:equality]{judgmental equality}, which subsumes \hyperref[def:lambda_term_alpha_equivalence]{\( \alpha \)-equivalence}, \hyperref[def:typed_term_reduction]{\( \beta \)-reduction} and \hyperref[def:typed_term_reduction]{\( \eta \)-reduction}. This makes unification subtle even without other binary relations involved, because, rather than considering a concrete term or type, we must now work with equivalence classes and conceive a way for picking a particular member when needed.
 

text/lambda_term_alpha_equivalence.tex

@@ -377,7 +377,7 @@ \section{\texorpdfstring{\( \muplambda \)}{λ}-term \texorpdfstring{\( \alpha \)
 \begin{definition}\label{def:lambda_substitution_composition}\mimprovised
   We define the \term{composition} \( \Bbbt\Bbbs \) of the \hyperref[def:atomic_lambda_term_substitution]{atomic \( \muplambda \)-term substitutions} \( \Bbbs \) and \( \Bbbt \) as
   \begin{equation}\label{eq:def:lambda_substitution_composition}
-    \parens[\big]{ \Bbbt\Bbbs }(x) \coloneqq x[\Bbbs][\Bbbt].
+    (\Bbbt\Bbbs)(x) \coloneqq x[\Bbbs][\Bbbt].
   \end{equation}
 
   This extends recursively to any number of substitutions, starting with the identity \( \id \) as a nullary composition.