---

Step * of Lemma csm-cubical-bool

No Annotations
∀[H:j⊢]. ∀[s:H j⟶ ()].  ((Bool)s = Bool ∈ {H ⊢ _:c𝕌})
BY
{ (Unfold `cubical-bool` 0 THEN Auto) }

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H:j\mvdash{}].  \mforall{}[s:H  j{}\mrightarrow{}  ()].    ((Bool)s  =  Bool)


By

---

Latex:
(Unfold  `cubical-bool`  0  THEN  Auto)

---

Home Index