---

Step * 1 1 of Lemma trivial-constrained-term


1. Gamma : CubicalSet{j}
2. B : {Gamma ⊢ _}
3. xx : Top
4. x : {Gamma ⊢ _:B}
5. I : fset(ℕ)
6. a : Gamma(I)
7. 0(𝔽)(a) = 1 ∈ Point(face_lattice(I))
⊢ (x I a) = (xx I a) ∈ B(a)
BY
{ (RepUR ``face-0 cubical-term-at`` -1 THEN Assert ⌜¬(0 = 1 ∈ Point(face_lattice(I)))⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  B  :  \{Gamma  \mvdash{}  \_\}
3.  xx  :  Top
4.  x  :  \{Gamma  \mvdash{}  \_:B\}
5.  I  :  fset(\mBbbN{})
6.  a  :  Gamma(I)
7.  0(\mBbbF{})(a)  =  1
\mvdash{}  (x  I  a)  =  (xx  I  a)


By

---

Latex:
(RepUR  ``face-0  cubical-term-at``  -1  THEN  Assert  \mkleeneopen{}\mneg{}(0  =  1)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index