---

Step * of Lemma csm-constrained-cubical-term

No Annotations
∀[Gamma,K:j⊢]. ∀[s:K j⟶ Gamma]. ∀[A:{Gamma ⊢ _}]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[t:{Gamma, phi ⊢ _:A}].
∀[v:{Gamma ⊢ _:A[phi |⟶ t]}].
  ((v)s ∈ {K ⊢ _:(A)s[(phi)s |⟶ (t)s]})
BY
{ (RepeatFor 5 (Intro) THEN Assert ⌜Gamma, phi ⊢ A⌝⋅) }

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

2
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]})

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma,K:j\mvdash{}].  \mforall{}[s:K  j{}\mrightarrow{}  Gamma].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \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:
(RepeatFor  5  (Intro)  THEN  Assert  \mkleeneopen{}Gamma,  phi  \mvdash{}  A\mkleeneclose{}\mcdot{})

---

Home Index