---

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

.....set predicate..... 
1. Gamma : CubicalSet{j}
2. K : CubicalSet{j}
3. s : K j⟶ Gamma
4. A : {Gamma ⊢ _}
5. phi : {Gamma ⊢ _:𝔽}
6. Gamma, phi ⊢ A
7. t : {Gamma, phi ⊢ _:A}
8. v : {Gamma ⊢ _:A[phi |⟶ t]}
⊢ (t)s = (v)s ∈ {K, (phi)s ⊢ _:(A)s}
BY
{ (DVar `v' THEN ApFunToHypEquands `Z' ⌜(Z)s⌝ ⌜{K, (phi)s ⊢ _:(A)s}⌝ (-1)⋅ THEN Auto) }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  Gamma  :  CubicalSet\{j\}
2.  K  :  CubicalSet\{j\}
3.  s  :  K  j{}\mrightarrow{}  Gamma
4.  A  :  \{Gamma  \mvdash{}  \_\}
5.  phi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
6.  Gamma,  phi  \mvdash{}  A
7.  t  :  \{Gamma,  phi  \mvdash{}  \_:A\}
8.  v  :  \{Gamma  \mvdash{}  \_:A[phi  |{}\mrightarrow{}  t]\}
\mvdash{}  (t)s  =  (v)s


By

---

Latex:
(DVar  `v'  THEN  ApFunToHypEquands  `Z'  \mkleeneopen{}(Z)s\mkleeneclose{}  \mkleeneopen{}\{K,  (phi)s  \mvdash{}  \_:(A)s\}\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto)

---

Home Index