Step * of Lemma csm-cubical-bool

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

1
1. CubicalSet{j}
2. 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