---

Step * of Lemma csm-is-cubical-equiv

No Annotations
∀[X:j⊢]. ∀[T,A:{X ⊢ _}]. ∀[w:{X ⊢ _:(T ⟶ A)}]. ∀[Z:j⊢]. ∀[s:Z j⟶ X].
  ((IsEquiv(T;A;w))s = IsEquiv((T)s;(A)s;(w)s) ∈ {Z ⊢ _})
BY
{ (Auto THEN Unfold `is-cubical-equiv` 0 THEN (RWO "csm-cubical-pi" 0 THENA Auto) THEN Try ((EqCD THEN Auto))) }

1
.....subterm..... T:t
3:n
1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. A : {X ⊢ _}
4. w : {X ⊢ _:(T ⟶ A)}
5. Z : CubicalSet{j}
6. s : Z j⟶ X
⊢ (Contractible(Fiber((w)p;q)))(s o p;q) = Z.(A)s ⊢ Contractible(Fiber(((w)s)p;q)) ∈ {Z.(A)s ⊢ _}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[T,A:\{X  \mvdash{}  \_\}].  \mforall{}[w:\{X  \mvdash{}  \_:(T  {}\mrightarrow{}  A)\}].  \mforall{}[Z:j\mvdash{}].  \mforall{}[s:Z  j{}\mrightarrow{}  X].
    ((IsEquiv(T;A;w))s  =  IsEquiv((T)s;(A)s;(w)s))


By

---

Latex:
(Auto
  THEN  Unfold  `is-cubical-equiv`  0
  THEN  (RWO  "csm-cubical-pi"  0  THENA  Auto)
  THEN  Try  ((EqCD  THEN  Auto)))

---

Home Index