---

Step * of Lemma equiv-witness_wf

No Annotations
∀[G:j⊢]. ∀[A,T:{G ⊢ _}]. ∀[f:{G ⊢ _:(T ⟶ A)}]. ∀[iseq:{G ⊢ _:IsEquiv(T;A;f)}].
  (equiv-witness(f;iseq) ∈ {G ⊢ _:Equiv(T;A)})
BY
{ (Auto THEN Unfolds ``cubical-equiv equiv-witness`` 0) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. T : {G ⊢ _}
4. f : {G ⊢ _:(T ⟶ A)}
5. iseq : {G ⊢ _:IsEquiv(T;A;f)}
⊢ cubical-pair(f;iseq) ∈ {G ⊢ _:Σ (T ⟶ A) IsEquiv((T)p;(A)p;q)}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,T:\{G  \mvdash{}  \_\}].  \mforall{}[f:\{G  \mvdash{}  \_:(T  {}\mrightarrow{}  A)\}].  \mforall{}[iseq:\{G  \mvdash{}  \_:IsEquiv(T;A;f)\}].
    (equiv-witness(f;iseq)  \mmember{}  \{G  \mvdash{}  \_:Equiv(T;A)\})


By

---

Latex:
(Auto  THEN  Unfolds  ``cubical-equiv  equiv-witness``  0)

---

Home Index