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