From 2e1684b34997f3612232ab2c4f13ab0214253939 Mon Sep 17 00:00:00 2001 From: phi16 Date: Wed, 13 Nov 2024 01:39:33 +0900 Subject: [PATCH] chore: fix typo (#441) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit # Description fix typo: x and y swapped. ``` x --refl--> x | : p | filler : p∙q v v y ----q---> z ``` --- src/1Lab/Path.lagda.md | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/1Lab/Path.lagda.md b/src/1Lab/Path.lagda.md index c0f9fb7c9..ce9de83e5 100644 --- a/src/1Lab/Path.lagda.md +++ b/src/1Lab/Path.lagda.md @@ -486,10 +486,10 @@ with faces $p$, $q$, $r$, and $s$, as in the diagram below. {a_{00}} && {a_{10}} \\ \\ {a_{01}} && {a_{11}} - \arrow["q(i)"', from=1-1, to=3-1] - \arrow["p(j)", from=1-1, to=1-3] - \arrow["s(i)", from=1-3, to=3-3] - \arrow["r(j)"', from=3-1, to=3-3] + \arrow["p(j)"', from=1-1, to=3-1] + \arrow["q(i)", from=1-1, to=1-3] + \arrow["r(j)", from=1-3, to=3-3] + \arrow["s(i)"', from=3-1, to=3-3] \end{tikzcd}\] ~~~ ::: @@ -1506,10 +1506,10 @@ for the single composition, whose type we read as saying that $\refl x && y \\ & {\bullet\text{-filler}~ p~ q} \\ x && z - \arrow["{\refl}", from=1-1, to=1-3] - \arrow["{p}"', from=1-1, to=3-1] - \arrow["{p \bullet q}", dashed, from=1-3, to=3-3] - \arrow["{q}"', from=3-1, to=3-3] + \arrow["{p}", from=1-1, to=1-3] + \arrow["{\refl}"', from=1-1, to=3-1] + \arrow["{q}", from=1-3, to=3-3] + \arrow["{p \bullet q}"', dashed, from=3-1, to=3-3] \end{tikzcd}\] ~~~