---

Step * of Lemma equal-cubical-equiv-at

No Annotations
∀[X:j⊢]. ∀[T,A:{X ⊢ _}]. ∀[I:fset(ℕ)]. ∀[a:X(I)]. ∀[x:Equiv(T;A)(a)]. ∀[y:u:(T ⟶ A)(a) × IsEquiv((T)p;(A)p;q)((a;u))].
  x = y ∈ Equiv(T;A)(a) supposing x = y ∈ (u:(T ⟶ A)(a) × IsEquiv((T)p;(A)p;q)((a;u)))
BY
{ (RepeatFor 6 (Intro) THEN All  (RepUR ``cubical-equiv``)⋅ THEN (All  (RWO "cubical-sigma-at") THENA Auto) THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[T,A:\{X  \mvdash{}  \_\}].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[a:X(I)].  \mforall{}[x:Equiv(T;A)(a)].
\mforall{}[y:u:(T  {}\mrightarrow{}  A)(a)  \mtimes{}  IsEquiv((T)p;(A)p;q)((a;u))].
    x  =  y  supposing  x  =  y


By

---

Latex:
(RepeatFor  6  (Intro)
  THEN  All    (RepUR  ``cubical-equiv``)\mcdot{}
  THEN  (All    (RWO  "cubical-sigma-at")  THENA  Auto)
  THEN  Auto)

---

Home Index