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