---

Step * 1 of Lemma csm-cubical-pi-typed


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 ⊢ _}
BY
{ (RepeatFor 2 (Unfolds ``csm-dependent typed-cc-fst typed-cc-snd`` 0) THEN BLemma `csm-cubical-pi` THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  Delta  :  CubicalSet\{j\}
3.  A  :  \{X  \mvdash{}  \_\}
4.  B  :  \{X.A  \mvdash{}  \_\}
5.  s  :  Delta  ij{}\mrightarrow{}  X
6.  Delta.(A)s  \mvdash{}  (B)(s)dep
\mvdash{}  (\mPi{}A  B)s  =  Delta  \mvdash{}  \mPi{}(A)s  (B)(s)dep


By

---

Latex:
(RepeatFor  2  (Unfolds  ``csm-dependent  typed-cc-fst  typed-cc-snd``  0)
  THEN  BLemma  `csm-cubical-pi`
  THEN  Auto)

---

Home Index