---

Step * 1 of Lemma cubical-contr_wf

.....assertion..... 
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : Gamma ⊢ CompOp(A)
4. p : {Gamma ⊢ _:Contractible(A)}
5. phi : {Gamma ⊢ _:𝔽}
6. Gamma.A ⊢ ((Path_((A)p)p (q)p q))([p.1] o p;q)
7. (A)iota = A ∈ {Gamma, phi ⊢ _}
8. u : {Gamma, phi ⊢ _:A}
9. {Gamma, phi ⊢ _:(Path_A p.1 u)} ∈ 𝕌{[i | j']}
⊢ app(p.2; u) ∈ {Gamma, phi ⊢ _:(Path_A p.1 u)}
BY
{ (Unfold `contractible-type` 4 THEN (GenConclTerm ⌜p.2⌝⋅ THENA Auto)) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : Gamma ⊢ CompOp(A)
4. p : {Gamma ⊢ _:Σ A Π(A)p (Path_((A)p)p (q)p q)}
5. phi : {Gamma ⊢ _:𝔽}
6. Gamma.A ⊢ ((Path_((A)p)p (q)p q))([p.1] o p;q)
7. (A)iota = A ∈ {Gamma, phi ⊢ _}
8. u : {Gamma, phi ⊢ _:A}
9. {Gamma, phi ⊢ _:(Path_A p.1 u)} ∈ 𝕌{[i | j']}
10. v : {Gamma ⊢ _:(Π(A)p (Path_((A)p)p (q)p q))[p.1]}
11. p.2 = v ∈ {Gamma ⊢ _:(Π(A)p (Path_((A)p)p (q)p q))[p.1]}
⊢ app(v; u) ∈ {Gamma, phi ⊢ _:(Path_A p.1 u)}

---

Latex:

---

Latex:
.....assertion..... 
1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  cA  :  Gamma  \mvdash{}  CompOp(A)
4.  p  :  \{Gamma  \mvdash{}  \_:Contractible(A)\}
5.  phi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
6.  Gamma.A  \mvdash{}  ((Path\_((A)p)p  (q)p  q))([p.1]  o  p;q)
7.  (A)iota  =  A
8.  u  :  \{Gamma,  phi  \mvdash{}  \_:A\}
9.  \{Gamma,  phi  \mvdash{}  \_:(Path\_A  p.1  u)\}  \mmember{}  \mBbbU{}\{[i  |  j']\}
\mvdash{}  app(p.2;  u)  \mmember{}  \{Gamma,  phi  \mvdash{}  \_:(Path\_A  p.1  u)\}


By

---

Latex:
(Unfold  `contractible-type`  4  THEN  (GenConclTerm  \mkleeneopen{}p.2\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index