---

Step * 1 of Lemma csm-univ-trans


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(𝕀)])}
BY
{ (NthHypSq (-1) THEN RepeatFor 2 ((EqCD THEN Try (Trivial)))) }

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(𝕀)])}
⊢ decode((T)s+) ~ (decode(T))s+

2
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(𝕀)])}
⊢ cop-to-cfun(compOp((T)s+)) ~ (cop-to-cfun(compOp(T)))s+

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  T  :  \{G.\mBbbI{}  \mvdash{}  \_:c\mBbbU{}\}
3.  H  :  CubicalSet\{j\}
4.  s  :  H  j{}\mrightarrow{}  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+)
\mvdash{}  (transprt-fun(G;decode(T);cop-to-cfun(compOp(T))))s
=  transprt-fun(H;decode((T)s+);cop-to-cfun(compOp((T)s+)))


By

---

Latex:
(NthHypSq  (-1)  THEN  RepeatFor  2  ((EqCD  THEN  Try  (Trivial))))

---

Home Index