---

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

.....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)]}
BY
{ (InstLemmaIJ `csm-is-cubical-equiv` [⌜K.((A)tau ⟶ (A)tau)⌝;⌜((A)tau)p⌝;⌜((A)tau)p⌝;⌜q⌝;⌜K⌝;⌜[cubical-id-fun(K)]⌝]⋅
   THENA 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)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)]}

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
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)
\mvdash{}  cubical-id-is-equiv(K;(A)tau)  =  (cubical-id-is-equiv(G;A))tau


By

---

Latex:
(InstLemmaIJ  `csm-is-cubical-equiv`  [\mkleeneopen{}K.((A)tau  {}\mrightarrow{}  (A)tau)\mkleeneclose{};\mkleeneopen{}((A)tau)p\mkleeneclose{};\mkleeneopen{}((A)tau)p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};
  \mkleeneopen{}[cubical-id-fun(K)]\mkleeneclose{}]\mcdot{}
  THENA  Auto
  )

---

Home Index