---

Step * of Lemma face-1-in-context-subset

No Annotations
∀[G:j⊢]. ∀[phi:{G ⊢ _:𝔽}].  (phi = 1(𝔽) ∈ {G, phi ⊢ _:𝔽})
BY
{ (Intros THEN CubicalTermEqual THEN Auto THEN (RepUR ``context-subset`` -1 THENA Auto)) }

1
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. I : fset(ℕ)
4. a : {rho:G(I)| phi(rho) = 1 ∈ Point(face_lattice(I))} 
⊢ (phi I a) = (1(𝔽) I a) ∈ 𝔽(a)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[phi:\{G  \mvdash{}  \_:\mBbbF{}\}].    (phi  =  1(\mBbbF{}))


By

---

Latex:
(Intros  THEN  CubicalTermEqual  THEN  Auto  THEN  (RepUR  ``context-subset``  -1  THENA  Auto))

---

Home Index