---

Step * 1 of Lemma app-trans-equiv-path


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)}
BY
{ (GenConcl ⌜app(equiv-fun((f)p); q) = b ∈ {G.decode(A) ⊢ _:(decode(B))p}⌝⋅ THENA 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)
15. b : {G.decode(A) ⊢ _:(decode(B))p}
16. app(equiv-fun((f)p); q) = b ∈ {G.decode(A) ⊢ _:(decode(B))p}
⊢ app((λtransprt-const(G.decode(A);(CompFun(B))p;transprt-const(G.decode(A);(CompFun(B))p;b))); a)
= transprt-const(G;CompFun(B);transprt-const(G;CompFun(B);app(equiv-fun(f); a)))
∈ {G ⊢ _:decode(B)}

---

Latex:

---

Latex:

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


By

---

Latex:
(GenConcl  \mkleeneopen{}app(equiv-fun((f)p);  q)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index