---

Step * 1 of Lemma bool-negation-equiv_wf

.....subterm..... T:t
2:n
1. bool-negation-equiv(()) ∈ {() ⊢ _:Equiv(discr(𝔹);discr(𝔹))}
⊢ discr(𝔹) = decode(Bool) ∈ {() ⊢ _}
BY
{ Unfold `cubical-bool` 0 }

1
1. bool-negation-equiv(()) ∈ {() ⊢ _:Equiv(discr(𝔹);discr(𝔹))}
⊢ discr(𝔹) = decode(encode(discr(𝔹);discrete-comp(();𝔹))) ∈ {() ⊢ _}

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  bool-negation-equiv(())  \mmember{}  \{()  \mvdash{}  \_:Equiv(discr(\mBbbB{});discr(\mBbbB{}))\}
\mvdash{}  discr(\mBbbB{})  =  decode(Bool)


By

---

Latex:
Unfold  `cubical-bool`  0

---

Home Index