---

Step * of Lemma trans-equiv-path_wf

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _:c𝕌}]. ∀[f:{G ⊢ _:Equiv(decode(A);decode(B))}].
  (trans-equiv-path(G;A;B;f) ∈ {G ⊢ _:(decode(A) ⟶ 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`` 0) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. f : {G ⊢ _:Equiv(decode(A);decode(B))}
5. G ⊢ decode(A)
6. (A)p ∈ {G.decode(A) ⊢ _:c𝕌}
7. G ⊢ decode(B)
8. (B)p ∈ {G.decode(A) ⊢ _:c𝕌}
9. G ⊢ Equiv(decode(A);decode(B))
10. G.decode(A) ⊢ Equiv((decode(A))p;(decode(B))p)
11. (f)p ∈ {G.decode(A) ⊢ _:Equiv((decode(A))p;(decode(B))p)}
12. q ∈ {G.decode(A) ⊢ _:(decode(A))p}
⊢ cubical-lam(G;transprt-const(G.decode(A);(CompFun(B))p;transprt-const(G.decode(A);(CompFun(B))p;app(equiv-fun((f)p);
                                                                                                      q))))
  ∈ {G ⊢ _:(decode(A) ⟶ 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))\}].
    (trans-equiv-path(G;A;B;f)  \mmember{}  \{G  \mvdash{}  \_:(decode(A)  {}\mrightarrow{}  decode(B))\})


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``  0)

---

Home Index