Step
*
1
2
of Lemma
cubical-nerve_wf
1. X : SmallCategory
⊢ λI,J,f,F. functor-comp(poset-functor(I;J;f);F) ∈ I:(Cname List)
⟶ J:(Cname List)
⟶ name-morph(I;J)
⟶ Functor(poset-cat(I);X)
⟶ Functor(poset-cat(J);X)
BY
{ (RepeatFor 4 ((FunExt THENW Auto)) THEN Reduce 0) }
1
1. X : SmallCategory
2. I : Cname List
3. J : Cname List
4. x : name-morph(I;J)
5. x1 : Functor(poset-cat(I);X)
⊢ functor-comp(poset-functor(I;J;x);x1) ∈ Functor(poset-cat(J);X)
Latex:
Latex:
1. X : SmallCategory
\mvdash{} \mlambda{}I,J,f,F. functor-comp(poset-functor(I;J;f);F) \mmember{} I:(Cname List)
{}\mrightarrow{} J:(Cname List)
{}\mrightarrow{} name-morph(I;J)
{}\mrightarrow{} Functor(poset-cat(I);X)
{}\mrightarrow{} Functor(poset-cat(J);X)
By
Latex:
(RepeatFor 4 ((FunExt THENW Auto)) THEN Reduce 0)
Home
Index