---

Step * 2 of Lemma cubical-contr_wf


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']}
10. app(p.2; u) ∈ {Gamma, phi ⊢ _:(Path_A p.1 u)}
⊢ comp (cA)p [phi ⊢→ (app(p.2; u))p @ q] p.1 ∈ {Gamma ⊢ _:A[phi |⟶ u]}
BY
{ Assert ⌜(app(p.2; u))p @ q ∈ {Gamma, phi.𝕀 ⊢ _:(A)p}⌝⋅ }

1
.....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']}
10. app(p.2; u) ∈ {Gamma, phi ⊢ _:(Path_A p.1 u)}
⊢ (app(p.2; u))p @ q ∈ {Gamma, phi.𝕀 ⊢ _:(A)p}

2
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']}
10. app(p.2; u) ∈ {Gamma, phi ⊢ _:(Path_A p.1 u)}
11. (app(p.2; u))p @ q ∈ {Gamma, phi.𝕀 ⊢ _:(A)p}
⊢ comp (cA)p [phi ⊢→ (app(p.2; u))p @ q] p.1 ∈ {Gamma ⊢ _:A[phi |⟶ u]}

---

Latex:

---

Latex:

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']\}
10.  app(p.2;  u)  \mmember{}  \{Gamma,  phi  \mvdash{}  \_:(Path\_A  p.1  u)\}
\mvdash{}  comp  (cA)p  [phi  \mvdash{}\mrightarrow{}  (app(p.2;  u))p  @  q]  p.1  \mmember{}  \{Gamma  \mvdash{}  \_:A[phi  |{}\mrightarrow{}  u]\}


By

---

Latex:
Assert  \mkleeneopen{}(app(p.2;  u))p  @  q  \mmember{}  \{Gamma,  phi.\mBbbI{}  \mvdash{}  \_:(A)p\}\mkleeneclose{}\mcdot{}

---

Home Index