---

Step * of Lemma app-trans-equiv-path

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _:c𝕌}]. ∀[f:{G ⊢ _:Equiv(decode(A);decode(B))}]. ∀[a:{G ⊢ _:decode(A)}].
  (app(trans-equiv-path(G;A;B;f); a)
  = transprt-const(G;CompFun(B);transprt-const(G;CompFun(B);app(equiv-fun(f); a)))
  ∈ {G ⊢ _:decode(B)})
BY
{ (Intros⋅
   THEN Unhide
   THEN ((Assert G ⊢ decode(A) BY
                Auto)
         THEN (Assert (A)p ∈ {G.decode(A) ⊢ _:c𝕌} BY
                     (BLemma `csm-ap-term-universe` THEN Auto))
         THEN (Assert G ⊢ decode(B) BY
                     Auto)
         THEN (Assert (B)p ∈ {G.decode(A) ⊢ _:c𝕌} BY
                     (BLemma `csm-ap-term-universe` THEN Auto))
         THEN (Assert G ⊢ Equiv(decode(A);decode(B)) BY
                     Auto)
         THEN (Assert G.decode(A) ⊢ Equiv((decode(A))p;(decode(B))p) BY
                     (RWO "csm-universe-decode" 0 THEN Auto)))
   THEN Unfold `trans-equiv-path` 0
   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 (Assert q ∈ {G.decode(A) ⊢ _:(decode(A))p} BY
               Auto)
   THEN RepUR ``let cubical-lam`` 0
   THEN (Assert (CompFun(B))p ∈ composition-structure{[[i | j] | [j | i]]:l, [i | j]:l}(G.decode(A); (decode(B))p) BY
               ((DoSubsume THENL [Auto; (RWO "csm-universe-decode" 0 THEN Auto)])
                THEN (MemCD THENL [Auto; (SubsumeC ⌜{G.decode(A) ⊢ _}⌝⋅ THEN Auto)])
                ))) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. f : {G ⊢ _:Equiv(decode(A);decode(B))}
5. a : {G ⊢ _:decode(A)}
6. G ⊢ decode(A)
7. (A)p ∈ {G.decode(A) ⊢ _:c𝕌}
8. G ⊢ decode(B)
9. (B)p ∈ {G.decode(A) ⊢ _:c𝕌}
10. G ⊢ Equiv(decode(A);decode(B))
11. G.decode(A) ⊢ Equiv((decode(A))p;(decode(B))p)
12. (f)p ∈ {G.decode(A) ⊢ _:Equiv((decode(A))p;(decode(B))p)}
13. q ∈ {G.decode(A) ⊢ _:(decode(A))p}
14. (CompFun(B))p ∈ composition-structure{[[i | j] | [j | i]]:l, [i | j]:l}(G.decode(A); (decode(B))p)
⊢ app((λtransprt-const(G.decode(A);(CompFun(B))p;transprt-const(G.decode(A);(CompFun(B))p;app(equiv-fun((f)p); q)))); a)
= transprt-const(G;CompFun(B);transprt-const(G;CompFun(B);app(equiv-fun(f); a)))
∈ {G ⊢ _:decode(B)}

---

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{}[a:\{G  \mvdash{}  \_:decode(A)\}].
    (app(trans-equiv-path(G;A;B;f);  a)
    =  transprt-const(G;CompFun(B);transprt-const(G;CompFun(B);app(equiv-fun(f);  a))))


By

---

Latex:
(Intros\mcdot{}
  THEN  Unhide
  THEN  ((Assert  G  \mvdash{}  decode(A)  BY
                            Auto)
              THEN  (Assert  (A)p  \mmember{}  \{G.decode(A)  \mvdash{}  \_:c\mBbbU{}\}  BY
                                      (BLemma  `csm-ap-term-universe`  THEN  Auto))
              THEN  (Assert  G  \mvdash{}  decode(B)  BY
                                      Auto)
              THEN  (Assert  (B)p  \mmember{}  \{G.decode(A)  \mvdash{}  \_:c\mBbbU{}\}  BY
                                      (BLemma  `csm-ap-term-universe`  THEN  Auto))
              THEN  (Assert  G  \mvdash{}  Equiv(decode(A);decode(B))  BY
                                      Auto)
              THEN  (Assert  G.decode(A)  \mvdash{}  Equiv((decode(A))p;(decode(B))p)  BY
                                      (RWO  "csm-universe-decode"  0  THEN  Auto)))
  THEN  Unfold  `trans-equiv-path`  0
  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  (Assert  q  \mmember{}  \{G.decode(A)  \mvdash{}  \_:(decode(A))p\}  BY
                          Auto)
  THEN  RepUR  ``let  cubical-lam``  0
  THEN  (Assert  (CompFun(B))p  \mmember{}  composition-structure\{[[i  |  j]  |  [j  |  i]]:l,  [i  |  j]:l\}(G.decode(A);
                                                                                                                                                                            (decode(B))p
                                                                                                                                                                            )  BY
                          ((DoSubsume  THENL  [Auto;  (RWO  "csm-universe-decode"  0  THEN  Auto)])
                            THEN  (MemCD  THENL  [Auto;  (SubsumeC  \mkleeneopen{}\{G.decode(A)  \mvdash{}  \_\}\mkleeneclose{}\mcdot{}  THEN  Auto)])
                            )))

---

Home Index