Step
*
2
1
1
2
1
1
1
1
1
1
4
1
1
1
1
1
1
1
1
1
of Lemma
csm-id-fiber-contraction
.....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)}
9. path-eta(id-fiber-contraction(K;(A)tau)).1
= path-eta((id-fiber-contraction(G;A))tau++).1
∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _:((((A)tau)p)p)p}
10. path-eta(id-fiber-contraction(K;(A)tau)).2 ∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _
:((Path_(((A)tau)p)p (q)p q))
(p o p;path-eta(id-fiber-contraction(K;(A)tau)).1)}
11. ∀[u:{K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _:(((A)tau)p)p o p}]
(((Path_(((A)tau)p)p (q)p q))(p o p;u)
= (K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ Path_(((A)tau)p)p o p (q)p o p u)
∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _})
12. ((Path_(((A)tau)p)p (q)p q))(p o p;path-eta(id-fiber-contraction(K;(A)tau)).1)
= (K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ Path_((((A)tau)p)p)p ((q)p)p
path-eta(id-fiber-contraction(K;(A)tau)).1)
∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _}
13. {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _
:((Path_(((A)tau)p)p (q)p q))(p o p;path-eta(id-fiber-contraction(K;(A)tau)).1)}
= {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _
:(Path_((((A)tau)p)p)p ((q)p)p path-eta(id-fiber-contraction(K;(A)tau)).1)}
∈ 𝕌{[i' | j']}
14. path-eta(id-fiber-contraction(K;(A)tau)).2 ∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _
:(Path_((((A)tau)p)p)p ((q)p)p
path-eta(id-fiber-contraction(K;(A)tau)).1)}
15. 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}
16. ((Σ ((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).𝕀 ⊢ _}
17. 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)}
18. path-eta((id-fiber-contraction(G;A))tau++).2 ∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _
:((Path_(((A)tau)p)p (q)p q))
(p o p;path-eta((id-fiber-contraction(G;A))tau++).1)}
19. ((Path_(((A)tau)p)p (q)p q))(p o p;path-eta((id-fiber-contraction(G;A))tau++).1)
= (K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ Path_((((A)tau)p)p)p ((q)p)p
path-eta((id-fiber-contraction(G;A))tau++).1)
∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _}
⊢ path-eta((id-fiber-contraction(G;A))tau++).2 ∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _
:(Path_((((A)tau)p)p)p ((q)p)p
path-eta((id-fiber-contraction(G;A))tau++).1)}
BY
{ (InferEqualType THEN Try (Trivial)) }
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}
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)}
9. path-eta(id-fiber-contraction(K;(A)tau)).1
= path-eta((id-fiber-contraction(G;A))tau++).1
∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _:((((A)tau)p)p)p}
10. path-eta(id-fiber-contraction(K;(A)tau)).2 ∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _
:((Path_(((A)tau)p)p (q)p q))
(p o p;path-eta(id-fiber-contraction(K;(A)tau)).1)}
11. ∀[u:{K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _:(((A)tau)p)p o p}]
(((Path_(((A)tau)p)p (q)p q))(p o p;u)
= (K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ Path_(((A)tau)p)p o p (q)p o p u)
∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _})
12. ((Path_(((A)tau)p)p (q)p q))(p o p;path-eta(id-fiber-contraction(K;(A)tau)).1)
= (K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ Path_((((A)tau)p)p)p ((q)p)p
path-eta(id-fiber-contraction(K;(A)tau)).1)
∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _}
13. {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _
:((Path_(((A)tau)p)p (q)p q))(p o p;path-eta(id-fiber-contraction(K;(A)tau)).1)}
= {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _
:(Path_((((A)tau)p)p)p ((q)p)p path-eta(id-fiber-contraction(K;(A)tau)).1)}
∈ 𝕌{[i' | j']}
14. path-eta(id-fiber-contraction(K;(A)tau)).2 ∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _
:(Path_((((A)tau)p)p)p ((q)p)p
path-eta(id-fiber-contraction(K;(A)tau)).1)}
15. 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}
16. ((Σ ((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).𝕀 ⊢ _}
17. 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)}
18. path-eta((id-fiber-contraction(G;A))tau++).2 ∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _
:((Path_(((A)tau)p)p (q)p q))
(p o p;path-eta((id-fiber-contraction(G;A))tau++).1)}
19. ((Path_(((A)tau)p)p (q)p q))(p o p;path-eta((id-fiber-contraction(G;A))tau++).1)
= (K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ Path_((((A)tau)p)p)p ((q)p)p
path-eta((id-fiber-contraction(G;A))tau++).1)
∈ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _}
⊢ {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _
:((Path_(((A)tau)p)p (q)p q))(p o p;path-eta((id-fiber-contraction(G;A))tau++).1)}
= {K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 ⊢ _
:(Path_((((A)tau)p)p)p ((q)p)p path-eta((id-fiber-contraction(G;A))tau++).1)}
∈ 𝕌{[i' | j']}
Latex:
Latex:
.....assertion.....
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\}
7. ((\mSigma{} ((A)tau)p (Path\_(((A)tau)p)p (q)p q))p)p
= \mSigma{} ((((A)tau)p)p)p ((Path\_(((A)tau)p)p (q)p q))(p o p o p;q)
8. 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)\}
9. path-eta(id-fiber-contraction(K;(A)tau)).1 = path-eta((id-fiber-contraction(G;A))tau++).1
10. path-eta(id-fiber-contraction(K;(A)tau)).2
\mmember{} \{K.(A)tau.\mSigma{} ((A)tau)p (Path\_(((A)tau)p)p (q)p q).\mBbbI{} \mvdash{} \_
:((Path\_(((A)tau)p)p (q)p q))(p o p;path-eta(id-fiber-contraction(K;(A)tau)).1)\}
11. \mforall{}[u:\{K.(A)tau.\mSigma{} ((A)tau)p (Path\_(((A)tau)p)p (q)p q).\mBbbI{} \mvdash{} \_:(((A)tau)p)p o p\}]
(((Path\_(((A)tau)p)p (q)p q))(p o p;u)
= (K.(A)tau.\mSigma{} ((A)tau)p (Path\_(((A)tau)p)p (q)p q).\mBbbI{} \mvdash{} Path\_(((A)tau)p)p o p (q)p o p u))
12. ((Path\_(((A)tau)p)p (q)p q))(p o p;path-eta(id-fiber-contraction(K;(A)tau)).1)
= (K.(A)tau.\mSigma{} ((A)tau)p (Path\_(((A)tau)p)p (q)p
q).\mBbbI{} \mvdash{} Path\_((((A)tau)p)p)p ((q)p)p
path-eta(id-fiber-contraction(K;(A)tau)).1)
13. \{K.(A)tau.\mSigma{} ((A)tau)p (Path\_(((A)tau)p)p (q)p q).\mBbbI{} \mvdash{} \_
:((Path\_(((A)tau)p)p (q)p q))(p o p;path-eta(id-fiber-contraction(K;(A)tau)).1)\}
= \{K.(A)tau.\mSigma{} ((A)tau)p (Path\_(((A)tau)p)p (q)p q).\mBbbI{} \mvdash{} \_
:(Path\_((((A)tau)p)p)p ((q)p)p path-eta(id-fiber-contraction(K;(A)tau)).1)\}
14. path-eta(id-fiber-contraction(K;(A)tau)).2
\mmember{} \{K.(A)tau.\mSigma{} ((A)tau)p (Path\_(((A)tau)p)p (q)p q).\mBbbI{} \mvdash{} \_
:(Path\_((((A)tau)p)p)p ((q)p)p path-eta(id-fiber-contraction(K;(A)tau)).1)\}
15. path-eta((id-fiber-contraction(G;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\}
16. ((\mSigma{} ((A)tau)p (Path\_(((A)tau)p)p (q)p q))p)p
= \mSigma{} ((((A)tau)p)p)p ((Path\_(((A)tau)p)p (q)p q))(p o p o p;q)
17. path-eta((id-fiber-contraction(G;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)\}
18. path-eta((id-fiber-contraction(G;A))tau++).2
\mmember{} \{K.(A)tau.\mSigma{} ((A)tau)p (Path\_(((A)tau)p)p (q)p q).\mBbbI{} \mvdash{} \_
:((Path\_(((A)tau)p)p (q)p q))(p o p;path-eta((id-fiber-contraction(G;A))tau++).1)\}
19. ((Path\_(((A)tau)p)p (q)p q))(p o p;path-eta((id-fiber-contraction(G;A))tau++).1)
= (K.(A)tau.\mSigma{} ((A)tau)p (Path\_(((A)tau)p)p (q)p
q).\mBbbI{} \mvdash{} Path\_((((A)tau)p)p)p ((q)p)p
path-eta((id-fiber-contraction(G;A))tau++).1)
\mvdash{} path-eta((id-fiber-contraction(G;A))tau++).2
\mmember{} \{K.(A)tau.\mSigma{} ((A)tau)p (Path\_(((A)tau)p)p (q)p q).\mBbbI{} \mvdash{} \_
:(Path\_((((A)tau)p)p)p ((q)p)p path-eta((id-fiber-contraction(G;A))tau++).1)\}
By
Latex:
(InferEqualType THEN Try (Trivial))
Home
Index