---

Step * 1 of Lemma equiv-bijection-equiv


1. A : Type
2. B : Type
3. e : A ~ B
⊢ <λu.((fst(e)) u), λa1,a2,eq. Ax, λb.<bij_inv(snd(e)) b, Ax>> = e ∈ A ~ B
BY
{ ((All (RepUR  ``equipollent``) THEN D -1) THEN Reduce 0 THEN EqCD THEN Auto) }

1
.....subterm..... T:t
2:n
1. A : Type
2. B : Type
3. f : A ⟶ B
4. e1 : Bij(A;B;f)
⊢ <λa1,a2,eq. Ax, λb.<bij_inv(e1) b, Ax>> = e1 ∈ Bij(A;B;λu.(f u))

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  e  :  A  \msim{}  B
\mvdash{}  <\mlambda{}u.((fst(e))  u),  \mlambda{}a1,a2,eq.  Ax,  \mlambda{}b.<bij\_inv(snd(e))  b,  Ax>>  =  e


By

---

Latex:
((All  (RepUR    ``equipollent``)  THEN  D  -1)  THEN  Reduce  0  THEN  EqCD  THEN  Auto)

---

Home Index