---

Step * 3 of Lemma csm-comp-structure_wf

.....wf..... 
1. Gamma : CubicalSet{j}
2. Delta : CubicalSet{j}
3. tau : Delta j⟶ Gamma
4. A : {Gamma ⊢ _}
5. cA : composition-function{j:l,i:l}(Gamma;A)
6. uniform-comp-function{j:l, i:l}(Gamma; A; cA)
7. comp : composition-function{j:l,i:l}(Delta;(A)tau)
⊢ istype(uniform-comp-function{j:l, i:l}(Delta; (A)tau; comp))
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
1.  Gamma  :  CubicalSet\{j\}
2.  Delta  :  CubicalSet\{j\}
3.  tau  :  Delta  j{}\mrightarrow{}  Gamma
4.  A  :  \{Gamma  \mvdash{}  \_\}
5.  cA  :  composition-function\{j:l,i:l\}(Gamma;A)
6.  uniform-comp-function\{j:l,  i:l\}(Gamma;  A;  cA)
7.  comp  :  composition-function\{j:l,i:l\}(Delta;(A)tau)
\mvdash{}  istype(uniform-comp-function\{j:l,  i:l\}(Delta;  (A)tau;  comp))


By

---

Latex:
Auto

---

Home Index