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