---

Step * of Lemma csm-cubical-pi-typed

No Annotations
∀X,Delta:j⊢. ∀A:{X ⊢ _}. ∀B:{X.A ⊢ _}. ∀s:Delta ij⟶ X.  ((ΠA B)s = Delta ⊢ Π(A)s (B)(s)dep ∈ {Delta ⊢ _})
BY
{ (Intros THEN (Assert Delta.(A)s ⊢ (B)(s)dep BY Auto)) }

1
1. X : CubicalSet{j}
2. Delta : CubicalSet{j}
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. s : Delta ij⟶ X
6. Delta.(A)s ⊢ (B)(s)dep
⊢ (ΠA B)s = Delta ⊢ Π(A)s (B)(s)dep ∈ {Delta ⊢ _}

---

Latex:

---

Latex:
No  Annotations
\mforall{}X,Delta:j\mvdash{}.  \mforall{}A:\{X  \mvdash{}  \_\}.  \mforall{}B:\{X.A  \mvdash{}  \_\}.  \mforall{}s:Delta  ij{}\mrightarrow{}  X.    ((\mPi{}A  B)s  =  Delta  \mvdash{}  \mPi{}(A)s  (B)(s)dep)


By

---

Latex:
(Intros  THEN  (Assert  Delta.(A)s  \mvdash{}  (B)(s)dep  BY  Auto))

---

Home Index