---

Step * of Lemma csm-transport

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma.𝕀 ⊢ _}]. ∀[cA:Gamma.𝕀 ⊢ CompOp(A)]. ∀[a:{Gamma ⊢ _:(A)[0(𝕀)]}]. ∀[H:j⊢]. ∀[s:H j⟶ Gamma].
  ((transport(Gamma;a))s = transport(H;(a)s) ∈ {H ⊢ _:((A)[1(𝕀)])s})
BY
{ (Auto
   THEN Unfold `transport` 0
   THEN (InstLemma `composition-term-uniformity` [⌜Gamma⌝;⌜H⌝;⌜s⌝;⌜0(𝔽)⌝;⌜A⌝;⌜discr(⋅)⌝;⌜a⌝;⌜cA⌝]⋅ THENA Auto)
   THEN NthHypEqGen (-1)
   THEN EqCDA) }

1
.....subterm..... T:t
3:n
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 ⊢ CompOp(A)
4. a : {Gamma ⊢ _:(A)[0(𝕀)]}
5. H : CubicalSet{j}
6. s : H j⟶ Gamma
7. (comp cA [0(𝔽) ⊢→ discr(⋅)] a)s = comp (cA)s+ [(0(𝔽))s ⊢→ (discr(⋅))s+] (a)s ∈ {H ⊢ _:((A)[1(𝕀)])s}
⊢ comp (cA)s+ [0(𝔽) ⊢→ discr(⋅)] (a)s = comp (cA)s+ [(0(𝔽))s ⊢→ (discr(⋅))s+] (a)s ∈ {H ⊢ _:((A)[1(𝕀)])s}

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  Unfold  `transport`  0
  THEN  (InstLemma  `composition-term-uniformity`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}0(\mBbbF{})\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}discr(\mcdot{})\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}cA\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  NthHypEqGen  (-1)
  THEN  EqCDA)

---

Home Index