---

Step * 2 of Lemma discrete-equiv-iff


1. A : Type
2. B : Type
3. A ~ B
⊢ {() ⊢ _:Equiv(discr(A);discr(B))}
BY
{ (RenameVar `e' (-1) THEN UseWitness ⌜bijection-equiv(();A;B;fst(e);bij_inv(snd(e)))⌝⋅ THEN D -1 THEN Reduce 0) }

1
1. A : Type
2. B : Type
3. f : A ⟶ B
4. e1 : Bij(A;B;f)
⊢ bijection-equiv(();A;B;f;bij_inv(e1)) ∈ {() ⊢ _:Equiv(discr(A);discr(B))}

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  A  \msim{}  B
\mvdash{}  \{()  \mvdash{}  \_:Equiv(discr(A);discr(B))\}


By

---

Latex:
(RenameVar  `e'  (-1)
  THEN  UseWitness  \mkleeneopen{}bijection-equiv(();A;B;fst(e);bij\_inv(snd(e)))\mkleeneclose{}\mcdot{}
  THEN  D  -1
  THEN  Reduce  0)

---

Home Index