---

Step * of Lemma Kanfiller_wf

∀[X:CubicalSet]. ∀[A:{X ⊢ _(Kan)}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].
∀[bx:A-open-box(X;Kan-type(A);I;alpha;J;x;i)].
  (filler(x;i;bx) ∈ {cube:Kan-type(A)(alpha)| fills-A-open-box(X;Kan-type(A);I;alpha;bx;cube)} )
BY
{ ((UnivCD THENA Auto) THEN MemTypeCD) }

1
1. X : CubicalSet
2. A : {X ⊢ _(Kan)}
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;Kan-type(A);I;alpha;J;x;i)
⊢ filler(x;i;bx) ∈ Kan-type(A)(alpha)

2
.....set predicate..... 
1. X : CubicalSet
2. A : {X ⊢ _(Kan)}
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;Kan-type(A);I;alpha;J;x;i)
⊢ fills-A-open-box(X;Kan-type(A);I;alpha;bx;filler(x;i;bx))

3
.....wf..... 
1. X : CubicalSet
2. A : {X ⊢ _(Kan)}
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;Kan-type(A);I;alpha;J;x;i)
9. cube : Kan-type(A)(alpha)
⊢ fills-A-open-box(X;Kan-type(A);I;alpha;bx;cube) ∈ Type

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_(Kan)\}].  \mforall{}[I:Cname  List].  \mforall{}[alpha:X(I)].  \mforall{}[J:nameset(I)  List].
\mforall{}[x:nameset(I)].  \mforall{}[i:\mBbbN{}2].  \mforall{}[bx:A-open-box(X;Kan-type(A);I;alpha;J;x;i)].
    (filler(x;i;bx)  \mmember{}  \{cube:Kan-type(A)(alpha)|  fills-A-open-box(X;Kan-type(A);I;alpha;bx;cube)\}  )


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  MemTypeCD)

---

Home Index