---

Step * of Lemma csm-term-to-pathtype

No Annotations
∀[G:j⊢]. ∀[A:{G ⊢ _}].
  ∀a:{G.𝕀 ⊢ _:(A)p}. ∀[H:j⊢]. ∀[sigma:H j⟶ G].  ((<>a)sigma = <>(a)sigma+ ∈ {H ⊢ _:Path((A)sigma)})
BY
{ (InstLemma `csm-term-to-path` [] THEN RepeatFor 5 (ParallelLast') THEN Fold `term-to-pathtype` (-1)) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. a : {G.𝕀 ⊢ _:(A)p}
4. H : CubicalSet{j}
5. sigma : H j⟶ G
6. (<>a)sigma = <>(a)sigma+ ∈ {H ⊢ _:(Path_(A)sigma ((a)sigma+)[0(𝕀)] ((a)sigma+)[1(𝕀)])}
⊢ (<>a)sigma = <>(a)sigma+ ∈ {H ⊢ _:Path((A)sigma)}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A:\{G  \mvdash{}  \_\}].    \mforall{}a:\{G.\mBbbI{}  \mvdash{}  \_:(A)p\}.  \mforall{}[H:j\mvdash{}].  \mforall{}[sigma:H  j{}\mrightarrow{}  G].    ((<>a)sigma  =  <>(a)sigma+)


By

---

Latex:
(InstLemma  `csm-term-to-path`  []  THEN  RepeatFor  5  (ParallelLast')  THEN  Fold  `term-to-pathtype`  (-1))

---

Home Index