Step
*
1
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) ∈ {G.A.Σ (A)p (Path_((A)p)p (q)p q) ⊢ _
:(Path_(Σ (A)p (Path_((A)p)p (q)p q))p (id-fiber-center(G;A))p q)}
6. ((Path_(Σ (A)p (Path_((A)p)p (q)p q))p (id-fiber-center(G;A))p q))tau++
= (K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q) ⊢ Path_((Σ (A)p (Path_((A)p)p (q)p q))p)tau++
((id-fiber-center(G;A))p)tau++ (q)tau++)
∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q) ⊢ _}
⊢ (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)}
BY
{ Assert ⌜(id-fiber-contraction(G;A))tau++ ∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q) ⊢ _
:((Path_(Σ (A)p (Path_((A)p)p (q)p q))p (id-fiber-center(G;A))p q))tau++}⌝
⋅ }
1
.....assertion.....
1. G : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ G
4. A : {G ⊢ _}
5. id-fiber-contraction(G;A) ∈ {G.A.Σ (A)p (Path_((A)p)p (q)p q) ⊢ _
:(Path_(Σ (A)p (Path_((A)p)p (q)p q))p (id-fiber-center(G;A))p q)}
6. ((Path_(Σ (A)p (Path_((A)p)p (q)p q))p (id-fiber-center(G;A))p q))tau++
= (K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q) ⊢ Path_((Σ (A)p (Path_((A)p)p (q)p q))p)tau++
((id-fiber-center(G;A))p)tau++ (q)tau++)
∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q) ⊢ _}
⊢ (id-fiber-contraction(G;A))tau++ ∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q) ⊢ _
:((Path_(Σ (A)p (Path_((A)p)p (q)p q))p (id-fiber-center(G;A))p q))tau++}
2
1. G : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ G
4. A : {G ⊢ _}
5. id-fiber-contraction(G;A) ∈ {G.A.Σ (A)p (Path_((A)p)p (q)p q) ⊢ _
:(Path_(Σ (A)p (Path_((A)p)p (q)p q))p (id-fiber-center(G;A))p q)}
6. ((Path_(Σ (A)p (Path_((A)p)p (q)p q))p (id-fiber-center(G;A))p q))tau++
= (K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q) ⊢ Path_((Σ (A)p (Path_((A)p)p (q)p q))p)tau++
((id-fiber-center(G;A))p)tau++ (q)tau++)
∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q) ⊢ _}
7. (id-fiber-contraction(G;A))tau++ ∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q) ⊢ _
:((Path_(Σ (A)p (Path_((A)p)p (q)p q))p (id-fiber-center(G;A))p q))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)}
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) \mmember{} \{G.A.\mSigma{} (A)p (Path\_((A)p)p (q)p q) \mvdash{} \_
:(Path\_(\mSigma{} (A)p (Path\_((A)p)p (q)p q))p (id-fiber-center(G;A))p q)\}
6. ((Path\_(\mSigma{} (A)p (Path\_((A)p)p (q)p q))p (id-fiber-center(G;A))p q))tau++
= (K.(A)tau.\mSigma{} ((A)tau)p (Path\_(((A)tau)p)p (q)p q) \mvdash{} Path\_((\mSigma{} (A)p (Path\_((A)p)p (q)p q))p)tau++
((id-fiber-center(G;A))p)tau++ (q)tau++)
\mvdash{} (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)\}
By
Latex:
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)p (Path\_((A)p)p (q)p q))p
(id-fiber-center(G;A))p q))tau++\}\mkleeneclose{}\mcdot{}
Home
Index