---

Step * of Lemma cubical-path-condition-0

∀[I:fset(ℕ)]. ∀[Gamma,A,i,rho,u,a0:Top].  cubical-path-condition(Gamma;A;I;i;rho;0;u;a0)
BY
{ (Intros THEN RepeatFor 2 ((D 0 THENA Auto))) }

1
1. I : fset(ℕ)
2. Gamma : Top
3. A : Top
4. i : Top
5. rho : Top
6. u : Top
7. a0 : Top
8. J : fset(ℕ)
9. f : I,0(J)
⊢ (a0 (i0)(rho) f) = u((i0) ⋅ f) ∈ A(f((i0)(rho)))

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[Gamma,A,i,rho,u,a0:Top].    cubical-path-condition(Gamma;A;I;i;rho;0;u;a0)


By

---

Latex:
(Intros  THEN  RepeatFor  2  ((D  0  THENA  Auto)))

---

Home Index