---

Step * of Lemma csm-transprt

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma.𝕀 ⊢ _}]. ∀[cA:Gamma.𝕀 ⊢ Compositon(A)]. ∀[a:{Gamma ⊢ _:(A)[0(𝕀)]}]. ∀[H:j⊢]. ∀[s:H j⟶ Gamma].
  ((transprt(Gamma;cA;a))s = transprt(H;(cA)s+;(a)s) ∈ {H ⊢ _:((A)[1(𝕀)])s})
BY
{ (Auto
   THEN Unfold `transprt` 0
   THEN (InstLemma `csm-comp_term` [⌜Gamma⌝;⌜0(𝔽)⌝;⌜A⌝;⌜cA⌝;⌜discr(⋅)⌝;⌜a⌝;⌜H⌝;⌜s⌝]⋅ THENA Auto)
   THEN (RWO "csm-face-0" (-1) THENA Auto)
   THEN (RWO "csm-discrete-cubical-term" (-1) THENA Auto)
   THEN SubsumeC ⌜{H ⊢ _:((A)s+)[1(𝕀)][0(𝔽) |⟶ (discr(⋅))[1(𝕀)]]}⌝⋅
   THEN Try (Trivial)
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  Unfold  `transprt`  0
  THEN  (InstLemma  `csm-comp\_term`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}0(\mBbbF{})\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}cA\mkleeneclose{};\mkleeneopen{}discr(\mcdot{})\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "csm-face-0"  (-1)  THENA  Auto)
  THEN  (RWO  "csm-discrete-cubical-term"  (-1)  THENA  Auto)
  THEN  SubsumeC  \mkleeneopen{}\{H  \mvdash{}  \_:((A)s+)[1(\mBbbI{})][0(\mBbbF{})  |{}\mrightarrow{}  (discr(\mcdot{}))[1(\mBbbI{})]]\}\mkleeneclose{}\mcdot{}
  THEN  Try  (Trivial)
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  Auto)

---

Home Index