---

Step * of Lemma equiv-bijection-is_wf

No Annotations
∀[A,B:Type]. ∀[e:{() ⊢ _:Equiv(discr(A);discr(B))}].  (equiv-bijection-is(e) ∈ Bij(A;B;equiv-bijection(e)))
BY
{ (Intros
   THEN (Unfold `equiv-bijection` 0 THEN Auto)
   THEN (InstLemma `equiv-contr_wf` [⌜()⌝;⌜discr(B)⌝;⌜discr(A)⌝;⌜e⌝]⋅ THENA Auto)
   THEN RepUR ``equiv-bijection-is biject inject surject`` 0
   THEN RepeatFor 2 ((MemCD THEN Try ((At ⌜Type⌝ (D 0)⋅ THEN Trivial))))) }

1
.....subterm..... T:t
1:n
1. A : Type
2. B : Type
3. e : {() ⊢ _:Equiv(discr(A);discr(B))}
4. ∀[a:{() ⊢ _:discr(B)}]. (equiv-contr(e;a) ∈ {() ⊢ _:Contractible(Fiber(equiv-fun(e);a))})
5. a1 : A
⊢ λa2,eq. Ax ∈ ∀a2:A. (((discrete-fun(equiv-fun(e))(⋅) a1) = (discrete-fun(equiv-fun(e))(⋅) a2) ∈ B) ⇒ (a1 = a2 ∈ A))

2
.....subterm..... T:t
1:n
1. A : Type
2. B : Type
3. e : {() ⊢ _:Equiv(discr(A);discr(B))}
4. ∀[a:{() ⊢ _:discr(B)}]. (equiv-contr(e;a) ∈ {() ⊢ _:Contractible(Fiber(equiv-fun(e);a))})
5. b : B
⊢ <equiv-contr(e;discr(b)).1.1(⋅), Ax> ∈ ∃a:A. ((discrete-fun(equiv-fun(e))(⋅) a) = b ∈ B)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B:Type].  \mforall{}[e:\{()  \mvdash{}  \_:Equiv(discr(A);discr(B))\}].
    (equiv-bijection-is(e)  \mmember{}  Bij(A;B;equiv-bijection(e)))


By

---

Latex:
(Intros
  THEN  (Unfold  `equiv-bijection`  0  THEN  Auto)
  THEN  (InstLemma  `equiv-contr\_wf`  [\mkleeneopen{}()\mkleeneclose{};\mkleeneopen{}discr(B)\mkleeneclose{};\mkleeneopen{}discr(A)\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``equiv-bijection-is  biject  inject  surject``  0
  THEN  RepeatFor  2  ((MemCD  THEN  Try  ((At  \mkleeneopen{}Type\mkleeneclose{}  (D  0)\mcdot{}  THEN  Trivial)))))

---

Home Index