Step * 1 2 of Lemma csm-univ-trans


1. CubicalSet{j}
2. {G.𝕀 ⊢ _:c𝕌}
3. CubicalSet{j}
4. 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+
BY
(RepUR ``comp-op-to-comp-fun universe-comp-op csm-composition`` THEN CsmUnfoldingComp THEN Auto) }


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{}  cop-to-cfun(compOp((T)s+))  \msim{}  (cop-to-cfun(compOp(T)))s+


By


Latex:
(RepUR  ``comp-op-to-comp-fun  universe-comp-op  csm-composition``  0  THEN  CsmUnfoldingComp  THEN  Auto)




Home Index