---

Step * of Lemma path-type_wf

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}].  X ⊢ (Path_A a b)
BY
{ (Intros THEN Unfold `path-type` 0 THEN MemCD THEN Try (Complete (Auto))) }

1
.....subterm..... T:t
2:n
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : fset(ℕ)
6. alpha : X(I)
7. p : Path(A)(alpha)
⊢ ((p I 1 0) = a(alpha) ∈ A(alpha)) ∧ ((p I 1 1) = b(alpha) ∈ A(alpha)) ∈ ℙ

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[a,b:\{X  \mvdash{}  \_:A\}].    X  \mvdash{}  (Path\_A  a  b)


By

---

Latex:
(Intros  THEN  Unfold  `path-type`  0  THEN  MemCD  THEN  Try  (Complete  (Auto)))

---

Home Index