---

Step * of Lemma csm-equivTerm

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _:c𝕌}]. ∀[H:j⊢]. ∀[s:H j⟶ G].  ((equivTerm(G;A;B))s = equivTerm(H;(A)s;(B)s) ∈ {H ⊢ _:c𝕌})
BY
{ ((Intros⋅
    THEN ((InstLemma `csm-ap-term_wf` [⌜parm{j}⌝;⌜parm{i'}⌝;⌜H⌝;⌜G⌝;⌜c𝕌⌝;⌜s⌝;⌜A⌝]⋅ THENA Auto)
          THEN (RWO "csm-cubical-universe" (-1) THENA Auto)
          )
    THEN (InstLemma `csm-ap-term_wf` [⌜parm{j}⌝;⌜parm{i'}⌝;⌜H⌝;⌜G⌝;⌜c𝕌⌝;⌜s⌝;⌜B⌝]⋅ THENA Auto)
    THEN (RWO "csm-cubical-universe" (-1) THENA Auto)
    THEN (Assert (Equiv(decode(A);decode(B)))s = Equiv(decode((A)s);decode((B)s)) ∈ {H ⊢ _} BY
                RWO "csm-cubical-equiv" 0
                THEN Auto))
   THEN Unfold `equivTerm` 0
   THEN (InstLemma `csm-universe-encode` [⌜G⌝;⌜Equiv(decode(A);decode(B))⌝;
         ⌜equiv-comp(G;decode(A);decode(B);compOp(A);compOp(B))⌝;⌜H⌝;⌜s⌝]⋅
         THENA Auto
         )
   THEN NthHypEqTrans (-1)
   THEN EqCDA
   THEN Try (Eq)) }

1
.....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)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G  \mvdash{}  \_:c\mBbbU{}\}].  \mforall{}[H:j\mvdash{}].  \mforall{}[s:H  j{}\mrightarrow{}  G].    ((equivTerm(G;A;B))s  =  equivTerm(H;(A)s;(B)s))


By

---

Latex:
((Intros\mcdot{}
    THEN  ((InstLemma  `csm-ap-term\_wf`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}c\mBbbU{}\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  (RWO  "csm-cubical-universe"  (-1)  THENA  Auto)
                )
    THEN  (InstLemma  `csm-ap-term\_wf`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}c\mBbbU{}\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)
    THEN  (RWO  "csm-cubical-universe"  (-1)  THENA  Auto)
    THEN  (Assert  (Equiv(decode(A);decode(B)))s  =  Equiv(decode((A)s);decode((B)s))  BY
                            RWO  "csm-cubical-equiv"  0
                            THEN  Auto))
  THEN  Unfold  `equivTerm`  0
  THEN  (InstLemma  `csm-universe-encode`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}Equiv(decode(A);decode(B))\mkleeneclose{};
              \mkleeneopen{}equiv-comp(G;decode(A);decode(B);compOp(A);compOp(B))\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  NthHypEqTrans  (-1)
  THEN  EqCDA
  THEN  Try  (Eq))

---

Home Index