---

Step * 1 1 1 of Lemma sq_stable_Kan-A-filler


1. [X] : CubicalSet
2. [A] : {X ⊢ _}
3. [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)
4. I : Cname List
5. alpha : X(I)
6. J : nameset(I) List
7. x@0 : nameset(I)
8. i : ℕ2
9. bx : A-open-box(X;A;I;alpha;J;x@0;i)
10. [f] : {f:A-face(X;A;I;alpha)| (f ∈ bx)} 
11. ↓let y,b,w = f in 
     (filler I alpha J x@0 i bx alpha (y:=b)) = w ∈ A((y:=b)(alpha))
⊢ let y,b,w = f in 
(filler I alpha J x@0 i bx alpha (y:=b)) = w ∈ A((y:=b)(alpha))
BY
{ (UseWitness ⌜Ax⌝⋅ THEN RepeatFor 2 (DVar `f') THEN DVar `f1' THEN All Reduce) }

1
1. X : CubicalSet
2. A : {X ⊢ _}
3. 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)
4. I : Cname List
5. alpha : X(I)
6. J : nameset(I) List
7. x@0 : nameset(I)
8. i : ℕ2
9. bx : A-open-box(X;A;I;alpha;J;x@0;i)
10. x : nameset(I)
11. i1 : ℕ2
12. f2 : A((x:=i1)(alpha))
13. (<x, i1, f2> ∈ bx)
14. ↓(filler I alpha J x@0 i bx alpha (x:=i1)) = f2 ∈ A((x:=i1)(alpha))
⊢ Ax ∈ (filler I alpha J x@0 i bx alpha (x:=i1)) = f2 ∈ A((x:=i1)(alpha))

---

Latex:

---

Latex:

1.  [X]  :  CubicalSet
2.  [A]  :  \{X  \mvdash{}  \_\}
3.  [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)
4.  I  :  Cname  List
5.  alpha  :  X(I)
6.  J  :  nameset(I)  List
7.  x@0  :  nameset(I)
8.  i  :  \mBbbN{}2
9.  bx  :  A-open-box(X;A;I;alpha;J;x@0;i)
10.  [f]  :  \{f:A-face(X;A;I;alpha)|  (f  \mmember{}  bx)\} 
11.  \mdownarrow{}let  y,b,w  =  f  in 
          (filler  I  alpha  J  x@0  i  bx  alpha  (y:=b))  =  w
\mvdash{}  let  y,b,w  =  f  in 
(filler  I  alpha  J  x@0  i  bx  alpha  (y:=b))  =  w


By

---

Latex:
(UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}  THEN  RepeatFor  2  (DVar  `f')  THEN  DVar  `f1'  THEN  All  Reduce)

---

Home Index