---

Step * of Lemma csm-cubical-id-equiv

No Annotations
∀[G,K:j⊢]. ∀[tau:K j⟶ G]. ∀[A:{G ⊢ _}].  ((IdEquiv(G;A))tau = IdEquiv(K;(A)tau) ∈ {K ⊢ _:Equiv((A)tau;(A)tau)})
BY
{ (Auto
   THEN Symmetry
   THEN (CubicalTermEqual THENA Auto)
   THEN Fold `cubical-term-at` 0
   THEN RepUR ``cubical-id-equiv equiv-witness`` 0
   THEN (RWO "csm-cubical-pair" 0 THENA Auto)
   THEN (Subst' (cubical-id-fun(G))tau ~ cubical-id-fun(K) 0
         THENA (RepUR ``cubical-id-fun cubical-lam cubical-lambda cc-snd`` 0⋅ THEN CsmUnfolding THEN Auto)
         )
   THEN Unfold `cubical-equiv` 0
   THEN RepeatFor 2 (EqCDA)) }

1
.....subterm..... T:t
2:n
1. G : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ G
4. A : {G ⊢ _}
5. I : fset(ℕ)
6. a : K(I)
⊢ cubical-id-is-equiv(K;(A)tau)
= (cubical-id-is-equiv(G;A))tau
∈ {K ⊢ _:(IsEquiv(((A)tau)p;((A)tau)p;q))[cubical-id-fun(K)]}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G,K:j\mvdash{}].  \mforall{}[tau:K  j{}\mrightarrow{}  G].  \mforall{}[A:\{G  \mvdash{}  \_\}].    ((IdEquiv(G;A))tau  =  IdEquiv(K;(A)tau))


By

---

Latex:
(Auto
  THEN  Symmetry
  THEN  (CubicalTermEqual  THENA  Auto)
  THEN  Fold  `cubical-term-at`  0
  THEN  RepUR  ``cubical-id-equiv  equiv-witness``  0
  THEN  (RWO  "csm-cubical-pair"  0  THENA  Auto)
  THEN  (Subst'  (cubical-id-fun(G))tau  \msim{}  cubical-id-fun(K)  0
              THENA  (RepUR  ``cubical-id-fun  cubical-lam  cubical-lambda  cc-snd``  0\mcdot{}
                            THEN  CsmUnfolding
                            THEN  Auto)
              )
  THEN  Unfold  `cubical-equiv`  0
  THEN  RepeatFor  2  (EqCDA))

---

Home Index