---

Step * 2 of Lemma csm-id-fiber-contraction


1. G : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ G
4. A : {G ⊢ _}
5. (id-fiber-contraction(G;A))tau++ ∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q) ⊢ _
                                       :Path((Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q))p)}
⊢ path-eta(id-fiber-contraction(K;(A)tau))
= path-eta((id-fiber-contraction(G;A))tau++)
∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _:((Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q))p)p}
BY
{ ((InstLemmaIJ `path-eta_wf` [⌜K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q)⌝;
    ⌜(Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q))p⌝]⋅
    THENA Auto
    )
   THEN (InstHyp [⌜id-fiber-contraction(K;(A)tau)⌝] (-1)⋅
         THENA (DoSubsume THEN Try (BLemma `path-type-sub-pathtype`) THEN Auto)
         )
   THEN Thin (-2)) }

1
1. G : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ G
4. A : {G ⊢ _}
5. (id-fiber-contraction(G;A))tau++ ∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q) ⊢ _
                                       :Path((Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q))p)}
6. path-eta(id-fiber-contraction(K;(A)tau)) ∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _
                                               :((Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q))p)p}
⊢ path-eta(id-fiber-contraction(K;(A)tau))
= path-eta((id-fiber-contraction(G;A))tau++)
∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _:((Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q))p)p}

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  K  :  CubicalSet\{j\}
3.  tau  :  K  j{}\mrightarrow{}  G
4.  A  :  \{G  \mvdash{}  \_\}
5.  (id-fiber-contraction(G;A))tau++  \mmember{}  \{K.(A)tau.\mSigma{}  ((A)tau)p  (Path\_(((A)tau)p)p  (q)p  q)  \mvdash{}  \_
                                                                              :Path((\mSigma{}  ((A)tau)p  (Path\_(((A)tau)p)p  (q)p  q))p)\}
\mvdash{}  path-eta(id-fiber-contraction(K;(A)tau))  =  path-eta((id-fiber-contraction(G;A))tau++)


By

---

Latex:
((InstLemmaIJ  `path-eta\_wf`  [\mkleeneopen{}K.(A)tau.\mSigma{}  ((A)tau)p  (Path\_(((A)tau)p)p  (q)p  q)\mkleeneclose{};
    \mkleeneopen{}(\mSigma{}  ((A)tau)p  (Path\_(((A)tau)p)p  (q)p  q))p\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  (InstHyp  [\mkleeneopen{}id-fiber-contraction(K;(A)tau)\mkleeneclose{}]  (-1)\mcdot{}
              THENA  (DoSubsume  THEN  Try  (BLemma  `path-type-sub-pathtype`)  THEN  Auto)
              )
  THEN  Thin  (-2))

---

Home Index