---

Step * 1 1 1 of Lemma groupoid-nerve-filler0_wf

.....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)
BY
{ (RepeatFor 2 (DVar `box')
   THEN Reduce 0
   THEN Try (((Assert (∃f∈[]. face-name(f) = <x, i> ∈ (nameset(I) × ℕ2)) BY
                     Complete (Auto))
              THEN D -1
              THEN Reduce (-2)
              THEN Auto))
   THEN DVar `u'
   THEN DVar `u1'
   THEN Reduce 0
   THEN (OnVar `u3' (RWO "cubical-nerve-I-cube") THENA Auto)
   THEN Subst' x = x1 ∈ Cname 0
   THEN Auto
   THEN (With ⌜0⌝ (D (-4))⋅ THENA (Reduce 0 THEN Auto))
   THEN Reduce (-1)⋅
   THEN (RW ListC (-1) THENA Auto)
   THEN D -1
   THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  C  :  SmallCategory
2.  G1  :  \{inv:x:cat-ob(C)  {}\mrightarrow{}  y:cat-ob(C)  {}\mrightarrow{}  (cat-arrow(C)  x  y)  {}\mrightarrow{}  (cat-arrow(C)  y  x)| 
                  \mforall{}x,y:cat-ob(C).  \mforall{}f:cat-arrow(C)  x  y.
                      (((cat-comp(C)  x  y  x  f  (inv  x  y  f))  =  (cat-id(C)  x))
                      \mwedge{}  ((cat-comp(C)  y  x  y  (inv  x  y  f)  f)  =  (cat-id(C)  y)))\} 
3.  I  :  Cname  List
4.  x  :  nameset(I)
5.  i  :  \mBbbN{}2
6.  box  :  open\_box(cubical-nerve(C);I;[];x;i)
7.  \mforall{}I:Cname  List.  \mforall{}x:nameset(I).    l\_subset(Cname;[x  /  I-[x]];I)
8.  \mforall{}I:Cname  List.  \mforall{}x:nameset(I).    (iota(x)  \mmember{}  name-morph(I-[x];I))
\mvdash{}  snd(snd(hd(box)))  \mmember{}  Functor(poset-cat(I-[x]);C)


By

---

Latex:
(RepeatFor  2  (DVar  `box')
  THEN  Reduce  0
  THEN  Try  (((Assert  (\mexists{}f\mmember{}[].  face-name(f)  =  <x,  i>)  BY
                                      Complete  (Auto))
                        THEN  D  -1
                        THEN  Reduce  (-2)
                        THEN  Auto))
  THEN  DVar  `u'
  THEN  DVar  `u1'
  THEN  Reduce  0
  THEN  (OnVar  `u3'  (RWO  "cubical-nerve-I-cube")  THENA  Auto)
  THEN  Subst'  x  =  x1  0
  THEN  Auto
  THEN  (With  \mkleeneopen{}0\mkleeneclose{}  (D  (-4))\mcdot{}  THENA  (Reduce  0  THEN  Auto))
  THEN  Reduce  (-1)\mcdot{}
  THEN  (RW  ListC  (-1)  THENA  Auto)
  THEN  D  -1
  THEN  Auto)

---

Home Index