---

Step * 1 of Lemma cubical-path-app-1


1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. t : {X ⊢ _:(Path_A a b)}
6. I : fset(ℕ)
7. a1 : X(I)
⊢ (t I a1 I 1 1) = (b I a1) ∈ A(a1)
BY
{ (RepUR ``path-type`` -3 THEN DVar `t') }

1
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. t : I:fset(ℕ)
⟶ a@0:X(I)
⟶ {p:Path(A) | ∀I,alpha. ((p I 1 0) = a(alpha) ∈ A(alpha)) ∧ ((p I 1 1) = b(alpha) ∈ A(alpha))}(a@0)
6. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a@0:X(I).
     ((t I a@0 a@0 f)
     = (t J f(a@0))
     ∈ {p:Path(A) | ∀I,alpha. ((p I 1 0) = a(alpha) ∈ A(alpha)) ∧ ((p I 1 1) = b(alpha) ∈ A(alpha))}(f(a@0)))
7. I : fset(ℕ)
8. a1 : X(I)
⊢ (t I a1 I 1 1) = (b I a1) ∈ A(a1)

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  A  :  \{X  \mvdash{}  \_\}
3.  a  :  \{X  \mvdash{}  \_:A\}
4.  b  :  \{X  \mvdash{}  \_:A\}
5.  t  :  \{X  \mvdash{}  \_:(Path\_A  a  b)\}
6.  I  :  fset(\mBbbN{})
7.  a1  :  X(I)
\mvdash{}  (t  I  a1  I  1  1)  =  (b  I  a1)


By

---

Latex:
(RepUR  ``path-type``  -3  THEN  DVar  `t')

---

Home Index