---

Step * of Lemma csm-transprt-const

No Annotations
∀[G:j⊢]. ∀[A:{G ⊢ _}]. ∀[cA:G +⊢ Compositon(A)]. ∀[a:{G ⊢ _:A}]. ∀[H:j⊢]. ∀[s:H j⟶ G].
  ((transprt-const(G;cA;a))s = transprt-const(H;(cA)s;(a)s) ∈ {H ⊢ _:(A)s})
BY
{ (Auto
   THEN (InstLemmaIJ `csm-transprt` [⌜G⌝;⌜(A)p⌝;⌜(cA)p⌝]⋅ THENA Auto)
   THEN (Subst' ((A)p)[0(𝕀)] ~ (A)1(G) -1 THENA (CsmUnfolding THEN Auto))
   THEN (Subst' ((A)p)[1(𝕀)] ~ (A)1(G) -1 THENA (CsmUnfolding THEN Auto))
   THEN (InstHyp [⌜a⌝;⌜H⌝;⌜s⌝] (-1)⋅ THENA Auto)
   THEN Thin (-2)
   THEN Unfold `transprt-const` 0) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. cA : G +⊢ Compositon(A)
4. a : {G ⊢ _:A}
5. H : CubicalSet{j}
6. s : H j⟶ G
7. (transprt(G;(cA)p;a))s = transprt(H;((cA)p)s+;(a)s) ∈ {H ⊢ _:((A)1(G))s}
⊢ (transprt(G;(cA)p;a))s = transprt(H;((cA)s)p;(a)s) ∈ {H ⊢ _:(A)s}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A:\{G  \mvdash{}  \_\}].  \mforall{}[cA:G  +\mvdash{}  Compositon(A)].  \mforall{}[a:\{G  \mvdash{}  \_:A\}].  \mforall{}[H:j\mvdash{}].  \mforall{}[s:H  j{}\mrightarrow{}  G].
    ((transprt-const(G;cA;a))s  =  transprt-const(H;(cA)s;(a)s))


By

---

Latex:
(Auto
  THEN  (InstLemmaIJ  `csm-transprt`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}(A)p\mkleeneclose{};\mkleeneopen{}(cA)p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Subst'  ((A)p)[0(\mBbbI{})]  \msim{}  (A)1(G)  -1  THENA  (CsmUnfolding  THEN  Auto))
  THEN  (Subst'  ((A)p)[1(\mBbbI{})]  \msim{}  (A)1(G)  -1  THENA  (CsmUnfolding  THEN  Auto))
  THEN  (InstHyp  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  Thin  (-2)
  THEN  Unfold  `transprt-const`  0)

---

Home Index