---

Step * 2 of Lemma pathtype-comp_wf


1. [G] : CubicalSet{j}
2. [A] : {G ⊢ _}
3. [cA] : G ⊢ Compositon(A)
4. pathtype-comp(G;A;cA) ∈ composition-function{j:l,i:l}(G;Path(A))
⊢ pathtype-comp(G;A;cA) ∈ G ⊢ Compositon(Path(A))
BY
{ (MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. cA : G ⊢ Compositon(A)
4. pathtype-comp(G;A;cA) ∈ composition-function{j:l,i:l}(G;Path(A))
⊢ uniform-comp-function{j:l, i:l}(G; Path(A); pathtype-comp(G;A;cA))

---

Latex:

---

Latex:

1.  [G]  :  CubicalSet\{j\}
2.  [A]  :  \{G  \mvdash{}  \_\}
3.  [cA]  :  G  \mvdash{}  Compositon(A)
4.  pathtype-comp(G;A;cA)  \mmember{}  composition-function\{j:l,i:l\}(G;Path(A))
\mvdash{}  pathtype-comp(G;A;cA)  \mmember{}  G  \mvdash{}  Compositon(Path(A))


By

---

Latex:
(MemTypeCD  THEN  Auto)

---

Home Index