---

Step * of Lemma csm-equiv-comp

No Annotations
∀[H,K:j⊢]. ∀[tau:K j⟶ H]. ∀[A,E:{H ⊢ _}]. ∀[cA:H ⊢ CompOp(A)]. ∀[cE:H ⊢ CompOp(E)].
  ((equiv-comp(H;A;E;cA;cE))tau = equiv-comp(K;(A)tau;(E)tau;(cA)tau;(cE)tau) ∈ K ⊢ CompOp(Equiv((A)tau;(E)tau)))
BY
{ ((UnivCD THENA Auto) THEN Unfold `equiv-comp` 0) }

1
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)
⊢ (cfun-to-cop(H;Equiv(A;E);equiv_comp(H;A;E;cop-to-cfun(cA);cop-to-cfun(cE))))tau
= cfun-to-cop(K;Equiv((A)tau;(E)tau);equiv_comp(K;(A)tau;(E)tau;cop-to-cfun((cA)tau);cop-to-cfun((cE)tau)))
∈ K ⊢ CompOp(Equiv((A)tau;(E)tau))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H,K:j\mvdash{}].  \mforall{}[tau:K  j{}\mrightarrow{}  H].  \mforall{}[A,E:\{H  \mvdash{}  \_\}].  \mforall{}[cA:H  \mvdash{}  CompOp(A)].  \mforall{}[cE:H  \mvdash{}  CompOp(E)].
    ((equiv-comp(H;A;E;cA;cE))tau  =  equiv-comp(K;(A)tau;(E)tau;(cA)tau;(cE)tau))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `equiv-comp`  0)

---

Home Index