---

Step * 1 1 1 1 2 2 1 1 1 5 1 1 1 1 1 3 of Lemma uabeta_wf


1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. G ⊢ decode(A)
5. (A)p ∈ {G.decode(A) ⊢ _:c𝕌}
6. G ⊢ decode(B)
7. (B)p ∈ {G.decode(A) ⊢ _:c𝕌}
8. G ⊢ Equiv(decode(A);decode(B))
9. G.decode(A) ⊢ Equiv((decode(A))p;(decode(B))p)
10. ∀[a,b:{G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((decode(B))p)p}].
      G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ (Path_((decode(B))p)p a b)
11. (q)p ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((Equiv(decode(A);decode(B)))p)p}
12. (q)p ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:Equiv(((decode(A))p)p;((decode(B))p)p)}
13. equiv-fun((q)p) ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:(((decode(A))p)p ⟶ ((decode(B))p)p)}
14. app(equiv-fun((q)p); q) ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((decode(B))p)p}
15. CompFun((A)p) ∈ G.Equiv(decode(A);decode(B)) +⊢ Compositon((decode(A))p)
16. CompFun((B)p) ∈ G.Equiv(decode(A);decode(B)) +⊢ Compositon((decode(B))p)
17. (A)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
18. (B)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
19. UA ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _
          :(Equiv(((decode(A))p)p;((decode(B))p)p) ⟶ (Path_c𝕌 ((A)p)p ((B)p)p))}
20. app(UA; (q)p) ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:(Path_c𝕌 ((A)p)p ((B)p)p)}
21. (Equiv(decode(A);decode(B)))p = Equiv(decode((A)p);decode((B)p)) ∈ {G.Equiv(decode(A);decode(B)) ⊢ _}
22. (decode(equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))[0(𝕀)]
= (decode(A))p
∈ {G.Equiv(decode(A);decode(B)) ⊢ _}
23. (decode(equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))[1(𝕀)]
= (decode(B))p
∈ {G.Equiv(decode(A);decode(B)) ⊢ _}
24. ((decode(equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))[0(𝕀)])p
= ((decode(A))p)p
∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _}
25. ((decode(equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))[1(𝕀)])p
= ((decode(B))p)p
∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _}
26. (univ-trans(G.Equiv(decode(A);decode(B));equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))p
= univ-trans(G.Equiv(decode(A);decode(B)).decode((A)p);(equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))p+)
∈ {G.Equiv(decode(A);decode(B)).decode((A)p) ⊢ _:(decode(((A)p)p) ⟶ decode(((B)p)p))}
27. app((univ-trans(G.Equiv(decode(A);decode(B));equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))p; q)
= app(univ-trans(G.Equiv(decode(A);decode(B)).decode((A)p);(equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))p+); q)
∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((decode(B))p)p}
⊢ q
= q
∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((decode(equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))[0(𝕀)])
                                                  p}
BY
{ Fold `member` 0 }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. G ⊢ decode(A)
5. (A)p ∈ {G.decode(A) ⊢ _:c𝕌}
6. G ⊢ decode(B)
7. (B)p ∈ {G.decode(A) ⊢ _:c𝕌}
8. G ⊢ Equiv(decode(A);decode(B))
9. G.decode(A) ⊢ Equiv((decode(A))p;(decode(B))p)
10. ∀[a,b:{G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((decode(B))p)p}].
      G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ (Path_((decode(B))p)p a b)
11. (q)p ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((Equiv(decode(A);decode(B)))p)p}
12. (q)p ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:Equiv(((decode(A))p)p;((decode(B))p)p)}
13. equiv-fun((q)p) ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:(((decode(A))p)p ⟶ ((decode(B))p)p)}
14. app(equiv-fun((q)p); q) ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((decode(B))p)p}
15. CompFun((A)p) ∈ G.Equiv(decode(A);decode(B)) +⊢ Compositon((decode(A))p)
16. CompFun((B)p) ∈ G.Equiv(decode(A);decode(B)) +⊢ Compositon((decode(B))p)
17. (A)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
18. (B)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
19. UA ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _
          :(Equiv(((decode(A))p)p;((decode(B))p)p) ⟶ (Path_c𝕌 ((A)p)p ((B)p)p))}
20. app(UA; (q)p) ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:(Path_c𝕌 ((A)p)p ((B)p)p)}
21. (Equiv(decode(A);decode(B)))p = Equiv(decode((A)p);decode((B)p)) ∈ {G.Equiv(decode(A);decode(B)) ⊢ _}
22. (decode(equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))[0(𝕀)]
= (decode(A))p
∈ {G.Equiv(decode(A);decode(B)) ⊢ _}
23. (decode(equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))[1(𝕀)]
= (decode(B))p
∈ {G.Equiv(decode(A);decode(B)) ⊢ _}
24. ((decode(equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))[0(𝕀)])p
= ((decode(A))p)p
∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _}
25. ((decode(equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))[1(𝕀)])p
= ((decode(B))p)p
∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _}
26. (univ-trans(G.Equiv(decode(A);decode(B));equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))p
= univ-trans(G.Equiv(decode(A);decode(B)).decode((A)p);(equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))p+)
∈ {G.Equiv(decode(A);decode(B)).decode((A)p) ⊢ _:(decode(((A)p)p) ⟶ decode(((B)p)p))}
27. app((univ-trans(G.Equiv(decode(A);decode(B));equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))p; q)
= app(univ-trans(G.Equiv(decode(A);decode(B)).decode((A)p);(equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))p+); q)
∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((decode(B))p)p}
⊢ q ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((decode(equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))
                                                       [0(𝕀)])p}

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  A  :  \{G  \mvdash{}  \_:c\mBbbU{}\}
3.  B  :  \{G  \mvdash{}  \_:c\mBbbU{}\}
4.  G  \mvdash{}  decode(A)
5.  (A)p  \mmember{}  \{G.decode(A)  \mvdash{}  \_:c\mBbbU{}\}
6.  G  \mvdash{}  decode(B)
7.  (B)p  \mmember{}  \{G.decode(A)  \mvdash{}  \_:c\mBbbU{}\}
8.  G  \mvdash{}  Equiv(decode(A);decode(B))
9.  G.decode(A)  \mvdash{}  Equiv((decode(A))p;(decode(B))p)
10.  \mforall{}[a,b:\{G.Equiv(decode(A);decode(B)).(decode(A))p  \mvdash{}  \_:((decode(B))p)p\}].
            G.Equiv(decode(A);decode(B)).(decode(A))p  \mvdash{}  (Path\_((decode(B))p)p  a  b)
11.  (q)p  \mmember{}  \{G.Equiv(decode(A);decode(B)).(decode(A))p  \mvdash{}  \_:((Equiv(decode(A);decode(B)))p)p\}
12.  (q)p  \mmember{}  \{G.Equiv(decode(A);decode(B)).(decode(A))p  \mvdash{}  \_:Equiv(((decode(A))p)p;((decode(B))p)p)\}
13.  equiv-fun((q)p)  \mmember{}  \{G.Equiv(decode(A);decode(B)).(decode(A))p  \mvdash{}  \_
                                              :(((decode(A))p)p  {}\mrightarrow{}  ((decode(B))p)p)\}
14.  app(equiv-fun((q)p);  q)  \mmember{}  \{G.Equiv(decode(A);decode(B)).(decode(A))p  \mvdash{}  \_:((decode(B))p)p\}
15.  CompFun((A)p)  \mmember{}  G.Equiv(decode(A);decode(B))  +\mvdash{}  Compositon((decode(A))p)
16.  CompFun((B)p)  \mmember{}  G.Equiv(decode(A);decode(B))  +\mvdash{}  Compositon((decode(B))p)
17.  (A)p  \mmember{}  \{G.Equiv(decode(A);decode(B))  \mvdash{}  \_:c\mBbbU{}\}
18.  (B)p  \mmember{}  \{G.Equiv(decode(A);decode(B))  \mvdash{}  \_:c\mBbbU{}\}
19.  UA  \mmember{}  \{G.Equiv(decode(A);decode(B)).(decode(A))p  \mvdash{}  \_
                    :(Equiv(((decode(A))p)p;((decode(B))p)p)  {}\mrightarrow{}  (Path\_c\mBbbU{}  ((A)p)p  ((B)p)p))\}
20.  app(UA;  (q)p)  \mmember{}  \{G.Equiv(decode(A);decode(B)).(decode(A))p  \mvdash{}  \_:(Path\_c\mBbbU{}  ((A)p)p  ((B)p)p)\}
21.  (Equiv(decode(A);decode(B)))p  =  Equiv(decode((A)p);decode((B)p))
22.  (decode(equiv\_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))[0(\mBbbI{})]  =  (decode(A))p
23.  (decode(equiv\_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))[1(\mBbbI{})]  =  (decode(B))p
24.  ((decode(equiv\_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))[0(\mBbbI{})])p  =  ((decode(A))p)p
25.  ((decode(equiv\_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))[1(\mBbbI{})])p  =  ((decode(B))p)p
26.  (univ-trans(G.Equiv(decode(A);decode(B));equiv\_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))p
=  univ-trans(G.Equiv(decode(A);decode(B)).decode((A)p);(equiv\_path(G.Equiv(...;...);(A)p;(B)p;q))p+)
27.  app((univ-trans(G.Equiv(decode(A);decode(B));equiv\_path(G.Equiv(decode(A);...);(A)p;(B)p;q)))p;
                q)
=  app(univ-trans(G.Equiv(decode(A);decode(B)).decode((A)p);(equiv\_path(G....;(A)p;(B)p;q))p+);  q)
\mvdash{}  q  =  q


By

---

Latex:
Fold  `member`  0

---

Home Index