---

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


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)))
BY
{ (GenConcl ⌜cubical-pair((q)p @ q;path-contraction(G.A.(A)p.(Path_((A)p)p (q)p q);q)) = b ∈ Top⌝⋅ THENA Auto) }

1
1. G : Top
2. phi : Top
3. A : Top
4. b : Top
5. cubical-pair((q)p @ q;path-contraction(G.A.(A)p.(Path_((A)p)p (q)p q);q)) = b ∈ Top
⊢ (λb) ~ (λb)

---

Latex:

---

Latex:

1.  G  :  Top
2.  phi  :  Top
3.  A  :  Top
\mvdash{}  (\mlambda{}cubical-pair((q)p  @  q;path-contraction(G.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:
(GenConcl  \mkleeneopen{}cubical-pair((q)p  @  q;path-contraction(G.A.(A)p.(Path\_((A)p)p  (q)p  q);q))  =  b\mkleeneclose{}\mcdot{}
  THENA  Auto
  )

---

Home Index