---

Step * 1 1 of Lemma csm-equiv-comp

.....assertion..... 
1. H : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ H
4. A : {H ⊢ _}
5. E : {H ⊢ _}
6. cA : H ⊢ CompOp(A)
7. cE : H ⊢ CompOp(E)
⊢ K ⊢ CompOp((Equiv(A;E))tau) = K ⊢ CompOp(Equiv((A)tau;(E)tau)) ∈ 𝕌{[i'' | j'']}
BY
{ (EqCDA THEN InstLemma `csm-cubical-equiv` [⌜H⌝;⌜K⌝;⌜tau⌝;⌜A⌝;⌜E⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  H  :  CubicalSet\{j\}
2.  K  :  CubicalSet\{j\}
3.  tau  :  K  j{}\mrightarrow{}  H
4.  A  :  \{H  \mvdash{}  \_\}
5.  E  :  \{H  \mvdash{}  \_\}
6.  cA  :  H  \mvdash{}  CompOp(A)
7.  cE  :  H  \mvdash{}  CompOp(E)
\mvdash{}  K  \mvdash{}  CompOp((Equiv(A;E))tau)  =  K  \mvdash{}  CompOp(Equiv((A)tau;(E)tau))


By

---

Latex:
(EqCDA  THEN  InstLemma  `csm-cubical-equiv`  [\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}tau\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}E\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index