---

Step * 2 2 of Lemma csm-Kan-cubical-type_wf


1. Delta : CubicalSet
2. Gamma : CubicalSet
3. s : Delta ⟶ Gamma
4. A : {Gamma ⊢ _}
5. filler : I:(Cname List)
⟶ alpha:Gamma(I)
⟶ J:(nameset(I) List)
⟶ x:nameset(I)
⟶ i:ℕ2
⟶ A-open-box(Gamma;A;I;alpha;J;x;i)
⟶ A(alpha)
6. Kan-A-filler(Gamma;A;filler)
7. ∀I:Cname List. ∀alpha:Gamma(I). ∀J:nameset(I) List. ∀x:nameset(I). ∀i:ℕ2. ∀bx:A-open-box(Gamma;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 I alpha J x i bx alpha f)
        = (filler K f(alpha) map(f;J) (f x) i A-open-box-image(Gamma;A;I;K;f;alpha;bx))
        ∈ A(f(alpha))))
8. I : Cname List
9. alpha : Delta(I)
10. J : nameset(I) List
11. x : nameset(I)
12. i : ℕ2
13. bx : A-open-box(Delta;(A)s;I;alpha;J;x;i)
14. K : Cname List
15. f : name-morph(I;K)
16. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
17. ↑isname(f x)
⊢ (filler I (s)alpha J x i bx alpha f)
= (filler K (s)f(alpha) map(f;J) (f x) i A-open-box-image(Delta;(A)s;I;K;f;alpha;bx))
∈ (A)s(f(alpha))
BY
{ TACTIC:(InstHyp [⌜I⌝;⌜(s)alpha⌝;⌜J⌝;⌜x⌝;⌜i⌝;⌜bx⌝;⌜K⌝;⌜f⌝] 7⋅ THENA Auto) }

1
1. Delta : CubicalSet
2. Gamma : CubicalSet
3. s : Delta ⟶ Gamma
4. A : {Gamma ⊢ _}
5. filler : I:(Cname List)
⟶ alpha:Gamma(I)
⟶ J:(nameset(I) List)
⟶ x:nameset(I)
⟶ i:ℕ2
⟶ A-open-box(Gamma;A;I;alpha;J;x;i)
⟶ A(alpha)
6. Kan-A-filler(Gamma;A;filler)
7. ∀I:Cname List. ∀alpha:Gamma(I). ∀J:nameset(I) List. ∀x:nameset(I). ∀i:ℕ2. ∀bx:A-open-box(Gamma;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 I alpha J x i bx alpha f)
        = (filler K f(alpha) map(f;J) (f x) i A-open-box-image(Gamma;A;I;K;f;alpha;bx))
        ∈ A(f(alpha))))
8. I : Cname List
9. alpha : Delta(I)
10. J : nameset(I) List
11. x : nameset(I)
12. i : ℕ2
13. bx : A-open-box(Delta;(A)s;I;alpha;J;x;i)
14. K : Cname List
15. f : name-morph(I;K)
16. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
17. ↑isname(f x)
18. (filler I (s)alpha J x i bx (s)alpha f)
= (filler K f((s)alpha) map(f;J) (f x) i A-open-box-image(Gamma;A;I;K;f;(s)alpha;bx))
∈ A(f((s)alpha))
⊢ (filler I (s)alpha J x i bx alpha f)
= (filler K (s)f(alpha) map(f;J) (f x) i A-open-box-image(Delta;(A)s;I;K;f;alpha;bx))
∈ (A)s(f(alpha))

---

Latex:

---

Latex:

1.  Delta  :  CubicalSet
2.  Gamma  :  CubicalSet
3.  s  :  Delta  {}\mrightarrow{}  Gamma
4.  A  :  \{Gamma  \mvdash{}  \_\}
5.  filler  :  I:(Cname  List)
{}\mrightarrow{}  alpha:Gamma(I)
{}\mrightarrow{}  J:(nameset(I)  List)
{}\mrightarrow{}  x:nameset(I)
{}\mrightarrow{}  i:\mBbbN{}2
{}\mrightarrow{}  A-open-box(Gamma;A;I;alpha;J;x;i)
{}\mrightarrow{}  A(alpha)
6.  Kan-A-filler(Gamma;A;filler)
7.  \mforall{}I:Cname  List.  \mforall{}alpha:Gamma(I).  \mforall{}J:nameset(I)  List.  \mforall{}x:nameset(I).  \mforall{}i:\mBbbN{}2.
      \mforall{}bx:A-open-box(Gamma;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  I  alpha  J  x  i  bx  alpha  f)
                =  (filler  K  f(alpha)  map(f;J)  (f  x)  i  A-open-box-image(Gamma;A;I;K;f;alpha;bx))))
8.  I  :  Cname  List
9.  alpha  :  Delta(I)
10.  J  :  nameset(I)  List
11.  x  :  nameset(I)
12.  i  :  \mBbbN{}2
13.  bx  :  A-open-box(Delta;(A)s;I;alpha;J;x;i)
14.  K  :  Cname  List
15.  f  :  name-morph(I;K)
16.  \mforall{}i:nameset(I).  ((i  \mmember{}  J)  {}\mRightarrow{}  (\muparrow{}isname(f  i)))
17.  \muparrow{}isname(f  x)
\mvdash{}  (filler  I  (s)alpha  J  x  i  bx  alpha  f)
=  (filler  K  (s)f(alpha)  map(f;J)  (f  x)  i  A-open-box-image(Delta;(A)s;I;K;f;alpha;bx))


By

---

Latex:
TACTIC:(InstHyp  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}(s)alpha\mkleeneclose{};\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}bx\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]  7\mcdot{}  THENA  Auto)

---

Home Index