---

Step * 1 of Lemma csm-path-ap-q_wf

.....wf..... 
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. H : CubicalSet{j}
4. s : H j⟶ G
5. B : {G ⊢ _}
6. a : {G, phi ⊢ _:B}
7. b : {G, phi ⊢ _:B}
8. t : {G, phi ⊢ _:(Path_B a b)}
9. xx : {G.𝕀, (phi)p ⊢ _:((Path_B a b))p}
10. (t)p = xx ∈ {G.𝕀, (phi)p ⊢ _:((Path_B a b))p}
11. ((phi)p)s+ ∈ {H.𝕀 ⊢ _:𝔽}
⊢ (xx)s+ ∈ {H.𝕀, ((phi)p)s+ ⊢ _:(((Path_B a b))p)s+}
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
1.  G  :  CubicalSet\{j\}
2.  phi  :  \{G  \mvdash{}  \_:\mBbbF{}\}
3.  H  :  CubicalSet\{j\}
4.  s  :  H  j{}\mrightarrow{}  G
5.  B  :  \{G  \mvdash{}  \_\}
6.  a  :  \{G,  phi  \mvdash{}  \_:B\}
7.  b  :  \{G,  phi  \mvdash{}  \_:B\}
8.  t  :  \{G,  phi  \mvdash{}  \_:(Path\_B  a  b)\}
9.  xx  :  \{G.\mBbbI{},  (phi)p  \mvdash{}  \_:((Path\_B  a  b))p\}
10.  (t)p  =  xx
11.  ((phi)p)s+  \mmember{}  \{H.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}
\mvdash{}  (xx)s+  \mmember{}  \{H.\mBbbI{},  ((phi)p)s+  \mvdash{}  \_:(((Path\_B  a  b))p)s+\}


By

---

Latex:
Auto

---

Home Index