---

Step * of Lemma csm-univ-trans

No Annotations
∀[G:j⊢]. ∀[T:{G.𝕀 ⊢ _:c𝕌}]. ∀[H:j⊢]. ∀[s:H j⟶ G].
  ((univ-trans(G;T))s = univ-trans(H;(T)s+) ∈ {H ⊢ _:(((decode(T))s+)[0(𝕀)] ⟶ ((decode(T))s+)[1(𝕀)])})
BY
{ (Auto
   THEN Unfold `univ-trans` 0
   THEN (InstLemma `csm-transprt-fun` [⌜G⌝;⌜decode(T)⌝;⌜cop-to-cfun(compOp(T))⌝;⌜H⌝;⌜s⌝]⋅ THENA Auto)) }

1
1. G : CubicalSet{j}
2. T : {G.𝕀 ⊢ _:c𝕌}
3. H : CubicalSet{j}
4. s : H j⟶ G
5. (transprt-fun(G;decode(T);cop-to-cfun(compOp(T))))s
= transprt-fun(H;(decode(T))s+;(cop-to-cfun(compOp(T)))s+)
∈ {H ⊢ _:(((decode(T))s+)[0(𝕀)] ⟶ ((decode(T))s+)[1(𝕀)])}
⊢ (transprt-fun(G;decode(T);cop-to-cfun(compOp(T))))s
= transprt-fun(H;decode((T)s+);cop-to-cfun(compOp((T)s+)))
∈ {H ⊢ _:(((decode(T))s+)[0(𝕀)] ⟶ ((decode(T))s+)[1(𝕀)])}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[T:\{G.\mBbbI{}  \mvdash{}  \_:c\mBbbU{}\}].  \mforall{}[H:j\mvdash{}].  \mforall{}[s:H  j{}\mrightarrow{}  G].    ((univ-trans(G;T))s  =  univ-trans(H;(T)s+))


By

---

Latex:
(Auto
  THEN  Unfold  `univ-trans`  0
  THEN  (InstLemma  `csm-transprt-fun`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}decode(T)\mkleeneclose{};\mkleeneopen{}cop-to-cfun(compOp(T))\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index