---

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


1. [Gamma] : CubicalSet{j}
2. [K] : CubicalSet{j}
3. [s] : K j⟶ Gamma
4. [A] : {Gamma ⊢ _}
5. [phi] : {Gamma ⊢ _:𝔽}
6. Gamma, phi ⊢ A
⊢ ∀[t:{Gamma, phi ⊢ _:A}]. ∀[v:{Gamma ⊢ _:A[phi |⟶ t]}].  ((v)s ∈ {K ⊢ _:(A)s[(phi)s |⟶ (t)s]})
BY
{ (Intros THEN (MemTypeCD THENL [Auto; Id; (EqualityIsType1 THEN Auto)])) }

1
.....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}

2
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]}
9. a : {K ⊢ _:(A)s}
⊢ a ∈ {K, (phi)s ⊢ _:(A)s}

---

Latex:

---

Latex:

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
\mvdash{}  \mforall{}[t:\{Gamma,  phi  \mvdash{}  \_:A\}].  \mforall{}[v:\{Gamma  \mvdash{}  \_:A[phi  |{}\mrightarrow{}  t]\}].    ((v)s  \mmember{}  \{K  \mvdash{}  \_:(A)s[(phi)s  |{}\mrightarrow{}  (t)s]\})


By

---

Latex:
(Intros  THEN  (MemTypeCD  THENL  [Auto;  Id;  (EqualityIsType1  THEN  Auto)]))

---

Home Index