---

Step * 1 of Lemma contr-path_wf


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)}
BY
{ Assert ⌜c.2 ∈ {X ⊢ _:ΠA (Path_(A)p (contr-center(c))p q)}⌝⋅ }

1
.....assertion..... 
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)]}
⊢ c.2 ∈ {X ⊢ _:ΠA (Path_(A)p (contr-center(c))p q)}

2
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)]}
7. c.2 ∈ {X ⊢ _:ΠA (Path_(A)p (contr-center(c))p q)}
⊢ app(c.2; x) ∈ {X ⊢ _:(Path_A contr-center(c) x)}

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  A  :  \{X  \mvdash{}  \_\}
3.  c  :  \{X  \mvdash{}  \_:\mSigma{}  A  \mPi{}(A)p  (Path\_((A)p)p  (q)p  q)\}
4.  x  :  \{X  \mvdash{}  \_:A\}
5.  c  \mmember{}  \{X  \mvdash{}  \_:Contractible(A)\}
6.  c.2  \mmember{}  \{X  \mvdash{}  \_:(\mPi{}(A)p  (Path\_((A)p)p  (q)p  q))[contr-center(c)]\}
\mvdash{}  app(c.2;  x)  \mmember{}  \{X  \mvdash{}  \_:(Path\_A  contr-center(c)  x)\}


By

---

Latex:
Assert  \mkleeneopen{}c.2  \mmember{}  \{X  \mvdash{}  \_:\mPi{}A  (Path\_(A)p  (contr-center(c))p  q)\}\mkleeneclose{}\mcdot{}

---

Home Index