---

Step * 1 of Lemma csm-equivTerm

.....subterm..... T:t
3:n
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𝕌}
⊢ (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
{ (InstLemma `csm-equiv-comp` [⌜G⌝;⌜H⌝;⌜s⌝;⌜decode(A)⌝;⌜decode(B)⌝;⌜compOp(A)⌝;⌜compOp(B)⌝]⋅ THENA 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))
⊢ (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)

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
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)
\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:
(InstLemma  `csm-equiv-comp`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}decode(A)\mkleeneclose{};\mkleeneopen{}decode(B)\mkleeneclose{};\mkleeneopen{}compOp(A)\mkleeneclose{};\mkleeneopen{}compOp(B)\mkleeneclose{}]\mcdot{}
  THENA  Auto
  )

---

Home Index