---

Step * of Lemma contr-path_wf

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[c:{X ⊢ _:Contractible(A)}]. ∀[x:{X ⊢ _:A}].
  (contr-path(c;x) ∈ {X ⊢ _:(Path_A contr-center(c) x)})
BY
{ (Auto
   THEN (Assert c ∈ {X ⊢ _:Contractible(A)} BY
               Trivial)
   THEN Unfold `contractible-type` -3
   THEN RepUR ``contr-path`` 0
   THEN (InstLemma `cubical-snd_wf` [⌜X⌝;⌜A⌝;⌜Π(A)p (Path_((A)p)p (q)p q)⌝;⌜c⌝]⋅ THENA Auto)
   THEN Fold `contr-center` (-1)) }

1
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. c : {X ⊢ _:Σ A Π(A)p (Path_((A)p)p (q)p q)}
4. x : {X ⊢ _:A}
5. c ∈ {X ⊢ _:Contractible(A)}
6. c.2 ∈ {X ⊢ _:(Π(A)p (Path_((A)p)p (q)p q))[contr-center(c)]}
⊢ app(c.2; x) ∈ {X ⊢ _:(Path_A contr-center(c) x)}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[c:\{X  \mvdash{}  \_:Contractible(A)\}].  \mforall{}[x:\{X  \mvdash{}  \_:A\}].
    (contr-path(c;x)  \mmember{}  \{X  \mvdash{}  \_:(Path\_A  contr-center(c)  x)\})


By

---

Latex:
(Auto
  THEN  (Assert  c  \mmember{}  \{X  \mvdash{}  \_:Contractible(A)\}  BY
                          Trivial)
  THEN  Unfold  `contractible-type`  -3
  THEN  RepUR  ``contr-path``  0
  THEN  (InstLemma  `cubical-snd\_wf`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}\mPi{}(A)p  (Path\_((A)p)p  (q)p  q)\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Fold  `contr-center`  (-1))

---

Home Index