---

Step * of Lemma is-equiv-witness_wf

No Annotations
∀[X:j⊢]. ∀[T,A:{X ⊢ _}]. ∀[w:{X ⊢ _:(T ⟶ A)}]. ∀[c:{X.A ⊢ _:Fiber((w)p;q)}].
∀[p:{X.A.Fiber((w)p;q) ⊢ _:(Path_(Fiber((w)p;q))p (c)p q)}].
  (is-equiv-witness(X;A;c;p) ∈ {X ⊢ _:IsEquiv(T;A;w)})
BY
{ (Intros
   THEN RepUR ``is-equiv-witness is-cubical-equiv`` 0
   THEN InstLemmaIJ `contr-witness_wf` [⌜X.A⌝;⌜Fiber((w)p;q)⌝;⌜c⌝;⌜p⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[T,A:\{X  \mvdash{}  \_\}].  \mforall{}[w:\{X  \mvdash{}  \_:(T  {}\mrightarrow{}  A)\}].  \mforall{}[c:\{X.A  \mvdash{}  \_:Fiber((w)p;q)\}].
\mforall{}[p:\{X.A.Fiber((w)p;q)  \mvdash{}  \_:(Path\_(Fiber((w)p;q))p  (c)p  q)\}].
    (is-equiv-witness(X;A;c;p)  \mmember{}  \{X  \mvdash{}  \_:IsEquiv(T;A;w)\})


By

---

Latex:
(Intros
  THEN  RepUR  ``is-equiv-witness  is-cubical-equiv``  0
  THEN  InstLemmaIJ  `contr-witness\_wf`  [\mkleeneopen{}X.A\mkleeneclose{};\mkleeneopen{}Fiber((w)p;q)\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index