Step * 1 2 of Lemma csm-equiv-comp

.....subterm..... T:t
1:n
1. CubicalSet{j}
2. CubicalSet{j}
3. tau j⟶ H
4. {H ⊢ _}
5. {H ⊢ _}
6. cA H ⊢ CompOp(A)
7. cE H ⊢ CompOp(E)
8. K ⊢ CompOp((Equiv(A;E))tau) K ⊢ CompOp(Equiv((A)tau;(E)tau)) ∈ 𝕌{[i'' j'']}
9. (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;E))tau;(equiv_comp(H;A;E;cop-to-cfun(cA);cop-to-cfun(cE)))tau)
∈ K ⊢ CompOp((Equiv(A;E))tau)
⊢ K ⊢ CompOp(Equiv((A)tau;(E)tau)) K ⊢ CompOp((Equiv(A;E))tau) ∈ 𝕌{[i' j']}
BY
EqCDA }

1
.....subterm..... T:t
2:n
1. CubicalSet{j}
2. CubicalSet{j}
3. tau j⟶ H
4. {H ⊢ _}
5. {H ⊢ _}
6. cA H ⊢ CompOp(A)
7. cE H ⊢ CompOp(E)
8. K ⊢ CompOp((Equiv(A;E))tau) K ⊢ CompOp(Equiv((A)tau;(E)tau)) ∈ 𝕌{[i'' j'']}
9. (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;E))tau;(equiv_comp(H;A;E;cop-to-cfun(cA);cop-to-cfun(cE)))tau)
∈ K ⊢ CompOp((Equiv(A;E))tau)
⊢ Equiv((A)tau;(E)tau) (Equiv(A;E))tau ∈ cubical-type{[j i]:l}(K)


Latex:


Latex:
.....subterm.....  T:t
1:n
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)
8.  K  \mvdash{}  CompOp((Equiv(A;E))tau)  =  K  \mvdash{}  CompOp(Equiv((A)tau;(E)tau))
9.  (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;E))tau;(equiv\_comp(H;A;E;cop-to-cfun(cA);cop-to-cfun(cE)))tau)
\mvdash{}  K  \mvdash{}  CompOp(Equiv((A)tau;(E)tau))  =  K  \mvdash{}  CompOp((Equiv(A;E))tau)


By


Latex:
EqCDA




Home Index