---

Step * of Lemma csm-paths-equal

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[p:{X ⊢ _:(Path_A a b)}]. ∀[H:j⊢]. ∀[tau:H j⟶ X]. ∀[q:{H ⊢ _:(Path(A))tau}].
  (p)tau = q ∈ {H ⊢ _:((Path_A a b))tau} supposing (p)tau = q ∈ {H ⊢ _:(Path(A))tau}
BY
{ (Intros THEN Assert ⌜(p)tau = q ∈ {H ⊢ _:(Path_(A)tau (a)tau (b)tau)}⌝⋅) }

1
.....assertion..... 
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. p : {X ⊢ _:(Path_A a b)}
6. H : CubicalSet{j}
7. tau : H j⟶ X
8. q : {H ⊢ _:(Path(A))tau}
9. (p)tau = q ∈ {H ⊢ _:(Path(A))tau}
⊢ (p)tau = q ∈ {H ⊢ _:(Path_(A)tau (a)tau (b)tau)}

2
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. p : {X ⊢ _:(Path_A a b)}
6. H : CubicalSet{j}
7. tau : H j⟶ X
8. q : {H ⊢ _:(Path(A))tau}
9. (p)tau = q ∈ {H ⊢ _:(Path(A))tau}
10. (p)tau = q ∈ {H ⊢ _:(Path_(A)tau (a)tau (b)tau)}
⊢ (p)tau = q ∈ {H ⊢ _:((Path_A a b))tau}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[a,b:\{X  \mvdash{}  \_:A\}].  \mforall{}[p:\{X  \mvdash{}  \_:(Path\_A  a  b)\}].  \mforall{}[H:j\mvdash{}].  \mforall{}[tau:H  j{}\mrightarrow{}  X].
\mforall{}[q:\{H  \mvdash{}  \_:(Path(A))tau\}].
    (p)tau  =  q  supposing  (p)tau  =  q


By

---

Latex:
(Intros  THEN  Assert  \mkleeneopen{}(p)tau  =  q\mkleeneclose{}\mcdot{})

---

Home Index