Step
*
1
of Lemma
cubical-id-equiv-subset
1. G : Top
2. phi : Top
3. A : Top
⊢ (λcubical-pair((q)p @ q;path-contraction(G, phi.A.(A)p.(Path_((A)p)p (q)p q);q))) 
~ (λcubical-pair((q)p @ q;path-contraction(G.A.(A)p.(Path_((A)p)p (q)p q);q)))
BY
{ Subst' 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) 0 }
1
.....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)
2
1. G : Top
2. phi : Top
3. A : Top
⊢ (λcubical-pair((q)p @ q;path-contraction(G.A.(A)p.(Path_((A)p)p (q)p q);q))) 
~ (λcubical-pair((q)p @ q;path-contraction(G.A.(A)p.(Path_((A)p)p (q)p q);q)))
Latex:
Latex:
1.  G  :  Top
2.  phi  :  Top
3.  A  :  Top
\mvdash{}  (\mlambda{}cubical-pair((q)p  @  q;path-contraction(G,  phi.A.(A)p.(Path\_((A)p)p  (q)p  q);q))) 
\msim{}  (\mlambda{}cubical-pair((q)p  @  q;path-contraction(G.A.(A)p.(Path\_((A)p)p  (q)p  q);q)))
By
Latex:
Subst'  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)  0
Home
Index