---

Step * 2 of Lemma equiv-bijection-is_wf

.....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)
BY
{ ((InstHyp [⌜discr(b)⌝] (-2)⋅ THENA Auto)
   THEN Unfold `contractible-type` -1
   THEN (Assert equiv-contr(e;discr(b)).1 ∈ {() ⊢ _:Fiber(equiv-fun(e);discr(b))} BY
               Auto)
   THEN Unfold `cubical-fiber` -1
   THEN (RWO  "discrete-fun-at-app<" 0 THENA Auto)) }

1
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
6. equiv-contr(e;discr(b)) ∈ {() ⊢ _:Σ Fiber(equiv-fun(e);discr(b)) Π(Fiber(equiv-fun(e);discr(b)))
                                                                      p (Path_((Fiber(equiv-fun(e);discr(b)))p)p (q)p
                                                                              q)}
7. equiv-contr(e;discr(b)).1 ∈ {() ⊢ _:Σ discr(A) (Path_(discr(B))p (discr(b))p app((equiv-fun(e))p; q))}
⊢ <equiv-contr(e;discr(b)).1.1(⋅), Ax> ∈ ∃a:A. (app(equiv-fun(e); discr(a))(⋅) = b ∈ B)

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  A  :  Type
2.  B  :  Type
3.  e  :  \{()  \mvdash{}  \_:Equiv(discr(A);discr(B))\}
4.  \mforall{}[a:\{()  \mvdash{}  \_:discr(B)\}].  (equiv-contr(e;a)  \mmember{}  \{()  \mvdash{}  \_:Contractible(Fiber(equiv-fun(e);a))\})
5.  b  :  B
\mvdash{}  <equiv-contr(e;discr(b)).1.1(\mcdot{}),  Ax>  \mmember{}  \mexists{}a:A.  ((discrete-fun(equiv-fun(e))(\mcdot{})  a)  =  b)


By

---

Latex:
((InstHyp  [\mkleeneopen{}discr(b)\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  Unfold  `contractible-type`  -1
  THEN  (Assert  equiv-contr(e;discr(b)).1  \mmember{}  \{()  \mvdash{}  \_:Fiber(equiv-fun(e);discr(b))\}  BY
                          Auto)
  THEN  Unfold  `cubical-fiber`  -1
  THEN  (RWO    "discrete-fun-at-app<"  0  THENA  Auto))

---

Home Index