---

Step * of Lemma face-forall-q=0

No Annotations
∀[Gamma:j⊢]. ((Gamma ⊢ ∀ (q=0)) = 0(𝔽) ∈ {Gamma ⊢ _:𝔽})
BY
{ (Auto
   THEN Symmetry
   THEN CubicalTermEqual
   THEN Auto
   THEN RepUR ``face-0 face-forall`` 0
   THEN (InstLemma `fl_all-fl0` [⌜I⌝;⌜new-name(I)⌝;⌜new-name(I)⌝]⋅ THENA Auto)
   THEN Symmetry
   THEN NthHypEq (-1)
   THEN EqCD
   THEN Auto) }

1
.....subterm..... T:t
2:n
1. Gamma : CubicalSet{j}
2. I : fset(ℕ)
3. a : Gamma(I)
4. (∀new-name(I).(new-name(I)=0))
= if (new-name(I) =z new-name(I)) then 0 else (new-name(I)=0) fi 
∈ Point(face_lattice(I))
⊢ (∀new-name(I).(q=0)((s(a);<new-name(I)>))) = (∀new-name(I).(new-name(I)=0)) ∈ 𝔽(a)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  ((Gamma  \mvdash{}  \mforall{}  (q=0))  =  0(\mBbbF{}))


By

---

Latex:
(Auto
  THEN  Symmetry
  THEN  CubicalTermEqual
  THEN  Auto
  THEN  RepUR  ``face-0  face-forall``  0
  THEN  (InstLemma  `fl\_all-fl0`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}new-name(I)\mkleeneclose{};\mkleeneopen{}new-name(I)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Symmetry
  THEN  NthHypEq  (-1)
  THEN  EqCD
  THEN  Auto)

---

Home Index