---

Step * of Lemma uniform-Kan-filler_wf

∀[X:CubicalSet]. ∀[filler:I:(Cname List) ⟶ J:(nameset(I) List) ⟶ x:nameset(I) ⟶ i:ℕ2 ⟶ open_box(X;I;J;x;i) ⟶ X(I)].
  (uniform-Kan-filler(X;filler) ∈ ℙ)
BY
{ (Auto
   THEN Unfold `uniform-Kan-filler` 0
   THEN RepeatFor 2 ((RepeatFor 5 (MemCD) THEN Try (QuickAuto)))
   THEN (FLemma `assert-isname` [-1] THENA Auto)
   THEN (Assert ⌜(nameset([x / J]) ⊆r name-morph-domain(f;I)) ∧ (map(f;J) ∈ nameset(K) List)⌝⋅ THENM Auto)) }

1
.....assertion..... 
1. X : CubicalSet
2. filler : I:(Cname List) ⟶ J:(nameset(I) List) ⟶ x:nameset(I) ⟶ i:ℕ2 ⟶ open_box(X;I;J;x;i) ⟶ X(I)
3. I : Cname List
4. J : nameset(I) List
5. x : nameset(I)
6. i : ℕ2
7. bx : open_box(X;I;J;x;i)
8. K : Cname List
9. f : name-morph(I;K)
10. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
11. ↑isname(f x)
12. f x ∈ nameset(K)
⊢ (nameset([x / J]) ⊆r name-morph-domain(f;I)) ∧ (map(f;J) ∈ nameset(K) List)

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[filler:I:(Cname  List)
                                                    {}\mrightarrow{}  J:(nameset(I)  List)
                                                    {}\mrightarrow{}  x:nameset(I)
                                                    {}\mrightarrow{}  i:\mBbbN{}2
                                                    {}\mrightarrow{}  open\_box(X;I;J;x;i)
                                                    {}\mrightarrow{}  X(I)].
    (uniform-Kan-filler(X;filler)  \mmember{}  \mBbbP{})


By

---

Latex:
(Auto
  THEN  Unfold  `uniform-Kan-filler`  0
  THEN  RepeatFor  2  ((RepeatFor  5  (MemCD)  THEN  Try  (QuickAuto)))
  THEN  (FLemma  `assert-isname`  [-1]  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}(nameset([x  /  J])  \msubseteq{}r  name-morph-domain(f;I))  \mwedge{}  (map(f;J)  \mmember{}  nameset(K)  List)\mkleeneclose{}\mcdot{}
  THENM  Auto
  ))

---

Home Index