---

Step * 1 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))tau (IsEquiv((A)p;(E)p;q))(tau o p;q) = Σ ((A)tau ⟶ (E)tau) IsEquiv(((A)tau)p;((E)tau)p;q) ∈ {K ⊢ _}
BY
{ EqCDA }

1
.....subterm..... T:t
2:n
1. H : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ H
4. A : {H ⊢ _}
5. E : {H ⊢ _}
⊢ ((A ⟶ E))tau = (K ⊢ (A)tau ⟶ (E)tau) ∈ {K ⊢ _}

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

---

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))tau  (IsEquiv((A)p;(E)p;q))(tau  o  p;q)
=  \mSigma{}  ((A)tau  {}\mrightarrow{}  (E)tau)  IsEquiv(((A)tau)p;((E)tau)p;q)


By

---

Latex:
EqCDA

---

Home Index