---

Step * of Lemma csm-cubical-equiv

No Annotations
∀[H,K:j⊢]. ∀[tau:K j⟶ H]. ∀[A,E:{H ⊢ _}].  ((Equiv(A;E))tau = Equiv((A)tau;(E)tau) ∈ {K ⊢ _})
BY
{ (Intros THEN Unfold `cubical-equiv` 0) }

1
1. H : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ H
4. A : {H ⊢ _}
5. E : {H ⊢ _}
⊢ (Σ (A ⟶ E) IsEquiv((A)p;(E)p;q))tau = Σ ((A)tau ⟶ (E)tau) IsEquiv(((A)tau)p;((E)tau)p;q) ∈ {K ⊢ _}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H,K:j\mvdash{}].  \mforall{}[tau:K  j{}\mrightarrow{}  H].  \mforall{}[A,E:\{H  \mvdash{}  \_\}].    ((Equiv(A;E))tau  =  Equiv((A)tau;(E)tau))


By

---

Latex:
(Intros  THEN  Unfold  `cubical-equiv`  0)

---

Home Index