---

Step * 1 of Lemma equipollent-type-unit-pair


1. [T] : Type
⊢ T ~ T × Unit
BY
{ (With ⌜λx.<x, ⋅>⌝ (D 0)⋅ THEN Auto THEN RepUR ``biject surject inject`` 0 THEN D 0 THEN Auto) }

1
1. [T] : Type
2. b : T × Unit@i
⊢ ∃a:T. (<a, ⋅> = b ∈ (T × Unit))

---

Latex:

---

Latex:

1.  [T]  :  Type
\mvdash{}  T  \msim{}  T  \mtimes{}  Unit


By

---

Latex:
(With  \mkleeneopen{}\mlambda{}x.<x,  \mcdot{}>\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  RepUR  ``biject  surject  inject``  0  THEN  D  0  THEN  Auto)

---

Home Index