---

Step * of Lemma equiv_term-0

No Annotations
∀[G:j⊢]. ∀[phi:{G ⊢ _:𝔽}].
  ∀[A,T:{G ⊢ _}]. ∀[f:{G ⊢ _:Equiv(T;A)}]. ∀[a:{G ⊢ _:A}]. ∀[t,c:Top]. ∀[cA:G +⊢ Compositon(A)].
  ∀[cT:G +⊢ Compositon(T)].
    (equiv f [phi ⊢→ (t,c)] a
    = transprt(G;(fiber-comp(G;T;A;equiv-fun(f);a;cT;cA))p;contr-center(equiv-contr(f;a)))
    ∈ {G ⊢ _:Fiber(equiv-fun(f);a)}) 
  supposing phi = 0(𝔽) ∈ {G ⊢ _:𝔽}
BY
{ (InstLemma `equiv-term-0` []
   THEN RepeatFor 9 (ParallelLast')
   THEN Intros
   THEN Unfold `equiv_term` 0
   THEN BackThruSomeHyp) }

---

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{}[a:\{G  \mvdash{}  \_:A\}].  \mforall{}[t,c:Top].  \mforall{}[cA:G  +\mvdash{}  Compositon(A)].
    \mforall{}[cT:G  +\mvdash{}  Compositon(T)].
        (equiv  f  [phi  \mvdash{}\mrightarrow{}  (t,c)]  a
        =  transprt(G;(fiber-comp(G;T;A;equiv-fun(f);a;cT;cA))p;contr-center(equiv-contr(f;a)))) 
    supposing  phi  =  0(\mBbbF{})


By

---

Latex:
(InstLemma  `equiv-term-0`  []
  THEN  RepeatFor  9  (ParallelLast')
  THEN  Intros
  THEN  Unfold  `equiv\_term`  0
  THEN  BackThruSomeHyp)

---

Home Index