michael/blog
1
0
Fork 0
Code Issues 1 Pull requests Releases Packages Wiki Activity

add the j
All checks were successful
ci/woodpecker/push/woodpecker Pipeline was successful
Details

Browse source
This commit is contained in:
Michael Zhang 2024-09-18 16:27:15 -05:00
parent c9c6365c87
commit 4273a1ca0b
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/content/posts/2024-09-18-hcomp/index.lagda.md
View file

@ -118,6 +118,11 @@ We can use $\mathsf{isProp}$ to generate us some faces, except using $x$ and $p(
![](./frontback.jpg) ![](./frontback.jpg)
Writing this down as code, we get:
* $(j = \mathsf{i0}) \rightarrow f(x, p(i), k)$
* $(j = \mathsf{i1}) \rightarrow f(x, q(i), k)$
This time, the $i$ dimension has the $\mathsf{refl}$ edges. This time, the $i$ dimension has the $\mathsf{refl}$ edges.
Since all the edges on the bottom face as $\mathsf{refl}$, we can just use the constant $\mathsf{refl}_{\mathsf{refl}_x}$ as the bottom face. Since all the edges on the bottom face as $\mathsf{refl}$, we can just use the constant $\mathsf{refl}_{\mathsf{refl}_x}$ as the bottom face.
In cubical, this is the constant expression `x`. In cubical, this is the constant expression `x`.