---

Step * of Lemma equiv-term-subset

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))}]. ∀[cF:G ⊢ Compositon(Fiber(equiv-fun(f);a))]. ∀[psi:{G ⊢ _:𝔽}].
  (equiv f [phi ⊢→ (t,  c)] a = equiv f [phi ⊢→ (t,  c)] a ∈ {G, psi ⊢ _:Fiber(equiv-fun(f);a)})
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 (GenConclTerm ⌜equiv-contr(f;a)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN RenameVar `e' (-1)
   THEN (RepUR ``let`` 0 THEN (InstLemma `cubical-fiber_wf` [⌜G⌝;⌜T⌝;⌜A⌝;⌜equiv-fun(f)⌝;⌜a⌝]⋅ THENA Auto))
   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 (InstLemma `comp_term_wf` [⌜G⌝;⌜phi⌝;⌜(Fiber(equiv-fun(f);a))p⌝;⌜(cF)p⌝]⋅ THENA 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(𝕀)]]})
⊢ 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:
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{}[cF:G  \mvdash{}  Compositon(Fiber(equiv-fun(f);a))].  \mforall{}[psi:\{G  \mvdash{}  \_:\mBbbF{}\}].
    (equiv  f  [phi  \mvdash{}\mrightarrow{}  (t,    c)]  a  =  equiv  f  [phi  \mvdash{}\mrightarrow{}  (t,    c)]  a)


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  (GenConclTerm  \mkleeneopen{}equiv-contr(f;a)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  RenameVar  `e'  (-1)
  THEN  (RepUR  ``let``  0
              THEN  (InstLemma  `cubical-fiber\_wf`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}equiv-fun(f)\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
              )
  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  (InstLemma  `comp\_term\_wf`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}(Fiber(equiv-fun(f);a))p\mkleeneclose{};\mkleeneopen{}(cF)p\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index