---

Step * of Lemma csm-id-fiber-contraction

No Annotations
∀[G,K:j⊢]. ∀[tau:K j⟶ G]. ∀[A:{G ⊢ _}].
  (id-fiber-contraction(K;(A)tau)
  = (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 (id-fiber-center(K;(A)tau))p q)})
BY
{ (Auto
   THEN (Assert ⌜(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)}⌝⋅
        THENM (BLemma `paths-equal-eta` THENA Auto)
        )
   ) }

1
.....assertion..... 
1. G : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ G
4. A : {G ⊢ _}
⊢ (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)}

2
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}

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Assert  \mkleeneopen{}(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)\}\mkleeneclose{}\mcdot{}
            THENM  (BLemma  `paths-equal-eta`  THENA  Auto)
            )
  )

---

Home Index