---

Step * of Lemma csm-term-to-path

No Annotations
∀[G:j⊢]. ∀[A:{G ⊢ _}].
  ∀a:{G.𝕀 ⊢ _:(A)p}
    ∀[H:j⊢]. ∀[sigma:H j⟶ G].
      ((<>(a))sigma = H ⊢ <>((a)sigma+) ∈ {H ⊢ _:(Path_(A)sigma ((a)sigma+)[0(𝕀)] ((a)sigma+)[1(𝕀)])})
BY
{ (Intros THEN (BLemma `paths-equal` THENA Auto) THEN Try ((RWO "csm-interval-type" 0 THEN Auto))) }

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

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

3
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. a : {G.𝕀 ⊢ _:(A)p}
4. H : CubicalSet{j}
5. sigma : H j⟶ G
⊢ (<>(a))sigma = H ⊢ <>((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  =  H  \mvdash{}  <>((a)sigma+))


By

---

Latex:
(Intros  THEN  (BLemma  `paths-equal`  THENA  Auto)  THEN  Try  ((RWO  "csm-interval-type"  0  THEN  Auto)))

---

Home Index