---

Step * 1 1 of Lemma context-subset-term-0


1. Gamma : CubicalSet{j}
2. T : {Gamma ⊢ _}
3. x : Top
⊢ x ∈ I:fset(ℕ) ⟶ a:{rho:Gamma(I)| 0 = 1 ∈ Point(face_lattice(I))}  ⟶ T(a)
BY
{ (RepeatFor 2 ((FunExt THENA Auto)) THEN D -1 THEN (Assert ¬(0 = 1 ∈ Point(face_lattice(I))) BY Auto) THEN Auto) }

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  T  :  \{Gamma  \mvdash{}  \_\}
3.  x  :  Top
\mvdash{}  x  \mmember{}  I:fset(\mBbbN{})  {}\mrightarrow{}  a:\{rho:Gamma(I)|  0  =  1\}    {}\mrightarrow{}  T(a)


By

---

Latex:
(RepeatFor  2  ((FunExt  THENA  Auto))  THEN  D  -1  THEN  (Assert  \mneg{}(0  =  1)  BY  Auto)  THEN  Auto)

---

Home Index