---

Step * 2 of Lemma groupoid-nerve-functor-flip

.....wf..... 
1. G : Groupoid
2. I : Cname List
3. u : nameset(I)
4. K : Cname List
5. f : name-morph(I;K)
6. f1 : name-morph(K;[])
7. x1 : nameset(I)
8. F : Functor(poset-cat(I-[x1]);cat(G))
⊢ istype((↑isname(f u)) ∧ ((f1 (f u)) = 0 ∈ ℕ2))
BY
{ (D 0 THEN Try (FLemma `assert-isname` [-1]) THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  G  :  Groupoid
2.  I  :  Cname  List
3.  u  :  nameset(I)
4.  K  :  Cname  List
5.  f  :  name-morph(I;K)
6.  f1  :  name-morph(K;[])
7.  x1  :  nameset(I)
8.  F  :  Functor(poset-cat(I-[x1]);cat(G))
\mvdash{}  istype((\muparrow{}isname(f  u))  \mwedge{}  ((f1  (f  u))  =  0))


By

---

Latex:
(D  0  THEN  Try  (FLemma  `assert-isname`  [-1])  THEN  Auto)

---

Home Index