---

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

No Annotations
∀[G,K:j⊢]. ∀[tau:K j⟶ G]. ∀[A:{G ⊢ _}].
  (cubical-id-is-equiv(K;(A)tau) = (cubical-id-is-equiv(G;A))tau ∈ {K ⊢ _:IsEquiv((A)tau;(A)tau;cubical-id-fun(K))})
BY
{ (Auto
   THEN (RepUR ``is-cubical-equiv cubical-id-is-equiv`` 0
         THEN (InstLemmaIJ `csm-cubical-id-fun` [⌜G⌝;⌜A⌝;⌜G.A⌝;⌜p⌝]⋅ THENA Auto)
         )
   THEN ((Assert cubical-id-fun(G) ∈ {G ⊢ _:(A ⟶ A)} BY
                Auto)
         THEN (InstLemmaIJ `cubical-fiber-id-fun` [⌜G.A⌝;⌜(A)p⌝;⌜q⌝]⋅ THENA Auto)
         THEN (InstLemmaIJ `csm-cubical-id-fun` [⌜G⌝;⌜A⌝;⌜G.A⌝;⌜p⌝]⋅ THENA Auto)
         THEN (RWO  "-1<" (-2) THENA Auto))
   THEN (InstLemmaIJ `csm-ap-cubical-lambda` [⌜G⌝;⌜A⌝;⌜Contractible(Fiber((cubical-id-fun(G))p;q))⌝;
         ⌜contr-witness(G.A;id-fiber-center(G;A);id-fiber-contraction(G;A))⌝
         ; ⌜K⌝;⌜tau⌝]⋅
         THENA Auto
         )
   THEN (Assert (cubical-id-fun(K))p ∈ {K.(A)tau ⊢ _:(((A)tau)p ⟶ ((A)tau)p)} BY
               ((Assert cubical-id-fun(K) ∈ {K ⊢ _:((A)tau ⟶ (A)tau)} BY Auto) THEN Auto))) }

1
1. G : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ G
4. A : {G ⊢ _}
5. (cubical-id-fun(G))p = cubical-id-fun(G.A) ∈ {G.A ⊢ _:((A)p ⟶ (A)p)}
6. cubical-id-fun(G) ∈ {G ⊢ _:(A ⟶ A)}
7. G.A ⊢ Fiber((cubical-id-fun(G))p;q) = Σ (A)p (Path_((A)p)p (q)p q) ∈ {G.A ⊢ _}
8. (cubical-id-fun(G))p = cubical-id-fun(G.A) ∈ {G.A ⊢ _:((A)p ⟶ (A)p)}
9. ((λcontr-witness(G.A;id-fiber-center(G;A);id-fiber-contraction(G;A))))tau
= (λ(contr-witness(G.A;id-fiber-center(G;A);id-fiber-contraction(G;A)))tau+)
∈ {K ⊢ _:(ΠA Contractible(Fiber((cubical-id-fun(G))p;q)))tau}
10. (cubical-id-fun(K))p ∈ {K.(A)tau ⊢ _:(((A)tau)p ⟶ ((A)tau)p)}
⊢ (λcontr-witness(K.(A)tau;id-fiber-center(K;(A)tau);id-fiber-contraction(K;(A)tau)))
= ((λcontr-witness(G.A;id-fiber-center(G;A);id-fiber-contraction(G;A))))tau
∈ {K ⊢ _:Π(A)tau Contractible(Fiber((cubical-id-fun(K))p;q))}

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (RepUR  ``is-cubical-equiv  cubical-id-is-equiv``  0
              THEN  (InstLemmaIJ  `csm-cubical-id-fun`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}G.A\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
              )
  THEN  ((Assert  cubical-id-fun(G)  \mmember{}  \{G  \mvdash{}  \_:(A  {}\mrightarrow{}  A)\}  BY
                            Auto)
              THEN  (InstLemmaIJ  `cubical-fiber-id-fun`  [\mkleeneopen{}G.A\mkleeneclose{};\mkleeneopen{}(A)p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (InstLemmaIJ  `csm-cubical-id-fun`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}G.A\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (RWO    "-1<"  (-2)  THENA  Auto))
  THEN  (InstLemmaIJ  `csm-ap-cubical-lambda`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}Contractible(Fiber((cubical-id-fun(G))p;q))\mkleeneclose{};
              \mkleeneopen{}contr-witness(G.A;id-fiber-center(G;A);id-fiber-contraction(G;A))\mkleeneclose{}
              ;  \mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}tau\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  (Assert  (cubical-id-fun(K))p  \mmember{}  \{K.(A)tau  \mvdash{}  \_:(((A)tau)p  {}\mrightarrow{}  ((A)tau)p)\}  BY
                          ((Assert  cubical-id-fun(K)  \mmember{}  \{K  \mvdash{}  \_:((A)tau  {}\mrightarrow{}  (A)tau)\}  BY  Auto)  THEN  Auto)))

---

Home Index