---

Step * 1 1 of Lemma cubical-id-equiv-subset

.....equality..... 
1. G : Top
2. phi : Top
3. A : Top
⊢ path-contraction(G, phi.A.(A)p.(Path_((A)p)p (q)p q);q) ~ path-contraction(G.A.(A)p.(Path_((A)p)p (q)p q);q)
BY
{ RepUR ``path-contraction term-to-path`` 0 }

1
1. G : Top
2. phi : Top
3. A : Top
⊢ (λ((q)p)p @ (q)p ∧ q) ~ (λ((q)p)p @ (q)p ∧ q)

---

Latex:

---

Latex:
.....equality..... 
1.  G  :  Top
2.  phi  :  Top
3.  A  :  Top
\mvdash{}  path-contraction(G,  phi.A.(A)p.(Path\_((A)p)p  (q)p  q);q) 
\msim{}  path-contraction(G.A.(A)p.(Path\_((A)p)p  (q)p  q);q)


By

---

Latex:
RepUR  ``path-contraction  term-to-path``  0

---

Home Index