---

Step * 1 1 of Lemma equiv-bijection-equiv

.....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))
BY
{ (All (RepUR ``biject inject surject bij_inv all implies``)
   THEN D -1
   THEN Reduce 0⋅
   THEN EqCD
   THEN Auto
   THEN (FunExt THENA Auto)
   THEN Reduce 0) }

1
1. A : Type
2. B : Type
3. f : A ⟶ B
4. e2 : a1:A ⟶ a2:A ⟶ ((f a1) = (f a2) ∈ B) ⟶ (a1 = a2 ∈ A)
5. e3 : b:B ⟶ (∃a:A. ((f a) = b ∈ B))
6. a1 : A
⊢ (λa2,eq. Ax) = (e2 a1) ∈ (a2:A ⟶ ((f a1) = (f a2) ∈ B) ⟶ (a1 = a2 ∈ A))

2
1. A : Type
2. B : Type
3. f : A ⟶ B
4. e2 : a1:A ⟶ a2:A ⟶ ((f a1) = (f a2) ∈ B) ⟶ (a1 = a2 ∈ A)
5. e3 : b:B ⟶ (∃a:A. ((f a) = b ∈ B))
6. b : B
⊢ <fst((e3 b)), Ax> = (e3 b) ∈ (∃a:A. ((f a) = b ∈ B))

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  B
4.  e1  :  Bij(A;B;f)
\mvdash{}  <\mlambda{}a1,a2,eq.  Ax,  \mlambda{}b.<bij\_inv(e1)  b,  Ax>>  =  e1


By

---

Latex:
(All  (RepUR  ``biject  inject  surject  bij\_inv  all  implies``)
  THEN  D  -1
  THEN  Reduce  0\mcdot{}
  THEN  EqCD
  THEN  Auto
  THEN  (FunExt  THENA  Auto)
  THEN  Reduce  0)

---

Home Index