---

Step * of Lemma path-restriction

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}].
  cubical-type-restriction(X;Path(A);I,a1,p.((p I 1 0) = a(a1) ∈ A(a1)) ∧ ((p I 1 1) = b(a1) ∈ A(a1)))
BY
{ Intros }

1
1. [X] : CubicalSet{j}
2. [A] : {X ⊢ _}
3. [a] : {X ⊢ _:A}
4. [b] : {X ⊢ _:A}
⊢ cubical-type-restriction(X;Path(A);I,a1,p.((p I 1 0) = a(a1) ∈ A(a1)) ∧ ((p I 1 1) = b(a1) ∈ A(a1)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[a,b:\{X  \mvdash{}  \_:A\}].
    cubical-type-restriction(X;Path(A);I,a1,p.((p  I  1  0)  =  a(a1))  \mwedge{}  ((p  I  1  1)  =  b(a1)))


By

---

Latex:
Intros

---

Home Index