---

Step * 1 1 of Lemma csm-equivTerm


1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. H : CubicalSet{j}
5. s : H j⟶ G
6. (A)s ∈ {H ⊢ _:c𝕌}
7. (B)s ∈ {H ⊢ _:c𝕌}
8. (Equiv(decode(A);decode(B)))s = Equiv(decode((A)s);decode((B)s)) ∈ {H ⊢ _}
9. (encode(Equiv(decode(A);decode(B));equiv-comp(G;decode(A);decode(B);compOp(A);compOp(B))))s
= encode((Equiv(decode(A);decode(B)))s;(equiv-comp(G;decode(A);decode(B);compOp(A);compOp(B)))s)
∈ {H ⊢ _:c𝕌}
10. (equiv-comp(G;decode(A);decode(B);compOp(A);compOp(B)))s
= equiv-comp(H;(decode(A))s;(decode(B))s;(compOp(A))s;(compOp(B))s)
∈ H ⊢ CompOp(Equiv((decode(A))s;(decode(B))s))
⊢ (equiv-comp(G;decode(A);decode(B);compOp(A);compOp(B)))s
= equiv-comp(H;decode((A)s);decode((B)s);compOp((A)s);compOp((B)s))
∈ H ⊢ CompOp((Equiv(decode(A);decode(B)))s)
BY
{ (Enough to prove H ⊢ CompOp((Equiv(decode(A);decode(B)))s)
   = H ⊢ CompOp(Equiv((decode(A))s;(decode(B))s))
   ∈ 𝕌{[i' | j']}
    Because (NthHypEqGen (-2) THEN EqCD THEN Auto)) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. H : CubicalSet{j}
5. s : H j⟶ G
6. (A)s ∈ {H ⊢ _:c𝕌}
7. (B)s ∈ {H ⊢ _:c𝕌}
8. (Equiv(decode(A);decode(B)))s = Equiv(decode((A)s);decode((B)s)) ∈ {H ⊢ _}
9. (encode(Equiv(decode(A);decode(B));equiv-comp(G;decode(A);decode(B);compOp(A);compOp(B))))s
= encode((Equiv(decode(A);decode(B)))s;(equiv-comp(G;decode(A);decode(B);compOp(A);compOp(B)))s)
∈ {H ⊢ _:c𝕌}
10. (equiv-comp(G;decode(A);decode(B);compOp(A);compOp(B)))s
= equiv-comp(H;(decode(A))s;(decode(B))s;(compOp(A))s;(compOp(B))s)
∈ H ⊢ CompOp(Equiv((decode(A))s;(decode(B))s))
⊢ H ⊢ CompOp((Equiv(decode(A);decode(B)))s) = H ⊢ CompOp(Equiv((decode(A))s;(decode(B))s)) ∈ 𝕌{[i' | j']}

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  A  :  \{G  \mvdash{}  \_:c\mBbbU{}\}
3.  B  :  \{G  \mvdash{}  \_:c\mBbbU{}\}
4.  H  :  CubicalSet\{j\}
5.  s  :  H  j{}\mrightarrow{}  G
6.  (A)s  \mmember{}  \{H  \mvdash{}  \_:c\mBbbU{}\}
7.  (B)s  \mmember{}  \{H  \mvdash{}  \_:c\mBbbU{}\}
8.  (Equiv(decode(A);decode(B)))s  =  Equiv(decode((A)s);decode((B)s))
9.  (encode(Equiv(decode(A);decode(B));equiv-comp(G;decode(A);decode(B);compOp(A);compOp(B))))s
=  encode((Equiv(decode(A);decode(B)))s;(equiv-comp(G;decode(A);decode(B);compOp(A);compOp(B)))s)
10.  (equiv-comp(G;decode(A);decode(B);compOp(A);compOp(B)))s
=  equiv-comp(H;(decode(A))s;(decode(B))s;(compOp(A))s;(compOp(B))s)
\mvdash{}  (equiv-comp(G;decode(A);decode(B);compOp(A);compOp(B)))s
=  equiv-comp(H;decode((A)s);decode((B)s);compOp((A)s);compOp((B)s))


By

---

Latex:
(Enough  to  prove  H  \mvdash{}  CompOp((Equiv(decode(A);decode(B)))s)
  =  H  \mvdash{}  CompOp(Equiv((decode(A))s;(decode(B))s))
    Because  (NthHypEqGen  (-2)  THEN  EqCD  THEN  Auto))

---

Home Index