---

Step * of Lemma cubical-id-equiv-subset

∀[G,phi,A:Top].  (IdEquiv(G, phi;A) ~ IdEquiv(G;A))
BY
{ (Intros
   THEN RepUR ``cubical-id-equiv cubical-id-fun cubical-lam`` 0
   THEN (RepUR ``cubical-id-is-equiv contr-witness id-fiber-center`` 0
         THEN RepUR ``cubical-refl term-to-path id-fiber-contraction`` 0
         THEN RepUR ``singleton-contraction term-to-path`` 0)
   THEN (RWW "cubical-lambda-subset cubical-lambda-subset2" 0 THENA Auto)
   THEN RepeatFor 5 ((EqCD THEN Try (Trivial)))) }

1
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)))

---

Latex:

---

Latex:
\mforall{}[G,phi,A:Top].    (IdEquiv(G,  phi;A)  \msim{}  IdEquiv(G;A))


By

---

Latex:
(Intros
  THEN  RepUR  ``cubical-id-equiv  cubical-id-fun  cubical-lam``  0
  THEN  (RepUR  ``cubical-id-is-equiv  contr-witness  id-fiber-center``  0
              THEN  RepUR  ``cubical-refl  term-to-path  id-fiber-contraction``  0
              THEN  RepUR  ``singleton-contraction  term-to-path``  0)
  THEN  (RWW  "cubical-lambda-subset  cubical-lambda-subset2"  0  THENA  Auto)
  THEN  RepeatFor  5  ((EqCD  THEN  Try  (Trivial))))

---

Home Index