---

Step * 1 of Lemma trans-equiv-path_wf


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))}
BY
{ (Enough to prove (CompFun(B))p ∈ composition-structure{[[i | j] | [j | i]]:l, [i | j]:l}(G.decode(A); (decode(B))p)
    Because Auto) }

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}
⊢ (CompFun(B))p ∈ composition-structure{[[i | j] | [j | i]]:l, [i | j]:l}(G.decode(A); (decode(B))p)

---

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.  G  \mvdash{}  decode(A)
6.  (A)p  \mmember{}  \{G.decode(A)  \mvdash{}  \_:c\mBbbU{}\}
7.  G  \mvdash{}  decode(B)
8.  (B)p  \mmember{}  \{G.decode(A)  \mvdash{}  \_:c\mBbbU{}\}
9.  G  \mvdash{}  Equiv(decode(A);decode(B))
10.  G.decode(A)  \mvdash{}  Equiv((decode(A))p;(decode(B))p)
11.  (f)p  \mmember{}  \{G.decode(A)  \mvdash{}  \_:Equiv((decode(A))p;(decode(B))p)\}
12.  q  \mmember{}  \{G.decode(A)  \mvdash{}  \_:(decode(A))p\}
\mvdash{}  cubical-lam(G;transprt-const(G.decode(A);(CompFun(B))p;transprt-const(G.decode(A);(...)p;app(...;
                                                                                                                                                                                              q))))
    \mmember{}  \{G  \mvdash{}  \_:(decode(A)  {}\mrightarrow{}  decode(B))\}


By

---

Latex:
(Enough  to  prove  (CompFun(B))p  \mmember{}  composition-structure\{[[i  |  j]  |  [j  |  i]]:l,  [i  |  j]:l\}
                                                                      (G.decode(A);  (decode(B))p)
    Because  Auto)

---

Home Index