---

Step * of Lemma implies-face-forall-holds

No Annotations
∀H:j⊢. ∀phi:{H.𝕀 ⊢ _:𝔽}.  (H.𝕀 ⊢ (1(𝔽) ⇒ phi) ⇒ H ⊢ (1(𝔽) ⇒ (∀ phi)))
BY
{ (Auto THEN D 0 THEN Auto THEN RepUR ``face-forall cubical-term-at`` 0 THEN Fold `cubical-term-at` 0) }

1
1. H : CubicalSet{j}
2. phi : {H.𝕀 ⊢ _:𝔽}
3. H.𝕀 ⊢ (1(𝔽) ⇒ phi)
4. I : fset(ℕ)
5. rho : H(I)
6. 1(𝔽)(rho) = 1 ∈ Point(face_lattice(I))
⊢ (∀new-name(I).phi((s(rho);<new-name(I)>))) = 1 ∈ Point(face_lattice(I))

---

Latex:

---

Latex:
No  Annotations
\mforall{}H:j\mvdash{}.  \mforall{}phi:\{H.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}.    (H.\mBbbI{}  \mvdash{}  (1(\mBbbF{})  {}\mRightarrow{}  phi)  {}\mRightarrow{}  H  \mvdash{}  (1(\mBbbF{})  {}\mRightarrow{}  (\mforall{}  phi)))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  RepUR  ``face-forall  cubical-term-at``  0  THEN  Fold  `cubical-term-at`  0)

---

Home Index