---

Step * 1 1 of Lemma face-forall-q=0

.....subterm..... T:t
3: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))
⊢ (q=0)((s(a);<new-name(I)>)) = (new-name(I)=0) ∈ Point(face_lattice(I+new-name(I)))
BY
{ RepUR ``face-zero cc-adjoin-cube cc-snd cubical-term-at`` 0 }

1
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))
⊢ dM-to-FL(I+new-name(I);¬(<new-name(I)>)) = (new-name(I)=0) ∈ Point(face_lattice(I+new-name(I)))

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
1.  Gamma  :  CubicalSet\{j\}
2.  I  :  fset(\mBbbN{})
3.  a  :  Gamma(I)
4.  (\mforall{}new-name(I).(new-name(I)=0))  =  if  (new-name(I)  =\msubz{}  new-name(I))  then  0  else  (new-name(I)=0)  fi 
\mvdash{}  (q=0)((s(a);<new-name(I)>))  =  (new-name(I)=0)


By

---

Latex:
RepUR  ``face-zero  cc-adjoin-cube  cc-snd  cubical-term-at``  0

---

Home Index