---

Step * of Lemma contr-witness_wf

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[c:{X ⊢ _:A}]. ∀[p:{X.A ⊢ _:(Path_(A)p (c)p q)}].
  (contr-witness(X;c;p) ∈ {X ⊢ _:Contractible(A)})
BY
{ (Auto
   THEN Unfolds ``contractible-type contr-witness`` 0
   THEN (Enough to prove (λp) ∈ {X ⊢ _:(Π(A)p (Path_((A)p)p (q)p q))[c]}
          Because Auto)) }

1
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. c : {X ⊢ _:A}
4. p : {X.A ⊢ _:(Path_(A)p (c)p q)}
⊢ (λp) ∈ {X ⊢ _:(Π(A)p (Path_((A)p)p (q)p q))[c]}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[c:\{X  \mvdash{}  \_:A\}].  \mforall{}[p:\{X.A  \mvdash{}  \_:(Path\_(A)p  (c)p  q)\}].
    (contr-witness(X;c;p)  \mmember{}  \{X  \mvdash{}  \_:Contractible(A)\})


By

---

Latex:
(Auto
  THEN  Unfolds  ``contractible-type  contr-witness``  0
  THEN  (Enough  to  prove  (\mlambda{}p)  \mmember{}  \{X  \mvdash{}  \_:(\mPi{}(A)p  (Path\_((A)p)p  (q)p  q))[c]\}
                Because  Auto))

---

Home Index