---

Step * 2 1 of Lemma groupoid-nerve-filler-uniform


1. G : Groupoid
2. True
3. I : Cname List
4. J : nameset(I) List
5. x : nameset(I)
6. i : ℕ2
7. bx : open_box(cubical-nerve(cat(G));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. ¬↑null(J)
⊢ f(groupoid-nerve-filler(G;I;J;x;i;bx))
= groupoid-nerve-filler(G;K;map(f;J);f x;i;open_box_image(cubical-nerve(cat(G));I;K;f;bx))
∈ cubical-nerve(cat(G))(K)
BY
{ ((RWO "cubical-nerve-I-cube" 0 THENA Auto)
   THEN Reduce 0
   THEN ((Assert f ∈ nameset(J) ⟶ nameset(K) BY
                ((FunExt THENA Auto)
                 THEN D -1
                 THEN OnMaybeHyp 11 (\h. ((InstHyp [⌜x1⌝] h⋅ THENA Auto)
                                          THEN Try ((FLemma `assert-isname` [-1] THEN Auto))
                                          THEN OnVar `x1' (\h. (D h+1 THEN D h+2 THEN HypSubst' (h+3) 0 THEN Auto) )
                                          ⋅))))
         THEN (Assert map(f;J) ∈ nameset(K) List BY
                     ((GenConcl ⌜J = L ∈ (nameset(J) List)⌝⋅ THENA (Unfold `nameset` 0 THEN Auto)) THEN Auto))
         THEN (Assert f x ∈ nameset(K) BY
                     (Thin (-2) THEN OnMaybeHyp 12 (\h. (FLemma `assert-isname` [h] THEN Auto)))))
   THEN Assert ⌜nameset([x / J]) ⊆r name-morph-domain(f;I)⌝⋅) }

1
.....assertion..... 
1. G : Groupoid
2. True
3. I : Cname List
4. J : nameset(I) List
5. x : nameset(I)
6. i : ℕ2
7. bx : open_box(cubical-nerve(cat(G));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. ¬↑null(J)
13. f ∈ nameset(J) ⟶ nameset(K)
14. map(f;J) ∈ nameset(K) List
15. f x ∈ nameset(K)
⊢ nameset([x / J]) ⊆r name-morph-domain(f;I)

2
1. G : Groupoid
2. True
3. I : Cname List
4. J : nameset(I) List
5. x : nameset(I)
6. i : ℕ2
7. bx : open_box(cubical-nerve(cat(G));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. ¬↑null(J)
13. f ∈ nameset(J) ⟶ nameset(K)
14. map(f;J) ∈ nameset(K) List
15. f x ∈ nameset(K)
16. nameset([x / J]) ⊆r name-morph-domain(f;I)
⊢ f(groupoid-nerve-filler(G;I;J;x;i;bx))
= groupoid-nerve-filler(G;K;map(f;J);f x;i;open_box_image(cubical-nerve(cat(G));I;K;f;bx))
∈ Functor(poset-cat(K);cat(G))

---

Latex:

---

Latex:

1.  G  :  Groupoid
2.  True
3.  I  :  Cname  List
4.  J  :  nameset(I)  List
5.  x  :  nameset(I)
6.  i  :  \mBbbN{}2
7.  bx  :  open\_box(cubical-nerve(cat(G));I;J;x;i)
8.  K  :  Cname  List
9.  f  :  name-morph(I;K)
10.  \mforall{}i:nameset(I).  ((i  \mmember{}  J)  {}\mRightarrow{}  (\muparrow{}isname(f  i)))
11.  \muparrow{}isname(f  x)
12.  \mneg{}\muparrow{}null(J)
\mvdash{}  f(groupoid-nerve-filler(G;I;J;x;i;bx))
=  groupoid-nerve-filler(G;K;map(f;J);f  x;i;open\_box\_image(cubical-nerve(cat(G));I;K;f;bx))


By

---

Latex:
((RWO  "cubical-nerve-I-cube"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  ((Assert  f  \mmember{}  nameset(J)  {}\mrightarrow{}  nameset(K)  BY
                            ((FunExt  THENA  Auto)
                              THEN  D  -1
                              THEN  OnMaybeHyp  11  (\mbackslash{}h.  ((InstHyp  [\mkleeneopen{}x1\mkleeneclose{}]  h\mcdot{}  THENA  Auto)
                                                                                THEN  Try  ((FLemma  `assert-isname`  [-1]  THEN  Auto))
                                                                                THEN  OnVar  `x1'  (\mbackslash{}h.  (D  h+1
                                                                                                                            THEN  D  h+2
                                                                                                                            THEN  HypSubst'  (h+3)  0
                                                                                                                            THEN  Auto)  )\mcdot{}))))
              THEN  (Assert  map(f;J)  \mmember{}  nameset(K)  List  BY
                                      ((GenConcl  \mkleeneopen{}J  =  L\mkleeneclose{}\mcdot{}  THENA  (Unfold  `nameset`  0  THEN  Auto))  THEN  Auto))
              THEN  (Assert  f  x  \mmember{}  nameset(K)  BY
                                      (Thin  (-2)  THEN  OnMaybeHyp  12  (\mbackslash{}h.  (FLemma  `assert-isname`  [h]  THEN  Auto)))))
  THEN  Assert  \mkleeneopen{}nameset([x  /  J])  \msubseteq{}r  name-morph-domain(f;I)\mkleeneclose{}\mcdot{})

---

Home Index