---

Step * of Lemma cubical-nerve_wf

∀[X:SmallCategory]. (cubical-nerve(X) ∈ CubicalSet)
BY
{ (Intro THEN Unfold `cubical-nerve` 0 THEN MemTypeCD THEN Reduce 0) }

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

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

3
.....wf..... 
1. X : SmallCategory
2. XF : X:L:(Cname List) ⟶ Type × (I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X I) ⟶ (X J))
⊢ let X,F = XF 
  in (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
        ((F I K (f o g)) = ((F J K g) o (F I J f)) ∈ ((X I) ⟶ (X K))))
     ∧ (∀I:Cname List. ((F I I 1) = (λx.x) ∈ ((X I) ⟶ (X I)))) ∈ Type

---

Latex:

---

Latex:
\mforall{}[X:SmallCategory].  (cubical-nerve(X)  \mmember{}  CubicalSet)


By

---

Latex:
(Intro  THEN  Unfold  `cubical-nerve`  0  THEN  MemTypeCD  THEN  Reduce  0)

---

Home Index