From 4273a1ca0bbf8776e96aa3d90d15ace88f1673de Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Wed, 18 Sep 2024 16:27:15 -0500 Subject: [PATCH] add the j --- src/content/posts/2024-09-18-hcomp/index.lagda.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/content/posts/2024-09-18-hcomp/index.lagda.md b/src/content/posts/2024-09-18-hcomp/index.lagda.md index eb3d87f..4cdc9b9 100644 --- a/src/content/posts/2024-09-18-hcomp/index.lagda.md +++ b/src/content/posts/2024-09-18-hcomp/index.lagda.md @@ -118,6 +118,11 @@ We can use $\mathsf{isProp}$ to generate us some faces, except using $x$ and $p( ![](./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. 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`.