Skip to content

Commit

Permalink
chore: fix typo (#441)
Browse files Browse the repository at this point in the history
# Description

fix typo: x and y swapped.

```
  x --refl--> x
  |           :
p |   filler  : p∙q
  v           v
  y ----q---> z
```
  • Loading branch information
phi16 authored Nov 12, 2024
1 parent 6032c6b commit 2e1684b
Showing 1 changed file with 8 additions and 8 deletions.
16 changes: 8 additions & 8 deletions src/1Lab/Path.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -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}\]
~~~
:::
Expand Down Expand Up @@ -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}\]
~~~
Expand Down

0 comments on commit 2e1684b

Please sign in to comment.