---

Step * 1 of Lemma cubical-nerve_wf


1. X : SmallCategory
⊢ <λJ.Functor(poset-cat(J);X), λI,J,f,F. functor-comp(poset-functor(I;J;f);F)> ∈ X:L:(Cname List) ⟶ Type × (I:(Cname Li\000Cst)
                                                                                                    ⟶ J:(Cname List)
                                                                                                    ⟶ name-morph(I;J)
                                                                                                    ⟶ (X I)
                                                                                                    ⟶ (X J))
BY
{ (MemCD THEN Reduce 0) }

1
.....subterm..... T:t
1:n
1. X : SmallCategory
⊢ λJ.Functor(poset-cat(J);X) ∈ L:(Cname List) ⟶ Type

2
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)

3
.....eq aux..... 
1. X : SmallCategory
2. X1 : L:(Cname List) ⟶ Type
⊢ I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X1 I) ⟶ (X1 J) ∈ Type

---

Latex:

---

Latex:

1.  X  :  SmallCategory
\mvdash{}  <\mlambda{}J.Functor(poset-cat(J);X),  \mlambda{}I,J,f,F.  functor-comp(poset-functor(I;J;f);F)>  \mmember{}  X:L:(Cname  List)  {}\mrightarrow{}\000C  Type
    \mtimes{}  (I:(Cname  List)  {}\mrightarrow{}  J:(Cname  List)  {}\mrightarrow{}  name-morph(I;J)  {}\mrightarrow{}  (X  I)  {}\mrightarrow{}  (X  J))


By

---

Latex:
(MemCD  THEN  Reduce  0)

---

Home Index