---

Step * of Lemma Kanfiller-uniform

∀[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)].
  ∀K:Cname List. ∀f:name-morph(I;K).
    ((∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i))))
    ⇒ (↑isname(f x))
    ⇒ ((filler(x;i;bx) alpha f)
       = filler(f x;i;A-open-box-image(X;Kan-type(A);I;K;f;alpha;bx))
       ∈ Kan-type(A)(f(alpha))))
BY
{ ((UnivCD THENA Auto)
   THEN RepeatFor 2 (DVar `A')
   THEN All Reduce
   THEN All (RepUR ``Kan-type``)
   THEN RepUR ``Kanfiller`` 0
   THEN (Assert uniform-Kan-A-filler(X;A1;A2) BY
               Auto)
   THEN (With ⌜I⌝ (D (-1))⋅ THENA Auto)
   THEN BHyp -1 
   THEN Auto) }

---

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)].
    \mforall{}K:Cname  List.  \mforall{}f:name-morph(I;K).
        ((\mforall{}i:nameset(I).  ((i  \mmember{}  J)  {}\mRightarrow{}  (\muparrow{}isname(f  i))))
        {}\mRightarrow{}  (\muparrow{}isname(f  x))
        {}\mRightarrow{}  ((filler(x;i;bx)  alpha  f)  =  filler(f  x;i;A-open-box-image(X;Kan-type(A);I;K;f;alpha;bx))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepeatFor  2  (DVar  `A')
  THEN  All  Reduce
  THEN  All  (RepUR  ``Kan-type``)
  THEN  RepUR  ``Kanfiller``  0
  THEN  (Assert  uniform-Kan-A-filler(X;A1;A2)  BY
                          Auto)
  THEN  (With  \mkleeneopen{}I\mkleeneclose{}  (D  (-1))\mcdot{}  THENA  Auto)
  THEN  BHyp  -1 
  THEN  Auto)

---

Home Index