---

Step * 1 of Lemma equiv-term-0

.....subterm..... T:t
1:n
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. phi = 0(𝔽) ∈ {G ⊢ _:𝔽}
4. A : {G ⊢ _}
5. T : {G ⊢ _}
6. f : {G ⊢ _:Equiv(T;A)}
7. a : {G ⊢ _:A}
8. t : Top
9. c : Top
10. cF : G +⊢ Compositon(Fiber(equiv-fun(f);a))
11. ctr : {G ⊢ _:Fiber(equiv-fun(f);a)}
12. contr-center(equiv-contr(f;a)) = ctr ∈ {G ⊢ _:Fiber(equiv-fun(f);a)}
13. xx : Top
14. (contr-path(equiv-contr(f;a);fiber-point(t;c)))p @ q = xx ∈ Top
15. ∀[a@0:{G ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)]}]. ∀[xx:Top].
      (comp (cF)p [0(𝔽) ⊢→ xx] a@0 = transprt(G;(cF)p;a@0) ∈ {G ⊢ _:((Fiber(equiv-fun(f);a))p)[1(𝕀)]})
16. comp (cF)p [0(𝔽) ⊢→ xx] ctr = transprt(G;(cF)p;ctr) ∈ {G ⊢ _:((Fiber(equiv-fun(f);a))p)[1(𝕀)]}
⊢ {G ⊢ _:Fiber(equiv-fun(f);a)} = {G ⊢ _:((Fiber(equiv-fun(f);a))p)[1(𝕀)]} ∈ 𝕌{[i | j']}
BY
{ (EqCDA THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  G  :  CubicalSet\{j\}
2.  phi  :  \{G  \mvdash{}  \_:\mBbbF{}\}
3.  phi  =  0(\mBbbF{})
4.  A  :  \{G  \mvdash{}  \_\}
5.  T  :  \{G  \mvdash{}  \_\}
6.  f  :  \{G  \mvdash{}  \_:Equiv(T;A)\}
7.  a  :  \{G  \mvdash{}  \_:A\}
8.  t  :  Top
9.  c  :  Top
10.  cF  :  G  +\mvdash{}  Compositon(Fiber(equiv-fun(f);a))
11.  ctr  :  \{G  \mvdash{}  \_:Fiber(equiv-fun(f);a)\}
12.  contr-center(equiv-contr(f;a))  =  ctr
13.  xx  :  Top
14.  (contr-path(equiv-contr(f;a);fiber-point(t;c)))p  @  q  =  xx
15.  \mforall{}[a@0:\{G  \mvdash{}  \_:((Fiber(equiv-fun(f);a))p)[0(\mBbbI{})]\}].  \mforall{}[xx:Top].
            (comp  (cF)p  [0(\mBbbF{})  \mvdash{}\mrightarrow{}  xx]  a@0  =  transprt(G;(cF)p;a@0))
16.  comp  (cF)p  [0(\mBbbF{})  \mvdash{}\mrightarrow{}  xx]  ctr  =  transprt(G;(cF)p;ctr)
\mvdash{}  \{G  \mvdash{}  \_:Fiber(equiv-fun(f);a)\}  =  \{G  \mvdash{}  \_:((Fiber(equiv-fun(f);a))p)[1(\mBbbI{})]\}


By

---

Latex:
(EqCDA  THEN  Auto)

---

Home Index