---

Step * 1 of Lemma csm-equiv-comp


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))
BY
{ (Assert ⌜K ⊢ CompOp((Equiv(A;E))tau) = K ⊢ CompOp(Equiv((A)tau;(E)tau)) ∈ 𝕌{[i'' | j'']}⌝⋅
THENM ((InstLemma `csm-comp-fun-to-comp-op` [⌜H⌝;⌜K⌝;⌜tau⌝;⌜Equiv(A;E)⌝;
        ⌜equiv_comp(H;A;E;cop-to-cfun(cA);cop-to-cfun(cE))⌝]⋅
        THENA Auto
        )
       THEN NthHypEqGen (-1)
       THEN EqCDA
       THEN Try (Eq))
) }

1
.....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'']}

2
.....subterm..... T:t
1:n
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)
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']}

3
.....subterm..... T:t
3:n
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)
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)
⊢ 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)))
= 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)tau;(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{}  \_\}
6.  cA  :  H  \mvdash{}  CompOp(A)
7.  cE  :  H  \mvdash{}  CompOp(E)
\mvdash{}  (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)))


By

---

Latex:
(Assert  \mkleeneopen{}K  \mvdash{}  CompOp((Equiv(A;E))tau)  =  K  \mvdash{}  CompOp(Equiv((A)tau;(E)tau))\mkleeneclose{}\mcdot{}
THENM  ((InstLemma  `csm-comp-fun-to-comp-op`  [\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}tau\mkleeneclose{};\mkleeneopen{}Equiv(A;E)\mkleeneclose{};
                \mkleeneopen{}equiv\_comp(H;A;E;cop-to-cfun(cA);cop-to-cfun(cE))\mkleeneclose{}]\mcdot{}
                THENA  Auto
                )
              THEN  NthHypEqGen  (-1)
              THEN  EqCDA
              THEN  Try  (Eq))
)

---

Home Index