---

Step * 1 of Lemma csm-ap-term-wf-subset


1. H : CubicalSet{j}
2. phi : {H ⊢ _:𝔽}
3. A : {H ⊢ _}
4. t : {H, phi ⊢ _:A}
5. K : CubicalSet{j}
6. psi : {K ⊢ _:𝔽}
7. B : {K ⊢ _}
8. tau : K j⟶ H
9. K ⊢ (psi ⇒ (phi)tau)
10. K, psi ⊢ B = (A)tau
11. (t)tau ∈ {K, (phi)tau ⊢ _:(A)tau}
12. (t)tau ∈ {K, psi ⊢ _:(A)tau}
⊢ (t)tau ∈ {K, psi ⊢ _:B}
BY
{ (InferEqualType THEN Auto) }

---

Latex:

---

Latex:

1.  H  :  CubicalSet\{j\}
2.  phi  :  \{H  \mvdash{}  \_:\mBbbF{}\}
3.  A  :  \{H  \mvdash{}  \_\}
4.  t  :  \{H,  phi  \mvdash{}  \_:A\}
5.  K  :  CubicalSet\{j\}
6.  psi  :  \{K  \mvdash{}  \_:\mBbbF{}\}
7.  B  :  \{K  \mvdash{}  \_\}
8.  tau  :  K  j{}\mrightarrow{}  H
9.  K  \mvdash{}  (psi  {}\mRightarrow{}  (phi)tau)
10.  K,  psi  \mvdash{}  B  =  (A)tau
11.  (t)tau  \mmember{}  \{K,  (phi)tau  \mvdash{}  \_:(A)tau\}
12.  (t)tau  \mmember{}  \{K,  psi  \mvdash{}  \_:(A)tau\}
\mvdash{}  (t)tau  \mmember{}  \{K,  psi  \mvdash{}  \_:B\}


By

---

Latex:
(InferEqualType  THEN  Auto)

---

Home Index