---

Step * 2 1 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)}
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}
BY
{ ((InstLemmaIJ `cubical-sigma-p-p` [⌜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)⌝;𝕀]⋅
    THENA Auto
    )
   THEN (Assert ⌜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)p)p ((Path_(((A)tau)p)p (q)p q))
                                                                                 (p o p o p;q)}⌝⋅
         THENA ((InferEqualType THEN Try (Trivial)) THEN EqCDA THEN Auto)
         )
   THEN (Assert ⌜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)p)p ((Path_(((A)tau)p)p (q)p q))(p o p o p;q)}⌝⋅
   THENM ((InferEqualType THEN Try (Trivial)) THEN EqCDA THEN Auto)
   )) }

1
.....assertion..... 
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}
7. ((Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q))p)p
= Σ ((((A)tau)p)p)p ((Path_(((A)tau)p)p (q)p q))(p o p o p;q)
∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _}
8. 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)p)p ((Path_(((A)tau)p)p (q)p q))(p o p o p;q)}
⊢ 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)p)p ((Path_(((A)tau)p)p (q)p q))(p o p o p;q)}

---

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)\}
6.  path-eta(id-fiber-contraction(K;(A)tau))  \mmember{}  \{K.(A)tau.\mSigma{}  ((A)tau)p  (Path\_(((A)tau)p)p  (q)p  q).\mBbbI{}  \mvdash{}  \_
                                                                                              :((\mSigma{}  ((A)tau)p  (Path\_(((A)tau)p)p  (q)p  q))p)p\}
\mvdash{}  path-eta(id-fiber-contraction(K;(A)tau))  =  path-eta((id-fiber-contraction(G;A))tau++)


By

---

Latex:
((InstLemmaIJ  `cubical-sigma-p-p`  [\mkleeneopen{}K.(A)tau\mkleeneclose{};\mkleeneopen{}\mSigma{}  ((A)tau)p  (Path\_(((A)tau)p)p  (q)p  q)\mkleeneclose{};\mkleeneopen{}((A)tau)p\mkleeneclose{};
    \mkleeneopen{}(Path\_(((A)tau)p)p  (q)p  q)\mkleeneclose{};\mBbbI{}]\mcdot{}
    THENA  Auto
    )
  THEN  (Assert  \mkleeneopen{}path-eta(id-fiber-contraction(K;(A)tau))
                              \mmember{}  \{K.(A)tau.\mSigma{}  ((A)tau)p  (Path\_(((A)tau)p)p  (q)p  q).\mBbbI{}  \mvdash{}  \_
                                    :\mSigma{}  ((((A)tau)p)p)p  ((Path\_(((A)tau)p)p  (q)p  q))(p  o  p  o  p;q)\}\mkleeneclose{}\mcdot{}
              THENA  ((InferEqualType  THEN  Try  (Trivial))  THEN  EqCDA  THEN  Auto)
              )
  THEN  (Assert 
              \mkleeneopen{}path-eta(id-fiber-contraction(K;(A)tau))  =  path-eta((id-fiber-contraction(G;A))tau++)\mkleeneclose{}\mcdot{}
  THENM  ((InferEqualType  THEN  Try  (Trivial))  THEN  EqCDA  THEN  Auto)
  ))

---

Home Index