+1

letter.tex

··· 16 \item I have corrected a mistake in \textbf{Example: definitional lenses for finite ordinals}, where I previously did not qualify that the loops on $\mathcal{F}(m)$ only form a proper set when $m \geq 2$. 17 \item I have added an example, \textbf{Definitional lenses over discrete reflexive graphs}, in order to illustrate how the coproduct of reflexive graphs arises from lenses. I have also moved the definition of discrete reflexive graphs earlier as requested. 18 \item I have corrected a typographical error in \textbf{Characterising identification induction with dependent lenses} (formerly \textbf{Characterising identification induction with midpoint lenses}) in which $\otimes_A$ was given the type $A\times A\to B$ rather than $A\times A\to A$. 0 19 \item I have significantly shortened the introduction to reflect reasonable assumptions about the audience, as requested. 20 \item I have added a mention to the introduction of Observational Type Theory as an alternative design as requested. 21 \item I have renamed the \textbf{bivariant midpoint lens} to \textbf{unbiased dependent lens}.

··· 16 \item I have corrected a mistake in \textbf{Example: definitional lenses for finite ordinals}, where I previously did not qualify that the loops on $\mathcal{F}(m)$ only form a proper set when $m \geq 2$. 17 \item I have added an example, \textbf{Definitional lenses over discrete reflexive graphs}, in order to illustrate how the coproduct of reflexive graphs arises from lenses. I have also moved the definition of discrete reflexive graphs earlier as requested. 18 \item I have corrected a typographical error in \textbf{Characterising identification induction with dependent lenses} (formerly \textbf{Characterising identification induction with midpoint lenses}) in which $\otimes_A$ was given the type $A\times A\to B$ rather than $A\times A\to A$. 19 + \item I have corrected a typographical error in \textbf{Binary product of path objects} in which $\gB$ was written as $\gA$. 20 \item I have significantly shortened the introduction to reflect reasonable assumptions about the audience, as requested. 21 \item I have added a mention to the introduction of Observational Type Theory as an alternative design as requested. 22 \item I have renamed the \textbf{bivariant midpoint lens} to \textbf{unbiased dependent lens}.

+1 -1

nodes/po-closure-properties.tex

··· 98 99 100 \begin{corollary}[Binary product of path objects]\label[corollary]{lem:bin-prod-po} 101 - If $\gA$ and $\gA$ are path objects, then so is $\gA\times \gB$. 102 \end{corollary} 103 104 \begin{proof}

··· 98 99 100 \begin{corollary}[Binary product of path objects]\label[corollary]{lem:bin-prod-po} 101 + If $\gA$ and $\gB$ are path objects, then so is $\gA\times \gB$. 102 \end{corollary} 103 104 \begin{proof}

-2

reviews/review2-excerpts.md

··· 29 Page 19: Definition 48 could use a citation or proof sketch for getting 30 between 1/2 to 3/4. 31 32 - Page 20: type in Corollary 55, an A should be a B 33 - 34 Page 27: Since the paper is generally working in an informal type theory 35 style, it seems worth a comment that Definitional lens and related 36 definitions cannot be an internal definition because they require a

··· 29 Page 19: Definition 48 could use a citation or proof sketch for getting 30 between 1/2 to 3/4. 31 0 0 32 Page 27: Since the paper is generally working in an informal type theory 33 style, it seems worth a comment that Definitional lens and related 34 definitions cannot be an internal definition because they require a