---

Step * of Lemma csm-path-ap-q_wf

No Annotations
∀[G:j⊢]. ∀[phi:{G ⊢ _:𝔽}]. ∀[H:j⊢]. ∀[s:H j⟶ G]. ∀[B:{G ⊢ _}]. ∀[a,b:{G, phi ⊢ _:B}]. ∀[t:{G, phi ⊢ _:(Path_B a b)}].
  (csm-path-ap-q(H;G;s;t) ∈ {H.𝕀, ((phi)p)s+ ⊢ _:((B)p)s+})
BY
{ (Intros
   THEN Unfold `csm-path-ap-q` 0
   THEN Unhide
   THEN (GenConcl ⌜(t)p = xx ∈ {G.𝕀, (phi)p ⊢ _:((Path_B a b))p}⌝⋅ THENA Auto)
   THEN (Assert ((phi)p)s+ ∈ {H.𝕀 ⊢ _:𝔽} BY
               (SubsumeC ⌜{H.𝕀 ⊢ _:(𝔽)s+}⌝⋅ THEN Auto))
   THEN GenConcl ⌜(xx)s+ = yy ∈ {H.𝕀, ((phi)p)s+ ⊢ _:(((Path_B a b))p)s+}⌝⋅) }

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

2
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+}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[phi:\{G  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[H:j\mvdash{}].  \mforall{}[s:H  j{}\mrightarrow{}  G].  \mforall{}[B:\{G  \mvdash{}  \_\}].  \mforall{}[a,b:\{G,  phi  \mvdash{}  \_:B\}].
\mforall{}[t:\{G,  phi  \mvdash{}  \_:(Path\_B  a  b)\}].
    (csm-path-ap-q(H;G;s;t)  \mmember{}  \{H.\mBbbI{},  ((phi)p)s+  \mvdash{}  \_:((B)p)s+\})


By

---

Latex:
(Intros
  THEN  Unfold  `csm-path-ap-q`  0
  THEN  Unhide
  THEN  (GenConcl  \mkleeneopen{}(t)p  =  xx\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Assert  ((phi)p)s+  \mmember{}  \{H.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}  BY
                          (SubsumeC  \mkleeneopen{}\{H.\mBbbI{}  \mvdash{}  \_:(\mBbbF{})s+\}\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  GenConcl  \mkleeneopen{}(xx)s+  =  yy\mkleeneclose{}\mcdot{})

---

Home Index