---

Step * 1 of Lemma csm-constrained-cubical-term

.....assertion..... 
1. [Gamma] : CubicalSet{j}
2. [K] : CubicalSet{j}
3. [s] : K j⟶ Gamma
4. [A] : {Gamma ⊢ _}
5. [phi] : {Gamma ⊢ _:𝔽}
⊢ Gamma, phi ⊢ A
BY
{ Auto }

---

Latex:

---

Latex:
.....assertion..... 
1.  [Gamma]  :  CubicalSet\{j\}
2.  [K]  :  CubicalSet\{j\}
3.  [s]  :  K  j{}\mrightarrow{}  Gamma
4.  [A]  :  \{Gamma  \mvdash{}  \_\}
5.  [phi]  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
\mvdash{}  Gamma,  phi  \mvdash{}  A


By

---

Latex:
Auto

---

Home Index