---

Step * 1 2 of Lemma csm-cubical-bool


1. H : CubicalSet{j}
2. s : H j⟶ ()
3. (encode(discr(𝔹);discrete-comp(();𝔹)))s = encode((discr(𝔹))s;(discrete-comp(();𝔹))s) ∈ {H ⊢ _:c𝕌}
⊢ encode(discr(𝔹);discrete-comp(();𝔹)) = encode(discr(𝔹);discrete-comp(();𝔹)) ∈ {H ⊢ _:c𝕌}
BY
{ Subst' encode(discr(𝔹);discrete-comp(();𝔹)) ~ encode(discr(𝔹);discrete-comp(H;𝔹)) 0 }

1
.....equality..... 
1. H : CubicalSet{j}
2. s : H j⟶ ()
3. (encode(discr(𝔹);discrete-comp(();𝔹)))s = encode((discr(𝔹))s;(discrete-comp(();𝔹))s) ∈ {H ⊢ _:c𝕌}
⊢ encode(discr(𝔹);discrete-comp(();𝔹)) ~ encode(discr(𝔹);discrete-comp(H;𝔹))

2
1. H : CubicalSet{j}
2. s : H j⟶ ()
3. (encode(discr(𝔹);discrete-comp(();𝔹)))s = encode((discr(𝔹))s;(discrete-comp(();𝔹))s) ∈ {H ⊢ _:c𝕌}
⊢ encode(discr(𝔹);discrete-comp(H;𝔹)) = encode(discr(𝔹);discrete-comp(();𝔹)) ∈ {H ⊢ _:c𝕌}

---

Latex:

---

Latex:

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{}  encode(discr(\mBbbB{});discrete-comp(();\mBbbB{}))  =  encode(discr(\mBbbB{});discrete-comp(();\mBbbB{}))


By

---

Latex:
Subst'  encode(discr(\mBbbB{});discrete-comp(();\mBbbB{}))  \msim{}  encode(discr(\mBbbB{});discrete-comp(H;\mBbbB{}))  0

---

Home Index