---

Step * of Lemma csm-trans-equiv-path

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _:c𝕌}]. ∀[f:{G ⊢ _:Equiv(decode(A);decode(B))}]. ∀[H:j⊢]. ∀[s:H j⟶ G].
  ((trans-equiv-path(G;A;B;f))s = trans-equiv-path(H;(A)s;(B)s;(f)s) ∈ {H ⊢ _:(decode((A)s) ⟶ decode((B)s))})
BY
{ ((Intros⋅
    THEN (Assert (A)s ∈ {H ⊢ _:c𝕌} BY
                (BLemma `csm-ap-term-universe` THENA Auto))
    THEN (Assert (B)s ∈ {H ⊢ _:c𝕌} BY
                (BLemma `csm-ap-term-universe` THENA Auto)))
   THEN (Assert G ⊢ Equiv(decode(A);decode(B)) BY
               Auto)
   THEN (((Assert G ⊢ decode(A) BY Auto) THEN (Assert G ⊢ decode(B) BY Auto))
         THEN (Assert (f)p ∈ {G.decode(A) ⊢ _:Equiv((decode(A))p;(decode(B))p)} BY
                     ((Assert (f)p ∈ {G.decode(A) ⊢ _:(Equiv(decode(A);decode(B)))p} BY
                             Auto)
                      THEN (InferEqualTypeGen THEN Try (Trivial))
                      THEN EqCDA
                      THEN Auto))
         )
   THEN Unfold `trans-equiv-path` 0
   THEN (Assert q ∈ {G.decode(A) ⊢ _:(decode(A))p} BY
               Auto)) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. f : {G ⊢ _:Equiv(decode(A);decode(B))}
5. H : CubicalSet{j}
6. s : H j⟶ G
7. (A)s ∈ {H ⊢ _:c𝕌}
8. (B)s ∈ {H ⊢ _:c𝕌}
9. G ⊢ Equiv(decode(A);decode(B))
10. G ⊢ decode(A)
11. G ⊢ decode(B)
12. (f)p ∈ {G.decode(A) ⊢ _:Equiv((decode(A))p;(decode(B))p)}
13. q ∈ {G.decode(A) ⊢ _:(decode(A))p}
⊢ (let tr = λb.transprt-const(G.decode(A);(CompFun(B))p;b) in
    let b = app(equiv-fun((f)p); q) in
    cubical-lam(G;tr (tr b)))s
= let tr = λb.transprt-const(H.decode((A)s);(CompFun((B)s))p;b) in
   let b = app(equiv-fun(((f)s)p); q) in
   cubical-lam(H;tr (tr b))
∈ {H ⊢ _:(decode((A)s) ⟶ decode((B)s))}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G  \mvdash{}  \_:c\mBbbU{}\}].  \mforall{}[f:\{G  \mvdash{}  \_:Equiv(decode(A);decode(B))\}].  \mforall{}[H:j\mvdash{}].  \mforall{}[s:H  j{}\mrightarrow{}  G].
    ((trans-equiv-path(G;A;B;f))s  =  trans-equiv-path(H;(A)s;(B)s;(f)s))


By

---

Latex:
((Intros\mcdot{}
    THEN  (Assert  (A)s  \mmember{}  \{H  \mvdash{}  \_:c\mBbbU{}\}  BY
                            (BLemma  `csm-ap-term-universe`  THENA  Auto))
    THEN  (Assert  (B)s  \mmember{}  \{H  \mvdash{}  \_:c\mBbbU{}\}  BY
                            (BLemma  `csm-ap-term-universe`  THENA  Auto)))
  THEN  (Assert  G  \mvdash{}  Equiv(decode(A);decode(B))  BY
                          Auto)
  THEN  (((Assert  G  \mvdash{}  decode(A)  BY  Auto)  THEN  (Assert  G  \mvdash{}  decode(B)  BY  Auto))
              THEN  (Assert  (f)p  \mmember{}  \{G.decode(A)  \mvdash{}  \_:Equiv((decode(A))p;(decode(B))p)\}  BY
                                      ((Assert  (f)p  \mmember{}  \{G.decode(A)  \mvdash{}  \_:(Equiv(decode(A);decode(B)))p\}  BY
                                                      Auto)
                                        THEN  (InferEqualTypeGen  THEN  Try  (Trivial))
                                        THEN  EqCDA
                                        THEN  Auto))
              )
  THEN  Unfold  `trans-equiv-path`  0
  THEN  (Assert  q  \mmember{}  \{G.decode(A)  \mvdash{}  \_:(decode(A))p\}  BY
                          Auto))

---

Home Index