---

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


1. G : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ G
4. A : {G ⊢ _}
5. I : fset(ℕ)
6. a : K(I)
7. (IsEquiv(((A)tau)p;((A)tau)p;q))[cubical-id-fun(K)]
= IsEquiv((((A)tau)p)[cubical-id-fun(K)];(((A)tau)p)[cubical-id-fun(K)];(q)[cubical-id-fun(K)])
∈ {K ⊢ _}
⊢ 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)]}
BY
{ (Subst' IsEquiv((((A)tau)p)[cubical-id-fun(K)];(((A)tau)p)[cubical-id-fun(K)];(q)[cubical-id-fun(K)]) 
   ~ IsEquiv((A)tau;(A)tau;cubical-id-fun(K)) -1
   THENA (CsmUnfolding THEN Auto THEN RepUR ``cubical-id-fun cubical-lam cubical-lambda`` 0 THEN Auto)
   ) }

1
1. G : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ G
4. A : {G ⊢ _}
5. I : fset(ℕ)
6. a : K(I)
7. (IsEquiv(((A)tau)p;((A)tau)p;q))[cubical-id-fun(K)] = IsEquiv((A)tau;(A)tau;cubical-id-fun(K)) ∈ {K ⊢ _}
⊢ 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:

1.  G  :  CubicalSet\{j\}
2.  K  :  CubicalSet\{j\}
3.  tau  :  K  j{}\mrightarrow{}  G
4.  A  :  \{G  \mvdash{}  \_\}
5.  I  :  fset(\mBbbN{})
6.  a  :  K(I)
7.  (IsEquiv(((A)tau)p;((A)tau)p;q))[cubical-id-fun(K)]
=  IsEquiv((((A)tau)p)[cubical-id-fun(K)];(((A)tau)p)[cubical-id-fun(K)];(q)[cubical-id-fun(K)])
\mvdash{}  cubical-id-is-equiv(K;(A)tau)  =  (cubical-id-is-equiv(G;A))tau


By

---

Latex:
(Subst'  IsEquiv((((A)tau)p)[cubical-id-fun(K)];(((A)tau)p)
                                                                                                [cubical-id-fun(K)];(q)[cubical-id-fun(K)]) 
  \msim{}  IsEquiv((A)tau;(A)tau;cubical-id-fun(K))  -1
  THENA  (CsmUnfolding  THEN  Auto  THEN  RepUR  ``cubical-id-fun  cubical-lam  cubical-lambda``  0  THEN  Auto)
  )

---

Home Index