---

Step * 2 of Lemma csm-path-ap-q_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.𝕀 ⊢ _:𝔽}
12. yy : {H.𝕀, ((phi)p)s+ ⊢ _:(((Path_B a b))p)s+}
13. (xx)s+ = yy ∈ {H.𝕀, ((phi)p)s+ ⊢ _:(((Path_B a b))p)s+}
⊢ yy @ q ∈ {H.𝕀, ((phi)p)s+ ⊢ _:((B)p)s+}
BY
{ InstLemma  `cubical-path-app_wf` [⌜H.𝕀, ((phi)p)s+⌝;⌜((B)p)s+⌝;⌜((a)p)s+⌝;⌜((b)p)s+⌝;⌜yy⌝;⌜q⌝]⋅ }

1
.....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.𝕀 ⊢ _:𝔽}
12. yy : {H.𝕀, ((phi)p)s+ ⊢ _:(((Path_B a b))p)s+}
13. (xx)s+ = yy ∈ {H.𝕀, ((phi)p)s+ ⊢ _:(((Path_B a b))p)s+}
⊢ H.𝕀, ((phi)p)s+ j⊢

2
.....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.𝕀 ⊢ _:𝔽}
12. yy : {H.𝕀, ((phi)p)s+ ⊢ _:(((Path_B a b))p)s+}
13. (xx)s+ = yy ∈ {H.𝕀, ((phi)p)s+ ⊢ _:(((Path_B a b))p)s+}
⊢ H.𝕀, ((phi)p)s+ ⊢ ((B)p)s+

3
.....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.𝕀 ⊢ _:𝔽}
12. yy : {H.𝕀, ((phi)p)s+ ⊢ _:(((Path_B a b))p)s+}
13. (xx)s+ = yy ∈ {H.𝕀, ((phi)p)s+ ⊢ _:(((Path_B a b))p)s+}
⊢ ((a)p)s+ ∈ {H.𝕀, ((phi)p)s+ ⊢ _:((B)p)s+}

4
.....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.𝕀 ⊢ _:𝔽}
12. yy : {H.𝕀, ((phi)p)s+ ⊢ _:(((Path_B a b))p)s+}
13. (xx)s+ = yy ∈ {H.𝕀, ((phi)p)s+ ⊢ _:(((Path_B a b))p)s+}
⊢ ((b)p)s+ ∈ {H.𝕀, ((phi)p)s+ ⊢ _:((B)p)s+}

5
.....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.𝕀 ⊢ _:𝔽}
12. yy : {H.𝕀, ((phi)p)s+ ⊢ _:(((Path_B a b))p)s+}
13. (xx)s+ = yy ∈ {H.𝕀, ((phi)p)s+ ⊢ _:(((Path_B a b))p)s+}
⊢ yy ∈ {H.𝕀, ((phi)p)s+ ⊢ _:(Path_((B)p)s+ ((a)p)s+ ((b)p)s+)}

6
.....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.𝕀 ⊢ _:𝔽}
12. yy : {H.𝕀, ((phi)p)s+ ⊢ _:(((Path_B a b))p)s+}
13. (xx)s+ = yy ∈ {H.𝕀, ((phi)p)s+ ⊢ _:(((Path_B a b))p)s+}
⊢ q ∈ {H.𝕀, ((phi)p)s+ ⊢ _:𝕀}

7
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.𝕀 ⊢ _:𝔽}
12. yy : {H.𝕀, ((phi)p)s+ ⊢ _:(((Path_B a b))p)s+}
13. (xx)s+ = yy ∈ {H.𝕀, ((phi)p)s+ ⊢ _:(((Path_B a b))p)s+}
14. yy @ q ∈ {H.𝕀, ((phi)p)s+ ⊢ _:((B)p)s+}
⊢ yy @ q ∈ {H.𝕀, ((phi)p)s+ ⊢ _:((B)p)s+}

---

Latex:

---

Latex:

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{}\}
12.  yy  :  \{H.\mBbbI{},  ((phi)p)s+  \mvdash{}  \_:(((Path\_B  a  b))p)s+\}
13.  (xx)s+  =  yy
\mvdash{}  yy  @  q  \mmember{}  \{H.\mBbbI{},  ((phi)p)s+  \mvdash{}  \_:((B)p)s+\}


By

---

Latex:
InstLemma    `cubical-path-app\_wf`  [\mkleeneopen{}H.\mBbbI{},  ((phi)p)s+\mkleeneclose{};\mkleeneopen{}((B)p)s+\mkleeneclose{};\mkleeneopen{}((a)p)s+\mkleeneclose{};\mkleeneopen{}((b)p)s+\mkleeneclose{};\mkleeneopen{}yy\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}

---

Home Index