Step
*
2
1
1
1
6
1
1
2
1
2
3
4
4
of Lemma
csm-id-fiber-contraction
.....subterm..... T:t
1:n
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
∈ (I:fset(ℕ) ⟶ a:K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀(I) ⟶ ((((A)tau)p)p)p(a))
10. ∀[X:cubical_set{[i | [j | i]]:l}]. ∀[A:{X ⊢ _}]. ∀[u:{X ⊢ _:A}]. ∀[z:I:fset(ℕ) ⟶ a:X(I) ⟶ A(a)].
u = z ∈ {X ⊢ _:A} supposing u = z ∈ (I:fset(ℕ) ⟶ a:X(I) ⟶ A(a))
11. v : {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)}
12. id-fiber-contraction(K;(A)tau)
= v
∈ {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)}
13. ∀[pth:{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(pth) ∈ {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})
14. path-eta(v) ∈ {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}
15. ((Σ ((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).𝕀 ⊢ _}
16. path-eta(v) ∈ {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)}
⊢ p o p o p ∈ K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀.((((A)tau)p)p)p ij⟶ K.(A)tau
BY
{ MemCD }
1
.....subterm..... T:t
1:n
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
∈ (I:fset(ℕ) ⟶ a:K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀(I) ⟶ ((((A)tau)p)p)p(a))
10. ∀[X:cubical_set{[i | [j | i]]:l}]. ∀[A:{X ⊢ _}]. ∀[u:{X ⊢ _:A}]. ∀[z:I:fset(ℕ) ⟶ a:X(I) ⟶ A(a)].
u = z ∈ {X ⊢ _:A} supposing u = z ∈ (I:fset(ℕ) ⟶ a:X(I) ⟶ A(a))
11. v : {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)}
12. id-fiber-contraction(K;(A)tau)
= v
∈ {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)}
13. ∀[pth:{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(pth) ∈ {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})
14. path-eta(v) ∈ {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}
15. ((Σ ((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).𝕀 ⊢ _}
16. path-eta(v) ∈ {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)}
⊢ K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀.((((A)tau)p)p)p cubical_set{[j | i]:l}
2
.....subterm..... T:t
2:n
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
∈ (I:fset(ℕ) ⟶ a:K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀(I) ⟶ ((((A)tau)p)p)p(a))
10. ∀[X:cubical_set{[i | [j | i]]:l}]. ∀[A:{X ⊢ _}]. ∀[u:{X ⊢ _:A}]. ∀[z:I:fset(ℕ) ⟶ a:X(I) ⟶ A(a)].
u = z ∈ {X ⊢ _:A} supposing u = z ∈ (I:fset(ℕ) ⟶ a:X(I) ⟶ A(a))
11. v : {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)}
12. id-fiber-contraction(K;(A)tau)
= v
∈ {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)}
13. ∀[pth:{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(pth) ∈ {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})
14. path-eta(v) ∈ {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}
15. ((Σ ((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).𝕀 ⊢ _}
16. path-eta(v) ∈ {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)}
⊢ K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀 cubical_set{[j | i]:l}
3
.....subterm..... T:t
3:n
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
∈ (I:fset(ℕ) ⟶ a:K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀(I) ⟶ ((((A)tau)p)p)p(a))
10. ∀[X:cubical_set{[i | [j | i]]:l}]. ∀[A:{X ⊢ _}]. ∀[u:{X ⊢ _:A}]. ∀[z:I:fset(ℕ) ⟶ a:X(I) ⟶ A(a)].
u = z ∈ {X ⊢ _:A} supposing u = z ∈ (I:fset(ℕ) ⟶ a:X(I) ⟶ A(a))
11. v : {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)}
12. id-fiber-contraction(K;(A)tau)
= v
∈ {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)}
13. ∀[pth:{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(pth) ∈ {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})
14. path-eta(v) ∈ {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}
15. ((Σ ((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).𝕀 ⊢ _}
16. path-eta(v) ∈ {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)}
⊢ K.(A)tau cubical_set{[j | i]:l}
4
.....subterm..... T:t
4:n
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
∈ (I:fset(ℕ) ⟶ a:K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀(I) ⟶ ((((A)tau)p)p)p(a))
10. ∀[X:cubical_set{[i | [j | i]]:l}]. ∀[A:{X ⊢ _}]. ∀[u:{X ⊢ _:A}]. ∀[z:I:fset(ℕ) ⟶ a:X(I) ⟶ A(a)].
u = z ∈ {X ⊢ _:A} supposing u = z ∈ (I:fset(ℕ) ⟶ a:X(I) ⟶ A(a))
11. v : {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)}
12. id-fiber-contraction(K;(A)tau)
= v
∈ {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)}
13. ∀[pth:{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(pth) ∈ {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})
14. path-eta(v) ∈ {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}
15. ((Σ ((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).𝕀 ⊢ _}
16. path-eta(v) ∈ {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)}
⊢ p ∈ cube_set_map{[j | i]:l}(K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀.((((A)tau)p)p)p;
K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀)
5
.....subterm..... T:t
5:n
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
∈ (I:fset(ℕ) ⟶ a:K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀(I) ⟶ ((((A)tau)p)p)p(a))
10. ∀[X:cubical_set{[i | [j | i]]:l}]. ∀[A:{X ⊢ _}]. ∀[u:{X ⊢ _:A}]. ∀[z:I:fset(ℕ) ⟶ a:X(I) ⟶ A(a)].
u = z ∈ {X ⊢ _:A} supposing u = z ∈ (I:fset(ℕ) ⟶ a:X(I) ⟶ A(a))
11. v : {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)}
12. id-fiber-contraction(K;(A)tau)
= v
∈ {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)}
13. ∀[pth:{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(pth) ∈ {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})
14. path-eta(v) ∈ {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}
15. ((Σ ((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).𝕀 ⊢ _}
16. path-eta(v) ∈ {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)}
⊢ p o p ∈ cube_set_map{[j | i]:l}(K.(A)tau.Σ ((A)tau)p (Path_(((A)tau)p)p (q)p q).𝕀; K.(A)tau)
Latex:
Latex:
.....subterm..... T:t
1:n
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. \mforall{}[X:cubical\_set\{[i | [j | i]]:l\}]. \mforall{}[A:\{X \mvdash{} \_\}]. \mforall{}[u:\{X \mvdash{} \_:A\}].
\mforall{}[z:I:fset(\mBbbN{}) {}\mrightarrow{} a:X(I) {}\mrightarrow{} A(a)].
u = z supposing u = z
11. v : \{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 (id-fiber-center(K;(A)tau))p q)\}
12. id-fiber-contraction(K;(A)tau) = v
13. \mforall{}[pth:\{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)\}]
(path-eta(pth) \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\})
14. path-eta(v) \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\}
15. ((\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)
16. path-eta(v) \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)\}
\mvdash{} p o p o p \mmember{} K.(A)tau.\mSigma{} ((A)tau)p (Path\_(((A)tau)p)p (q)p q).\mBbbI{}.((((A)tau)p)p)p ij{}\mrightarrow{} K.(A)tau
By
Latex:
MemCD
Home
Index