---

Step * of Lemma equiv-contr_wf

No Annotations
∀[G:j⊢]. ∀[A,T:{G ⊢ _}]. ∀[f:{G ⊢ _:Equiv(T;A)}]. ∀[a:{G ⊢ _:A}].
  (equiv-contr(f;a) ∈ {G ⊢ _:Contractible(Fiber(equiv-fun(f);a))})
BY
{ (Auto
   THEN RepUR ``cubical-equiv`` -2
   THEN (InstLemmaIJ `cubical-snd_wf` [⌜G⌝;⌜(T ⟶ A)⌝;⌜IsEquiv((T)p;(A)p;q)⌝;⌜f⌝]⋅ THENA Auto)
   THEN Fold `equiv-fun` (-1)) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. T : {G ⊢ _}
4. f : {G ⊢ _:Σ (T ⟶ A) IsEquiv((T)p;(A)p;q)}
5. a : {G ⊢ _:A}
6. f.2 ∈ {G ⊢ _:(IsEquiv((T)p;(A)p;q))[equiv-fun(f)]}
⊢ equiv-contr(f;a) ∈ {G ⊢ _:Contractible(Fiber(equiv-fun(f);a))}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,T:\{G  \mvdash{}  \_\}].  \mforall{}[f:\{G  \mvdash{}  \_:Equiv(T;A)\}].  \mforall{}[a:\{G  \mvdash{}  \_:A\}].
    (equiv-contr(f;a)  \mmember{}  \{G  \mvdash{}  \_:Contractible(Fiber(equiv-fun(f);a))\})


By

---

Latex:
(Auto
  THEN  RepUR  ``cubical-equiv``  -2
  THEN  (InstLemmaIJ  `cubical-snd\_wf`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}(T  {}\mrightarrow{}  A)\mkleeneclose{};\mkleeneopen{}IsEquiv((T)p;(A)p;q)\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Fold  `equiv-fun`  (-1))

---

Home Index