---

Step * 1 of Lemma unit-pathtype


1. G : CubicalSet{j}
2. a : {G ⊢ _:Path(1)}
3. b : {G ⊢ _:Path(1)}
4. I : fset(ℕ)
5. a1 : G(I)
⊢ (a I a1) = (b I a1) ∈ Path(1)(a1)
BY
{ (DVar `a' THEN DVar `b') }

1
1. G : CubicalSet{j}
2. a : I:fset(ℕ) ⟶ a:G(I) ⟶ Path(1)(a)
3. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a@0:G(I).  ((a I a@0 a@0 f) = (a J f(a@0)) ∈ Path(1)(f(a@0)))
4. b : I:fset(ℕ) ⟶ a:G(I) ⟶ Path(1)(a)
5. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:G(I).  ((b I a a f) = (b J f(a)) ∈ Path(1)(f(a)))
6. I : fset(ℕ)
7. a1 : G(I)
⊢ (a I a1) = (b I a1) ∈ Path(1)(a1)

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  a  :  \{G  \mvdash{}  \_:Path(1)\}
3.  b  :  \{G  \mvdash{}  \_:Path(1)\}
4.  I  :  fset(\mBbbN{})
5.  a1  :  G(I)
\mvdash{}  (a  I  a1)  =  (b  I  a1)


By

---

Latex:
(DVar  `a'  THEN  DVar  `b')

---

Home Index