---

Step * 2 of Lemma Kan-discrete_wf


1. X : CubicalSet
2. T : Type
⊢ Kan-A-filler(X;discr(T);λI,alpha,J,x,i,bx. (snd(snd(hd(bx)))))
BY
{ RepeatFor 2 ((D 0 THEN Auto)) }

1
1. X : CubicalSet
2. T : Type
3. I : Cname List
4. alpha : X(I)
5. J : nameset(I) List
6. x : nameset(I)
7. i : ℕ2
8. bx : A-open-box(X;discr(T);I;alpha;J;x;i)
9. i@0 : ℕ||bx||
⊢ is-A-face(X;discr(T);I;alpha;(λI,alpha,J,x,i,bx. (snd(snd(hd(bx))))) I alpha J x i bx;bx[i@0])

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  T  :  Type
\mvdash{}  Kan-A-filler(X;discr(T);\mlambda{}I,alpha,J,x,i,bx.  (snd(snd(hd(bx)))))


By

---

Latex:
RepeatFor  2  ((D  0  THEN  Auto))

---

Home Index