---

Step * 2 of Lemma term-to-path_wf


1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X.𝕀 ⊢ _:(A)p}
4. I : fset(ℕ)
5. alpha : X(I)
⊢ ((λa)(alpha) I 1 0) = (a)[0(𝕀)](alpha) ∈ A(alpha)
BY
{ (RepUR ``cubical-lambda cubical-term-at csm-ap-term csm-ap csm-id-adjoin`` 0
   THEN RepUR ``csm-adjoin interval-0 interval-1 csm-id csm-ap`` 0
   THEN Fold `cc-adjoin-cube` 0
   THEN Fold `cubical-term-at` 0) }

1
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X.𝕀 ⊢ _:(A)p}
4. I : fset(ℕ)
5. alpha : X(I)
⊢ a((1(alpha);0)) = a((alpha;0)) ∈ A(alpha)

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  A  :  \{X  \mvdash{}  \_\}
3.  a  :  \{X.\mBbbI{}  \mvdash{}  \_:(A)p\}
4.  I  :  fset(\mBbbN{})
5.  alpha  :  X(I)
\mvdash{}  ((\mlambda{}a)(alpha)  I  1  0)  =  (a)[0(\mBbbI{})](alpha)


By

---

Latex:
(RepUR  ``cubical-lambda  cubical-term-at  csm-ap-term  csm-ap  csm-id-adjoin``  0
  THEN  RepUR  ``csm-adjoin  interval-0  interval-1  csm-id  csm-ap``  0
  THEN  Fold  `cc-adjoin-cube`  0
  THEN  Fold  `cubical-term-at`  0)

---

Home Index