---

Step * of Lemma is-cubical-equiv-at

No Annotations
∀[X:j⊢]. ∀[T:{X ⊢ _}]. ∀[A,w,I,rho:Top].
  (IsEquiv(T;A;w)(rho) ~ {eqv:J:fset(ℕ)
                          ⟶ f:J ⟶ I
                          ⟶ u:A(f(rho))
                          ⟶ (u1:u1:T((p)(f(rho);u)) × (Path_((A)p)p (q)p app(((w)p)p; q))(((f(rho);u);u1))
                             × cubical-pi-family(X.A.Fiber((w)p;q);(Fiber((w)p;q))p;(Path_((Fiber((w)p;q))p)p (q)p
                                                                                          q);J;((f(rho);u);u1)))| 
                          ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A(f(rho)).
                            ((eqv J f u (f(rho);u) g)
                            = (eqv K f ⋅ g (u f(rho) g))
                            ∈ (u1:u1:T((p)g((f(rho);u))) × (Path_((A)p)p (q)p app(((w)p)p; q))((g((f(rho);u));u1))
                              × cubical-pi-family(X.A.Fiber((w)p;q);(Fiber((w)p;q))p;(Path_((Fiber((w)p;q))p)p (q)p
                                                                                           q);K;(g((f(rho);u));u1))))} )
BY
{ (Auto
   THEN RepUR ``is-cubical-equiv cubical-pi`` 0
   THEN RW (AddrC [1] UnfoldTopAbC) 0
   THEN RWW  "contractible-type-at cubical-fiber-at csm-ap-type-at" 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[T:\{X  \mvdash{}  \_\}].  \mforall{}[A,w,I,rho:Top].
    (IsEquiv(T;A;w)(rho)  \msim{}  \{eqv:J:fset(\mBbbN{})
                                                    {}\mrightarrow{}  f:J  {}\mrightarrow{}  I
                                                    {}\mrightarrow{}  u:A(f(rho))
                                                    {}\mrightarrow{}  (u1:u1:T((p)(f(rho);u))
                                                          \mtimes{}  (Path\_((A)p)p  (q)p  app(((w)p)p;  q))(((f(rho);u);u1))
                                                          \mtimes{}  cubical-pi-family(X.A.Fiber((w)p;q);(Fiber((w)p;q))
                                                                                                                                        p;(Path\_((Fiber((w)p;q))p)p  (q)p
                                                                                                                                                        q);J;((f(rho);u);u1)))| 
                                                    \mforall{}J,K:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}g:K  {}\mrightarrow{}  J.  \mforall{}u:A(f(rho)).
                                                        ((eqv  J  f  u  (f(rho);u)  g)  =  (eqv  K  f  \mcdot{}  g  (u  f(rho)  g)))\}  )


By

---

Latex:
(Auto
  THEN  RepUR  ``is-cubical-equiv  cubical-pi``  0
  THEN  RW  (AddrC  [1]  UnfoldTopAbC)  0
  THEN  RWW    "contractible-type-at  cubical-fiber-at  csm-ap-type-at"  0
  THEN  Auto)

---

Home Index