---

Step * 1 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. a1 : A
⊢ λa2,eq. Ax ∈ ∀a2:A. (((discrete-fun(equiv-fun(e))(⋅) a1) = (discrete-fun(equiv-fun(e))(⋅) a2) ∈ B) ⇒ (a1 = a2 ∈ A))
BY
{ (Auto
   THEN (RWO  "discrete-fun-at-app<" (-1) THENA Auto)
   THEN (GenConcl ⌜app(equiv-fun(e); discr(a1))(⋅) = b ∈ B⌝⋅ THENA Auto)
   THEN (InstLemma `cubical-term_wf` [⌜()⌝;⌜((Path_(discr(B))p (discr(b))p app((equiv-fun(e))p; q)))[discr(a1)]⌝]⋅
         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. a1 : A
6. a2 : A
7. eq : app(equiv-fun(e); discr(a1))(⋅) = app(equiv-fun(e); discr(a2))(⋅) ∈ B
8. b : B
9. app(equiv-fun(e); discr(a1))(⋅) = b ∈ B
10. {() ⊢ _:((Path_(discr(B))p (discr(b))p app((equiv-fun(e))p; q)))[discr(a1)]} ∈ 𝕌{[i | j']}
⊢ a1 = a2 ∈ A

---

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.  a1  :  A
\mvdash{}  \mlambda{}a2,eq.  Ax  \mmember{}  \mforall{}a2:A
                      (((discrete-fun(equiv-fun(e))(\mcdot{})  a1)  =  (discrete-fun(equiv-fun(e))(\mcdot{})  a2))  {}\mRightarrow{}  (a1  =  a2))


By

---

Latex:
(Auto
  THEN  (RWO    "discrete-fun-at-app<"  (-1)  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}app(equiv-fun(e);  discr(a1))(\mcdot{})  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `cubical-term\_wf`  [\mkleeneopen{}()\mkleeneclose{};\mkleeneopen{}((Path\_(discr(B))p  (discr(b))p  app((equiv-fun(e))p;  q)))
                                                                                      [discr(a1)]\mkleeneclose{}]\mcdot{}
              THENA  Auto
              ))

---

Home Index