---

Step * 3 of Lemma cubical-nerve_wf

.....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
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
1.  X  :  SmallCategory
2.  XF  :  X:L:(Cname  List)  {}\mrightarrow{}  Type  \mtimes{}  (I:(Cname  List)
                                                                      {}\mrightarrow{}  J:(Cname  List)
                                                                      {}\mrightarrow{}  name-morph(I;J)
                                                                      {}\mrightarrow{}  (X  I)
                                                                      {}\mrightarrow{}  (X  J))
\mvdash{}  let  X,F  =  XF 
    in  (\mforall{}I,J,K:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}g:name-morph(J;K).
                ((F  I  K  (f  o  g))  =  ((F  J  K  g)  o  (F  I  J  f))))
          \mwedge{}  (\mforall{}I:Cname  List.  ((F  I  I  1)  =  (\mlambda{}x.x)))  \mmember{}  Type


By

---

Latex:
Auto

---

Home Index