---

Step * 2 of Lemma equiv-term-0

.....subterm..... T:t
2: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(𝕀)]}
⊢ comp (cF)p [phi ⊢→ xx] ctr = comp (cF)p [0(𝔽) ⊢→ xx] ctr ∈ {G ⊢ _:Fiber(equiv-fun(f);a)}
BY
{ (EquationFromStrongHyp 3
   THEN (InstLemma `comp_term_wf` [⌜G⌝;⌜Z⌝;⌜(Fiber(equiv-fun(f);a))p⌝;⌜(cF)p⌝]⋅ THENA Auto)
   THEN InstHyp [⌜xx⌝;⌜ctr⌝] (-1)⋅) }

1
.....wf..... 
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. A : {G ⊢ _}
4. T : {G ⊢ _}
5. f : {G ⊢ _:Equiv(T;A)}
6. a : {G ⊢ _:A}
7. t : Top
8. c : Top
9. cF : G +⊢ Compositon(Fiber(equiv-fun(f);a))
10. ctr : {G ⊢ _:Fiber(equiv-fun(f);a)}
11. contr-center(equiv-contr(f;a)) = ctr ∈ {G ⊢ _:Fiber(equiv-fun(f);a)}
12. xx : Top
13. (contr-path(equiv-contr(f;a);fiber-point(t;c)))p @ q = xx ∈ Top
14. ∀[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(𝕀)]})
15. Z : {G ⊢ _:𝔽}
16. Z = phi ∈ {G ⊢ _:𝔽}
17. Z = 0(𝔽) ∈ {G ⊢ _:𝔽}
18. ∀[u:{G, Z.𝕀 ⊢ _:(Fiber(equiv-fun(f);a))p}]. ∀[a0:{G ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)][Z |⟶ (u)[0(𝕀)]]}].
      (comp (cF)p [Z ⊢→ u] a0 ∈ {G ⊢ _:((Fiber(equiv-fun(f);a))p)[1(𝕀)][Z |⟶ (u)[1(𝕀)]]})
⊢ xx ∈ {G, Z.𝕀 ⊢ _:(Fiber(equiv-fun(f);a))p}

2
.....wf..... 
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. A : {G ⊢ _}
4. T : {G ⊢ _}
5. f : {G ⊢ _:Equiv(T;A)}
6. a : {G ⊢ _:A}
7. t : Top
8. c : Top
9. cF : G +⊢ Compositon(Fiber(equiv-fun(f);a))
10. ctr : {G ⊢ _:Fiber(equiv-fun(f);a)}
11. contr-center(equiv-contr(f;a)) = ctr ∈ {G ⊢ _:Fiber(equiv-fun(f);a)}
12. xx : Top
13. (contr-path(equiv-contr(f;a);fiber-point(t;c)))p @ q = xx ∈ Top
14. ∀[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(𝕀)]})
15. Z : {G ⊢ _:𝔽}
16. Z = phi ∈ {G ⊢ _:𝔽}
17. Z = 0(𝔽) ∈ {G ⊢ _:𝔽}
18. ∀[u:{G, Z.𝕀 ⊢ _:(Fiber(equiv-fun(f);a))p}]. ∀[a0:{G ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)][Z |⟶ (u)[0(𝕀)]]}].
      (comp (cF)p [Z ⊢→ u] a0 ∈ {G ⊢ _:((Fiber(equiv-fun(f);a))p)[1(𝕀)][Z |⟶ (u)[1(𝕀)]]})
⊢ ctr ∈ {G ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)][Z |⟶ (xx)[0(𝕀)]]}

3
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. A : {G ⊢ _}
4. T : {G ⊢ _}
5. f : {G ⊢ _:Equiv(T;A)}
6. a : {G ⊢ _:A}
7. t : Top
8. c : Top
9. cF : G +⊢ Compositon(Fiber(equiv-fun(f);a))
10. ctr : {G ⊢ _:Fiber(equiv-fun(f);a)}
11. contr-center(equiv-contr(f;a)) = ctr ∈ {G ⊢ _:Fiber(equiv-fun(f);a)}
12. xx : Top
13. (contr-path(equiv-contr(f;a);fiber-point(t;c)))p @ q = xx ∈ Top
14. ∀[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(𝕀)]})
15. Z : {G ⊢ _:𝔽}
16. Z = phi ∈ {G ⊢ _:𝔽}
17. Z = 0(𝔽) ∈ {G ⊢ _:𝔽}
18. ∀[u:{G, Z.𝕀 ⊢ _:(Fiber(equiv-fun(f);a))p}]. ∀[a0:{G ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)][Z |⟶ (u)[0(𝕀)]]}].
      (comp (cF)p [Z ⊢→ u] a0 ∈ {G ⊢ _:((Fiber(equiv-fun(f);a))p)[1(𝕀)][Z |⟶ (u)[1(𝕀)]]})
19. comp (cF)p [Z ⊢→ xx] ctr ∈ {G ⊢ _:((Fiber(equiv-fun(f);a))p)[1(𝕀)][Z |⟶ (xx)[1(𝕀)]]}
⊢ comp (cF)p [Z ⊢→ xx] ctr ∈ {G ⊢ _:Fiber(equiv-fun(f);a)}

---

Latex:

---

Latex:
.....subterm.....  T:t
2: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{}  comp  (cF)p  [phi  \mvdash{}\mrightarrow{}  xx]  ctr  =  comp  (cF)p  [0(\mBbbF{})  \mvdash{}\mrightarrow{}  xx]  ctr


By

---

Latex:
(EquationFromStrongHyp  3
  THEN  (InstLemma  `comp\_term\_wf`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}Z\mkleeneclose{};\mkleeneopen{}(Fiber(equiv-fun(f);a))p\mkleeneclose{};\mkleeneopen{}(cF)p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  InstHyp  [\mkleeneopen{}xx\mkleeneclose{};\mkleeneopen{}ctr\mkleeneclose{}]  (-1)\mcdot{})

---

Home Index