Step
*
of Lemma
sq_stable_uniform-Kan-A-filler
∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[filler:I:(Cname List)
⟶ alpha:X(I)
⟶ J:(nameset(I) List)
⟶ x:nameset(I)
⟶ i:ℕ2
⟶ A-open-box(X;A;I;alpha;J;x;i)
⟶ A(alpha)].
SqStable(uniform-Kan-A-filler(X;A;filler))
BY
{ (Auto
THEN (D 0 THENA Auto)
THEN UseWitness ⌜λa,b,c,d,e,f,g,h,i,j. Ax⌝⋅
THEN D -1
THEN All (Unfold `uniform-Kan-A-filler`)
THEN RepeatFor 10 ((MemCD THENA Auto))
THEN MemCD
THEN BackThruSomeHyp
THEN Auto) }
Latex:
Latex:
\mforall{}[X:CubicalSet]. \mforall{}[A:\{X \mvdash{} \_\}]. \mforall{}[filler:I:(Cname List)
{}\mrightarrow{} alpha:X(I)
{}\mrightarrow{} J:(nameset(I) List)
{}\mrightarrow{} x:nameset(I)
{}\mrightarrow{} i:\mBbbN{}2
{}\mrightarrow{} A-open-box(X;A;I;alpha;J;x;i)
{}\mrightarrow{} A(alpha)].
SqStable(uniform-Kan-A-filler(X;A;filler))
By
Latex:
(Auto
THEN (D 0 THENA Auto)
THEN UseWitness \mkleeneopen{}\mlambda{}a,b,c,d,e,f,g,h,i,j. Ax\mkleeneclose{}\mcdot{}
THEN D -1
THEN All (Unfold `uniform-Kan-A-filler`)
THEN RepeatFor 10 ((MemCD THENA Auto))
THEN MemCD
THEN BackThruSomeHyp
THEN Auto)
Home
Index