---

Step * 1 1 of Lemma groupoid-nerve-filler0_wf


1. G : Groupoid
2. I : Cname List
3. x : nameset(I)
4. i : ℕ2
5. box : open_box(cubical-nerve(cat(G));I;[];x;i)
6. ∀I:Cname List. ∀x:nameset(I).  l_subset(Cname;[x / I-[x]];I)
7. ∀I:Cname List. ∀x:nameset(I).  (iota(x) ∈ name-morph(I-[x];I))
⊢ groupoid-nerve-filler0(I;x;box) ∈ Functor(poset-cat(I);cat(G))
BY
{ (Unfold `groupoid-nerve-filler0` 0
   THEN (D 1 THEN All (RepUR  ``groupoid-cat``))
   THEN (Assert ⌜snd(snd(hd(box))) ∈ Functor(poset-cat(I-[x]);C)⌝⋅ THENM Auto)) }

1
.....assertion..... 
1. C : SmallCategory
2. G1 : {inv:x:cat-ob(C) ⟶ y:cat-ob(C) ⟶ (cat-arrow(C) x y) ⟶ (cat-arrow(C) y x)| 
         ∀x,y:cat-ob(C). ∀f:cat-arrow(C) x y.
           (((cat-comp(C) x y x f (inv x y f)) = (cat-id(C) x) ∈ (cat-arrow(C) x x))
           ∧ ((cat-comp(C) y x y (inv x y f) f) = (cat-id(C) y) ∈ (cat-arrow(C) y y)))} 
3. I : Cname List
4. x : nameset(I)
5. i : ℕ2
6. box : open_box(cubical-nerve(C);I;[];x;i)
7. ∀I:Cname List. ∀x:nameset(I).  l_subset(Cname;[x / I-[x]];I)
8. ∀I:Cname List. ∀x:nameset(I).  (iota(x) ∈ name-morph(I-[x];I))
⊢ snd(snd(hd(box))) ∈ Functor(poset-cat(I-[x]);C)

---

Latex:

---

Latex:

1.  G  :  Groupoid
2.  I  :  Cname  List
3.  x  :  nameset(I)
4.  i  :  \mBbbN{}2
5.  box  :  open\_box(cubical-nerve(cat(G));I;[];x;i)
6.  \mforall{}I:Cname  List.  \mforall{}x:nameset(I).    l\_subset(Cname;[x  /  I-[x]];I)
7.  \mforall{}I:Cname  List.  \mforall{}x:nameset(I).    (iota(x)  \mmember{}  name-morph(I-[x];I))
\mvdash{}  groupoid-nerve-filler0(I;x;box)  \mmember{}  Functor(poset-cat(I);cat(G))


By

---

Latex:
(Unfold  `groupoid-nerve-filler0`  0
  THEN  (D  1  THEN  All  (RepUR    ``groupoid-cat``))
  THEN  (Assert  \mkleeneopen{}snd(snd(hd(box)))  \mmember{}  Functor(poset-cat(I-[x]);C)\mkleeneclose{}\mcdot{}  THENM  Auto))

---

Home Index