---

Step * 1 of Lemma csm-equiv_term


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. cA : G +⊢ Compositon(A)
11. cT : G +⊢ Compositon(T)
12. H : CubicalSet{j}
13. s : H j⟶ G
14. fiber-point(t;c) ∈ {G, phi ⊢ _:Fiber(equiv-fun(f);a)}
15. (fiber-point(t;c))s ∈ {H, (phi)s ⊢ _:(Fiber(equiv-fun(f);a))s}
16. (fiber-point(t;c))s ∈ {H, (phi)s ⊢ _:Fiber((equiv-fun(f))s;(a)s)}
⊢ (equiv f [phi ⊢→ (t,  c)] a)s
= equiv (f)s [(phi)s ⊢→ ((t)s,  (c)s)] (a)s
∈ {H ⊢ _:Fiber(equiv-fun((f)s);(a)s)[(phi)s |⟶ fiber-point((t)s;(c)s)]}
BY
{ (Enough to prove equiv (f)s [(phi)s ⊢→ ((t)s,  (c)s)] (a)s
   = equiv (f)s [(phi)s ⊢→ ((t)s,  (c)s)] (a)s
   ∈ {H ⊢ _:Fiber(equiv-fun((f)s);(a)s)[(phi)s |⟶ fiber-point((t)s;(c)s)]}
    Because (RWO  "csm-equiv-term" 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. cA : G +⊢ Compositon(A)
11. cT : G +⊢ Compositon(T)
12. H : CubicalSet{j}
13. s : H j⟶ G
14. fiber-point(t;c) ∈ {G, phi ⊢ _:Fiber(equiv-fun(f);a)}
15. (fiber-point(t;c))s ∈ {H, (phi)s ⊢ _:(Fiber(equiv-fun(f);a))s}
16. (fiber-point(t;c))s ∈ {H, (phi)s ⊢ _:Fiber((equiv-fun(f))s;(a)s)}
⊢ equiv (f)s [(phi)s ⊢→ ((t)s,  (c)s)] (a)s
= equiv (f)s [(phi)s ⊢→ ((t)s,  (c)s)] (a)s
∈ {H ⊢ _:Fiber(equiv-fun((f)s);(a)s)[(phi)s |⟶ fiber-point((t)s;(c)s)]}

2
.....aux..... 
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. cA : G +⊢ Compositon(A)
11. cT : G +⊢ Compositon(T)
12. H : CubicalSet{j}
13. s : H j⟶ G
14. fiber-point(t;c) ∈ {G, phi ⊢ _:Fiber(equiv-fun(f);a)}
15. (fiber-point(t;c))s ∈ {H, (phi)s ⊢ _:(Fiber(equiv-fun(f);a))s}
16. (fiber-point(t;c))s ∈ {H, (phi)s ⊢ _:Fiber((equiv-fun(f))s;(a)s)}
17. equiv (f)s [(phi)s ⊢→ ((t)s,  (c)s)] (a)s
= equiv (f)s [(phi)s ⊢→ ((t)s,  (c)s)] (a)s
∈ {H ⊢ _:Fiber(equiv-fun((f)s);(a)s)[(phi)s |⟶ fiber-point((t)s;(c)s)]}
⊢ fiber-point((t)s;(c)s) ∈ {H, (phi)s ⊢ _:Fiber(equiv-fun((f)s);(a)s)}

---

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.  cA  :  G  +\mvdash{}  Compositon(A)
11.  cT  :  G  +\mvdash{}  Compositon(T)
12.  H  :  CubicalSet\{j\}
13.  s  :  H  j{}\mrightarrow{}  G
14.  fiber-point(t;c)  \mmember{}  \{G,  phi  \mvdash{}  \_:Fiber(equiv-fun(f);a)\}
15.  (fiber-point(t;c))s  \mmember{}  \{H,  (phi)s  \mvdash{}  \_:(Fiber(equiv-fun(f);a))s\}
16.  (fiber-point(t;c))s  \mmember{}  \{H,  (phi)s  \mvdash{}  \_:Fiber((equiv-fun(f))s;(a)s)\}
\mvdash{}  (equiv  f  [phi  \mvdash{}\mrightarrow{}  (t,    c)]  a)s  =  equiv  (f)s  [(phi)s  \mvdash{}\mrightarrow{}  ((t)s,    (c)s)]  (a)s


By

---

Latex:
(Enough  to  prove  equiv  (f)s  [(phi)s  \mvdash{}\mrightarrow{}  ((t)s,    (c)s)]  (a)s
  =  equiv  (f)s  [(phi)s  \mvdash{}\mrightarrow{}  ((t)s,    (c)s)]  (a)s
    Because  (RWO    "csm-equiv-term"  0  THEN  Auto))

---

Home Index