---

Step * 1 1 of Lemma csm-cubical-bool

.....equality..... 
1. H : CubicalSet{j}
2. s : H j⟶ ()
3. (encode(discr(𝔹);discrete-comp(();𝔹)))s = encode((discr(𝔹))s;(discrete-comp(();𝔹))s) ∈ {H ⊢ _:c𝕌}
⊢ (discrete-comp(();𝔹))s ~ discrete-comp(();𝔹)
BY
{ (RepUR ``csm-composition discrete-comp`` 0 THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
1.  H  :  CubicalSet\{j\}
2.  s  :  H  j{}\mrightarrow{}  ()
3.  (encode(discr(\mBbbB{});discrete-comp(();\mBbbB{})))s  =  encode((discr(\mBbbB{}))s;(discrete-comp(();\mBbbB{}))s)
\mvdash{}  (discrete-comp(();\mBbbB{}))s  \msim{}  discrete-comp(();\mBbbB{})


By

---

Latex:
(RepUR  ``csm-composition  discrete-comp``  0  THEN  Auto)

---

Home Index