---

Step * 1 of Lemma equiv-term-subset


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. psi : {G ⊢ _:𝔽}
12. e : {G ⊢ _:Contractible(Fiber(equiv-fun(f);a))}
13. G ⊢ Fiber(equiv-fun(f);a)
14. fiber-point(t;c) ∈ {G, phi ⊢ _:Fiber(equiv-fun(f);a)}
15. ∀[u:{G, phi.𝕀 ⊢ _:(Fiber(equiv-fun(f);a))p}]. ∀[a0:{G ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}].
      (comp (cF)p [phi ⊢→ u] a0 ∈ {G ⊢ _:((Fiber(equiv-fun(f);a))p)[1(𝕀)][phi |⟶ (u)[1(𝕀)]]})
⊢ comp (cF)p [phi ⊢→ (contr-path(e;fiber-point(t;c)))p @ q] contr-center(e)
= comp (cF)p [phi ⊢→ (contr-path(e;fiber-point(t;c)))p @ q] contr-center(e)
∈ {G, psi ⊢ _:Fiber(equiv-fun(f);a)}
BY
{ ((Assert contr-center(e) ∈ {G, phi ⊢ _:Fiber(equiv-fun(f);a)} BY
          (SubsumeC ⌜{G ⊢ _:Fiber(equiv-fun(f);a)}⌝⋅ THEN Auto))
   THEN (Assert contr-path(e;fiber-point(t;c)) ∈ {G, phi ⊢ _:(Path_Fiber(equiv-fun(f);a) contr-center(e)
                                                                   fiber-point(t;c))} BY
               (MemCD THEN RWW "contractible-type-subset" 0 THEN 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. psi : {G ⊢ _:𝔽}
12. e : {G ⊢ _:Contractible(Fiber(equiv-fun(f);a))}
13. G ⊢ Fiber(equiv-fun(f);a)
14. fiber-point(t;c) ∈ {G, phi ⊢ _:Fiber(equiv-fun(f);a)}
15. ∀[u:{G, phi.𝕀 ⊢ _:(Fiber(equiv-fun(f);a))p}]. ∀[a0:{G ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}].
      (comp (cF)p [phi ⊢→ u] a0 ∈ {G ⊢ _:((Fiber(equiv-fun(f);a))p)[1(𝕀)][phi |⟶ (u)[1(𝕀)]]})
16. contr-center(e) ∈ {G, phi ⊢ _:Fiber(equiv-fun(f);a)}
17. contr-path(e;fiber-point(t;c)) ∈ {G, phi ⊢ _:(Path_Fiber(equiv-fun(f);a) contr-center(e) fiber-point(t;c))}
⊢ comp (cF)p [phi ⊢→ (contr-path(e;fiber-point(t;c)))p @ q] contr-center(e)
= comp (cF)p [phi ⊢→ (contr-path(e;fiber-point(t;c)))p @ q] contr-center(e)
∈ {G, psi ⊢ _:Fiber(equiv-fun(f);a)}

---

Latex:

---

Latex:

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.  psi  :  \{G  \mvdash{}  \_:\mBbbF{}\}
12.  e  :  \{G  \mvdash{}  \_:Contractible(Fiber(equiv-fun(f);a))\}
13.  G  \mvdash{}  Fiber(equiv-fun(f);a)
14.  fiber-point(t;c)  \mmember{}  \{G,  phi  \mvdash{}  \_:Fiber(equiv-fun(f);a)\}
15.  \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{})]]\}].
            (comp  (cF)p  [phi  \mvdash{}\mrightarrow{}  u]  a0  \mmember{}  \{G  \mvdash{}  \_:((Fiber(equiv-fun(f);a))p)[1(\mBbbI{})][phi  |{}\mrightarrow{}  (u)[1(\mBbbI{})]]\})
\mvdash{}  comp  (cF)p  [phi  \mvdash{}\mrightarrow{}  (contr-path(e;fiber-point(t;c)))p  @  q]  contr-center(e)
=  comp  (cF)p  [phi  \mvdash{}\mrightarrow{}  (contr-path(e;fiber-point(t;c)))p  @  q]  contr-center(e)


By

---

Latex:
((Assert  contr-center(e)  \mmember{}  \{G,  phi  \mvdash{}  \_:Fiber(equiv-fun(f);a)\}  BY
                (SubsumeC  \mkleeneopen{}\{G  \mvdash{}  \_:Fiber(equiv-fun(f);a)\}\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (Assert  contr-path(e;fiber-point(t;c))
                            \mmember{}  \{G,  phi  \mvdash{}  \_:(Path\_Fiber(equiv-fun(f);a)  contr-center(e)  fiber-point(t;c))\}  BY
                          (MemCD  THEN  RWW  "contractible-type-subset"  0  THEN  Auto))
  )

---

Home Index