---

Step * of Lemma face-type-comp-at-lemma

No Annotations
∀[H:j⊢]. ∀[phi:{H ⊢ _:𝔽}]. ∀[I,J:fset(ℕ)]. ∀[i:ℕ]. ∀[f:J ⟶ I+i]. ∀[v:H(I)].  (phi(f(s(v))) = f(s(phi(v))) ∈ 𝔽(f))
BY
{ Intros }

1
1. H : CubicalSet{j}
2. phi : {H ⊢ _:𝔽}
3. I : fset(ℕ)
4. J : fset(ℕ)
5. i : ℕ
6. f : J ⟶ I+i
7. v : H(I)
⊢ phi(f(s(v))) = f(s(phi(v))) ∈ 𝔽(f)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H:j\mvdash{}].  \mforall{}[phi:\{H  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[I,J:fset(\mBbbN{})].  \mforall{}[i:\mBbbN{}].  \mforall{}[f:J  {}\mrightarrow{}  I+i].  \mforall{}[v:H(I)].
    (phi(f(s(v)))  =  f(s(phi(v))))


By

---

Latex:
Intros

---

Home Index