---

Step * of Lemma Kan_sigma_filler_uniform

∀X:CubicalSet. ∀A:{X ⊢ _(Kan)}. ∀B:{X.Kan-type(A) ⊢ _(Kan)}.
  uniform-Kan-A-filler(X;Σ Kan-type(A) Kan-type(B);Kan_sigma_filler(A;B))
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN (Assert map(f;J) ∈ nameset(K) List BY
               ((GenConcl ⌜J = L ∈ ({x:Cname| (x ∈ J)}  List)⌝⋅ THENA Auto)
                THEN (Assert ⌜f ∈ {x:Cname| (x ∈ J)}  ⟶ nameset(K)⌝⋅ THENM Auto)
                THEN (FunExt THENA Auto)
                THEN D -1
                THEN DVar `bx'
                THEN BLemma `assert-isname`
                THEN Auto))
   THEN (FLemma `assert-isname` [-2] THENA Auto)
   THEN (Assert l_subset(Cname;map(f;J);K) BY
               ((GenConclTerm ⌜map(f;J)⌝⋅ THENA Auto)
                THEN D 0
                THEN Auto
                THEN RepeatFor 2 (D -1)
                THEN HypSubst' (-1) 0
                THEN GenConclTerm ⌜v[i1]⌝⋅
                THEN Auto
                THEN D -2
                THEN Unhide
                THEN Auto))) }

1
1. X : CubicalSet
2. A : {X ⊢ _(Kan)}
3. B : {X.Kan-type(A) ⊢ _(Kan)}
4. I : Cname List
5. alpha : X(I)
6. J : nameset(I) List
7. x : nameset(I)
8. i : ℕ2
9. bx : A-open-box(X;Σ Kan-type(A) Kan-type(B);I;alpha;J;x;i)
10. K : Cname List
11. f : name-morph(I;K)
12. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
13. ↑isname(f x)
14. map(f;J) ∈ nameset(K) List
15. f x ∈ nameset(K)
16. l_subset(Cname;map(f;J);K)
⊢ (Kan_sigma_filler(A;B) I alpha J x i bx alpha f)
= (Kan_sigma_filler(A;B) K f(alpha) map(f;J) (f x) i A-open-box-image(X;Σ Kan-type(A) Kan-type(B);I;K;f;alpha;bx))
∈ Σ Kan-type(A) Kan-type(B)(f(alpha))

---

Latex:

---

Latex:
\mforall{}X:CubicalSet.  \mforall{}A:\{X  \mvdash{}  \_(Kan)\}.  \mforall{}B:\{X.Kan-type(A)  \mvdash{}  \_(Kan)\}.
    uniform-Kan-A-filler(X;\mSigma{}  Kan-type(A)  Kan-type(B);Kan\_sigma\_filler(A;B))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  (Assert  map(f;J)  \mmember{}  nameset(K)  List  BY
                          ((GenConcl  \mkleeneopen{}J  =  L\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  (Assert  \mkleeneopen{}f  \mmember{}  \{x:Cname|  (x  \mmember{}  J)\}    {}\mrightarrow{}  nameset(K)\mkleeneclose{}\mcdot{}  THENM  Auto)
                            THEN  (FunExt  THENA  Auto)
                            THEN  D  -1
                            THEN  DVar  `bx'
                            THEN  BLemma  `assert-isname`
                            THEN  Auto))
  THEN  (FLemma  `assert-isname`  [-2]  THENA  Auto)
  THEN  (Assert  l\_subset(Cname;map(f;J);K)  BY
                          ((GenConclTerm  \mkleeneopen{}map(f;J)\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  D  0
                            THEN  Auto
                            THEN  RepeatFor  2  (D  -1)
                            THEN  HypSubst'  (-1)  0
                            THEN  GenConclTerm  \mkleeneopen{}v[i1]\mkleeneclose{}\mcdot{}
                            THEN  Auto
                            THEN  D  -2
                            THEN  Unhide
                            THEN  Auto)))

---

Home Index