Step
*
2
1
1
1
1
1
1
1
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))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. I : fset(ℕ)
10. alpha : K(I)
11. a4 : (A)tau(alpha)
12. u : ((A)tau)p(<alpha, a4>)
13. a5 : J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u1:Point(dM(J)) ⟶ (((A)tau)p)p(f((<alpha, a4>;u)))
14. ∀J,K1:fset(ℕ). ∀f:J ⟶ I. ∀g:K1 ⟶ J. ∀u1:Point(dM(J)).
((a5 J f u1 f((<alpha, a4>;u)) g) = (a5 K1 f ⋅ g (u1 f((<alpha, a4>;u)) g)) ∈ (((A)tau)p)p(g(f((<alpha, a4>;u)))))
15. ((a5 I 1 0) = (q)p((<alpha, a4>;u)) ∈ (((A)tau)p)p((<alpha, a4>;u)))
∧ ((a5 I 1 1) = q((<alpha, a4>;u)) ∈ (((A)tau)p)p((<alpha, a4>;u)))
16. a1 : 𝕀(<<alpha, a4>, u, a5>)
⊢ a5 I 1 ⋅ 1 a1 ∈ ((((A)tau)p)p)p((((alpha;a4);(u;a5));a1))
BY
{ InferEqualType }
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. I : fset(ℕ)
10. alpha : K(I)
11. a4 : (A)tau(alpha)
12. u : ((A)tau)p(<alpha, a4>)
13. a5 : J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u1:Point(dM(J)) ⟶ (((A)tau)p)p(f((<alpha, a4>;u)))
14. ∀J,K1:fset(ℕ). ∀f:J ⟶ I. ∀g:K1 ⟶ J. ∀u1:Point(dM(J)).
((a5 J f u1 f((<alpha, a4>;u)) g) = (a5 K1 f ⋅ g (u1 f((<alpha, a4>;u)) g)) ∈ (((A)tau)p)p(g(f((<alpha, a4>;u)))))
15. ((a5 I 1 0) = (q)p((<alpha, a4>;u)) ∈ (((A)tau)p)p((<alpha, a4>;u)))
∧ ((a5 I 1 1) = q((<alpha, a4>;u)) ∈ (((A)tau)p)p((<alpha, a4>;u)))
16. a1 : 𝕀(<<alpha, a4>, u, a5>)
⊢ (((A)tau)p)p(1 ⋅ 1((<alpha, a4>;u))) = ((((A)tau)p)p)p((((alpha;a4);(u;a5));a1)) ∈ Type
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)}
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. I : fset(ℕ)
10. alpha : K(I)
11. a4 : (A)tau(alpha)
12. u : ((A)tau)p(<alpha, a4>)
13. a5 : J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u1:Point(dM(J)) ⟶ (((A)tau)p)p(f((<alpha, a4>;u)))
14. ∀J,K1:fset(ℕ). ∀f:J ⟶ I. ∀g:K1 ⟶ J. ∀u1:Point(dM(J)).
((a5 J f u1 f((<alpha, a4>;u)) g) = (a5 K1 f ⋅ g (u1 f((<alpha, a4>;u)) g)) ∈ (((A)tau)p)p(g(f((<alpha, a4>;u)))))
15. ((a5 I 1 0) = (q)p((<alpha, a4>;u)) ∈ (((A)tau)p)p((<alpha, a4>;u)))
∧ ((a5 I 1 1) = q((<alpha, a4>;u)) ∈ (((A)tau)p)p((<alpha, a4>;u)))
16. a1 : 𝕀(<<alpha, a4>, u, a5>)
17. (((A)tau)p)p(1 ⋅ 1((<alpha, a4>;u))) = ((((A)tau)p)p)p((((alpha;a4);(u;a5));a1)) ∈ Type
⊢ a5 I 1 ⋅ 1 a1 ∈ (((A)tau)p)p(1 ⋅ 1((<alpha, a4>;u)))
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\}
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. I : fset(\mBbbN{})
10. alpha : K(I)
11. a4 : (A)tau(alpha)
12. u : ((A)tau)p(<alpha, a4>)
13. a5 : J:fset(\mBbbN{}) {}\mrightarrow{} f:J {}\mrightarrow{} I {}\mrightarrow{} u1:Point(dM(J)) {}\mrightarrow{} (((A)tau)p)p(f((<alpha, a4>u)))
14. \mforall{}J,K1:fset(\mBbbN{}). \mforall{}f:J {}\mrightarrow{} I. \mforall{}g:K1 {}\mrightarrow{} J. \mforall{}u1:Point(dM(J)).
((a5 J f u1 f((<alpha, a4>u)) g) = (a5 K1 f \mcdot{} g (u1 f((<alpha, a4>u)) g)))
15. ((a5 I 1 0) = (q)p((<alpha, a4>u))) \mwedge{} ((a5 I 1 1) = q((<alpha, a4>u)))
16. a1 : \mBbbI{}(<<alpha, a4>, u, a5>)
\mvdash{} a5 I 1 \mcdot{} 1 a1 \mmember{} ((((A)tau)p)p)p((((alpha;a4);(u;a5));a1))
By
Latex:
InferEqualType
Home
Index