---

Step * 1 of Lemma csm-equiv-term

.....wf..... 
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. A : {G ⊢ _}
4. T : {G ⊢ _}
5. f : {G ⊢ _:Equiv(T;A)}
6. t : {G, phi ⊢ _:T}
7. a : {G ⊢ _:A}
8. app(equiv-fun(f); t) ∈ {G, phi ⊢ _:A}
9. c : {G, phi ⊢ _:(Path_A a app(equiv-fun(f); t))}
10. cF : G ⊢ Compositon(Fiber(equiv-fun(f);a))
11. H : CubicalSet{j}
12. s : H j⟶ G
13. e : {G ⊢ _:Contractible(Fiber(equiv-fun(f);a))}
14. equiv-contr(f;a) = e ∈ {G ⊢ _:Contractible(Fiber(equiv-fun(f);a))}
15. G ⊢ Fiber(equiv-fun(f);a)
16. fiber-point(t;c) ∈ {G, phi ⊢ _:Fiber(equiv-fun(f);a)}
17. ∀[u:{G, phi.𝕀 ⊢ _:(Fiber(equiv-fun(f);a))p}]. ∀[a0:{G ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}].
    ∀[Delta:j⊢]. ∀[s:Delta j⟶ G].
      ((comp (cF)p [phi ⊢→ u] a0)s
      = comp ((cF)p)s+ [(phi)s ⊢→ (u)s+] (a0)s
      ∈ {Delta ⊢ _:(((Fiber(equiv-fun(f);a))p)s+)[1(𝕀)][(phi)s |⟶ ((u)s+)[1(𝕀)]]})
18. contr-center(e) ∈ {G, phi ⊢ _:Fiber(equiv-fun(f);a)}
19. contr-path(e;fiber-point(t;c)) ∈ {G, phi ⊢ _:(Path_Fiber(equiv-fun(f);a) contr-center(e) fiber-point(t;c))}
⊢ (contr-path(e;fiber-point(t;c)))p @ q ∈ {G, phi.𝕀 ⊢ _:(Fiber(equiv-fun(f);a))p}
BY
{ (Assert p ∈ G, phi.𝕀 j⟶ G, phi BY
         Auto) }

1
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. A : {G ⊢ _}
4. T : {G ⊢ _}
5. f : {G ⊢ _:Equiv(T;A)}
6. t : {G, phi ⊢ _:T}
7. a : {G ⊢ _:A}
8. app(equiv-fun(f); t) ∈ {G, phi ⊢ _:A}
9. c : {G, phi ⊢ _:(Path_A a app(equiv-fun(f); t))}
10. cF : G ⊢ Compositon(Fiber(equiv-fun(f);a))
11. H : CubicalSet{j}
12. s : H j⟶ G
13. e : {G ⊢ _:Contractible(Fiber(equiv-fun(f);a))}
14. equiv-contr(f;a) = e ∈ {G ⊢ _:Contractible(Fiber(equiv-fun(f);a))}
15. G ⊢ Fiber(equiv-fun(f);a)
16. fiber-point(t;c) ∈ {G, phi ⊢ _:Fiber(equiv-fun(f);a)}
17. ∀[u:{G, phi.𝕀 ⊢ _:(Fiber(equiv-fun(f);a))p}]. ∀[a0:{G ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}].
    ∀[Delta:j⊢]. ∀[s:Delta j⟶ G].
      ((comp (cF)p [phi ⊢→ u] a0)s
      = comp ((cF)p)s+ [(phi)s ⊢→ (u)s+] (a0)s
      ∈ {Delta ⊢ _:(((Fiber(equiv-fun(f);a))p)s+)[1(𝕀)][(phi)s |⟶ ((u)s+)[1(𝕀)]]})
18. contr-center(e) ∈ {G, phi ⊢ _:Fiber(equiv-fun(f);a)}
19. contr-path(e;fiber-point(t;c)) ∈ {G, phi ⊢ _:(Path_Fiber(equiv-fun(f);a) contr-center(e) fiber-point(t;c))}
20. p ∈ G, phi.𝕀 j⟶ G, phi
⊢ (contr-path(e;fiber-point(t;c)))p @ q ∈ {G, phi.𝕀 ⊢ _:(Fiber(equiv-fun(f);a))p}

---

Latex:

---

Latex:
.....wf..... 
1.  G  :  CubicalSet\{j\}
2.  phi  :  \{G  \mvdash{}  \_:\mBbbF{}\}
3.  A  :  \{G  \mvdash{}  \_\}
4.  T  :  \{G  \mvdash{}  \_\}
5.  f  :  \{G  \mvdash{}  \_:Equiv(T;A)\}
6.  t  :  \{G,  phi  \mvdash{}  \_:T\}
7.  a  :  \{G  \mvdash{}  \_:A\}
8.  app(equiv-fun(f);  t)  \mmember{}  \{G,  phi  \mvdash{}  \_:A\}
9.  c  :  \{G,  phi  \mvdash{}  \_:(Path\_A  a  app(equiv-fun(f);  t))\}
10.  cF  :  G  \mvdash{}  Compositon(Fiber(equiv-fun(f);a))
11.  H  :  CubicalSet\{j\}
12.  s  :  H  j{}\mrightarrow{}  G
13.  e  :  \{G  \mvdash{}  \_:Contractible(Fiber(equiv-fun(f);a))\}
14.  equiv-contr(f;a)  =  e
15.  G  \mvdash{}  Fiber(equiv-fun(f);a)
16.  fiber-point(t;c)  \mmember{}  \{G,  phi  \mvdash{}  \_:Fiber(equiv-fun(f);a)\}
17.  \mforall{}[u:\{G,  phi.\mBbbI{}  \mvdash{}  \_:(Fiber(equiv-fun(f);a))p\}].
        \mforall{}[a0:\{G  \mvdash{}  \_:((Fiber(equiv-fun(f);a))p)[0(\mBbbI{})][phi  |{}\mrightarrow{}  (u)[0(\mBbbI{})]]\}].  \mforall{}[Delta:j\mvdash{}].
        \mforall{}[s:Delta  j{}\mrightarrow{}  G].
            ((comp  (cF)p  [phi  \mvdash{}\mrightarrow{}  u]  a0)s  =  comp  ((cF)p)s+  [(phi)s  \mvdash{}\mrightarrow{}  (u)s+]  (a0)s)
18.  contr-center(e)  \mmember{}  \{G,  phi  \mvdash{}  \_:Fiber(equiv-fun(f);a)\}
19.  contr-path(e;fiber-point(t;c))  \mmember{}  \{G,  phi  \mvdash{}  \_:(Path\_Fiber(equiv-fun(f);a)  contr-center(e)
                                                                                                              fiber-point(t;c))\}
\mvdash{}  (contr-path(e;fiber-point(t;c)))p  @  q  \mmember{}  \{G,  phi.\mBbbI{}  \mvdash{}  \_:(Fiber(equiv-fun(f);a))p\}


By

---

Latex:
(Assert  p  \mmember{}  G,  phi.\mBbbI{}  j{}\mrightarrow{}  G,  phi  BY
              Auto)

---

Home Index