---

Step * 1 of Lemma csm-cubical-equiv


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 ⊢ _}
BY
{ (RWO "csm-cubical-sigma" 0 THEN Auto) }

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

---

Latex:

---

Latex:

1.  H  :  CubicalSet\{j\}
2.  K  :  CubicalSet\{j\}
3.  tau  :  K  j{}\mrightarrow{}  H
4.  A  :  \{H  \mvdash{}  \_\}
5.  E  :  \{H  \mvdash{}  \_\}
\mvdash{}  (\mSigma{}  (A  {}\mrightarrow{}  E)  IsEquiv((A)p;(E)p;q))tau  =  \mSigma{}  ((A)tau  {}\mrightarrow{}  (E)tau)  IsEquiv(((A)tau)p;((E)tau)p;q)


By

---

Latex:
(RWO  "csm-cubical-sigma"  0  THEN  Auto)

---

Home Index