---

Step * 2 of Lemma cubical-nerve_wf


1. X : SmallCategory
⊢ (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
     ((λF.functor-comp(poset-functor(I;K;(f o g));F))
     = ((λF.functor-comp(poset-functor(J;K;g);F)) o (λF.functor-comp(poset-functor(I;J;f);F)))
     ∈ (Functor(poset-cat(I);X) ⟶ Functor(poset-cat(K);X))))
∧ (∀I:Cname List
     ((λF.functor-comp(poset-functor(I;I;1);F)) = (λx.x) ∈ (Functor(poset-cat(I);X) ⟶ Functor(poset-cat(I);X))))
BY
{ Auto }

---

Latex:

---

Latex:

1.  X  :  SmallCategory
\mvdash{}  (\mforall{}I,J,K:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}g:name-morph(J;K).
          ((\mlambda{}F.functor-comp(poset-functor(I;K;(f  o  g));F))
          =  ((\mlambda{}F.functor-comp(poset-functor(J;K;g);F))  o  (\mlambda{}F.functor-comp(poset-functor(I;J;f);F)))))
\mwedge{}  (\mforall{}I:Cname  List.  ((\mlambda{}F.functor-comp(poset-functor(I;I;1);F))  =  (\mlambda{}x.x)))


By

---

Latex:
Auto

---

Home Index