---

Step * of Lemma csm-equiv_term

No Annotations
∀[G:j⊢]. ∀[phi:{G ⊢ _:𝔽}]. ∀[A,T:{G ⊢ _}]. ∀[f:{G ⊢ _:Equiv(T;A)}]. ∀[t:{G, phi ⊢ _:T}]. ∀[a:{G ⊢ _:A}].
∀[c:{G, phi ⊢ _:(Path_A a app(equiv-fun(f); t))}]. ∀[cA:G +⊢ Compositon(A)]. ∀[cT:G +⊢ Compositon(T)]. ∀[H:j⊢].
∀[s:H j⟶ G].
  ((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
{ (RepeatFor 7 (Intro)
   THEN (Assert app(equiv-fun(f); t) ∈ {G, phi ⊢ _:A} BY
               (MemCD THEN Try (RWO "cubical-fun-subset" 0) THEN Auto))
   THEN Intros
   THEN Unhide
   THEN Unfold `equiv_term` 0
   THEN (Assert fiber-point(t;c) ∈ {G, phi ⊢ _:Fiber(equiv-fun(f);a)} BY
               (InferEqualType
                THENL [(RWO  "fiber-subset" 0 THEN Auto); (MemCD THEN RWW "cubical-fun-subset" 0 THEN Auto)]
               ))
   THEN (Assert (fiber-point(t;c))s ∈ {H, (phi)s ⊢ _:(Fiber(equiv-fun(f);a))s} BY
               Auto)
   THEN (Assert (fiber-point(t;c))s ∈ {H, (phi)s ⊢ _:Fiber((equiv-fun(f))s;(a)s)} BY
               (InferEqualType THEN Try (Trivial) THEN EqCDA 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 [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)]}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[phi:\{G  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[A,T:\{G  \mvdash{}  \_\}].  \mforall{}[f:\{G  \mvdash{}  \_:Equiv(T;A)\}].  \mforall{}[t:\{G,  phi  \mvdash{}  \_:T\}].
\mforall{}[a:\{G  \mvdash{}  \_:A\}].  \mforall{}[c:\{G,  phi  \mvdash{}  \_:(Path\_A  a  app(equiv-fun(f);  t))\}].  \mforall{}[cA:G  +\mvdash{}  Compositon(A)].
\mforall{}[cT:G  +\mvdash{}  Compositon(T)].  \mforall{}[H:j\mvdash{}].  \mforall{}[s:H  j{}\mrightarrow{}  G].
    ((equiv  f  [phi  \mvdash{}\mrightarrow{}  (t,c)]  a)s  =  equiv  (f)s  [(phi)s  \mvdash{}\mrightarrow{}  ((t)s,(c)s)]  (a)s)


By

---

Latex:
(RepeatFor  7  (Intro)
  THEN  (Assert  app(equiv-fun(f);  t)  \mmember{}  \{G,  phi  \mvdash{}  \_:A\}  BY
                          (MemCD  THEN  Try  (RWO  "cubical-fun-subset"  0)  THEN  Auto))
  THEN  Intros
  THEN  Unhide
  THEN  Unfold  `equiv\_term`  0
  THEN  (Assert  fiber-point(t;c)  \mmember{}  \{G,  phi  \mvdash{}  \_:Fiber(equiv-fun(f);a)\}  BY
                          (InferEqualType
                            THENL  [(RWO    "fiber-subset"  0  THEN  Auto)
                                        ;  (MemCD  THEN  RWW  "cubical-fun-subset"  0  THEN  Auto)]
                          ))
  THEN  (Assert  (fiber-point(t;c))s  \mmember{}  \{H,  (phi)s  \mvdash{}  \_:(Fiber(equiv-fun(f);a))s\}  BY
                          Auto)
  THEN  (Assert  (fiber-point(t;c))s  \mmember{}  \{H,  (phi)s  \mvdash{}  \_:Fiber((equiv-fun(f))s;(a)s)\}  BY
                          (InferEqualType  THEN  Try  (Trivial)  THEN  EqCDA  THEN  Auto)))

---

Home Index