Step * of Lemma pathtype-comp_wf

No Annotations
[G:j⊢]. ∀[A:{G ⊢ _}]. ∀[cA:G ⊢ Compositon(A)].  (pathtype-comp(G;A;cA) ∈ G ⊢ Compositon(Path(A)))
BY
(Intros THEN Assert ⌜pathtype-comp(G;A;cA) ∈ composition-function{j:l,i:l}(G;Path(A))⌝⋅}

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

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


Latex:


Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A:\{G  \mvdash{}  \_\}].  \mforall{}[cA:G  \mvdash{}  Compositon(A)].    (pathtype-comp(G;A;cA)  \mmember{}  G  \mvdash{}  Compositon(Path(A)))


By


Latex:
(Intros  THEN  Assert  \mkleeneopen{}pathtype-comp(G;A;cA)  \mmember{}  composition-function\{j:l,i:l\}(G;Path(A))\mkleeneclose{}\mcdot{})




Home Index