Step
*
1
2
of Lemma
composition-op-nc-e
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. comp : Gamma ⊢ CompOp(A)
4. I : fset(ℕ)
5. i : {i:ℕ| ¬i ∈ I}
6. j : {j:ℕ| ¬j ∈ I}
7. ∀g:I ⟶ I. ∀rho:Gamma(I+i). ∀phi:𝔽(I). ∀u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}.
∀a0:cubical-path-0(Gamma;A;I;i;rho;phi;u).
((comp I i rho phi u a0 (i1)(rho) g)
= (comp I j g,i=j(rho) g(phi) (u)subset-trans(I+i;I+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
∈ A(g((i1)(rho))))
8. rho : Gamma(I+i)
9. phi : 𝔽(I)
10. u : {I+i,s(phi) ⊢ _:(A)<rho> o iota}
11. a0 : cubical-path-0(Gamma;A;I;i;rho;phi;u)
12. (comp I i rho phi u a0 (i1)(rho) 1)
= (comp I j e(i;j)(rho) 1(phi) (u)subset-trans(I+i;I+j;e(i;j);s(phi)) (a0 (i0)(rho) 1))
∈ A(1((i1)(rho)))
13. A((i1)(rho)) = A((j1)(e(i;j)(rho))) ∈ Type
14. comp I i rho phi u a0 ∈ {a1:A((i1)(rho))| cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1)}
15. (u)subset-trans(I+i;I+j;e(i;j);s(phi)) ∈ {I+j,s(1(phi)) ⊢ _:(A)<e(i;j)(rho)> o iota}
⊢ (comp I i rho phi u a0) = (comp I j e(i;j)(rho) phi (u)subset-trans(I+i;I+j;e(i;j);s(phi)) a0) ∈ A((i1)(rho))
BY
{ (NthHypEqGen (-4) THEN EqCD THEN Try (Trivial)) }
1
.....subterm..... T:t
1:n
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. comp : Gamma ⊢ CompOp(A)
4. I : fset(ℕ)
5. i : {i:ℕ| ¬i ∈ I}
6. j : {j:ℕ| ¬j ∈ I}
7. ∀g:I ⟶ I. ∀rho:Gamma(I+i). ∀phi:𝔽(I). ∀u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}.
∀a0:cubical-path-0(Gamma;A;I;i;rho;phi;u).
((comp I i rho phi u a0 (i1)(rho) g)
= (comp I j g,i=j(rho) g(phi) (u)subset-trans(I+i;I+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
∈ A(g((i1)(rho))))
8. rho : Gamma(I+i)
9. phi : 𝔽(I)
10. u : {I+i,s(phi) ⊢ _:(A)<rho> o iota}
11. a0 : cubical-path-0(Gamma;A;I;i;rho;phi;u)
12. (comp I i rho phi u a0 (i1)(rho) 1)
= (comp I j e(i;j)(rho) 1(phi) (u)subset-trans(I+i;I+j;e(i;j);s(phi)) (a0 (i0)(rho) 1))
∈ A(1((i1)(rho)))
13. A((i1)(rho)) = A((j1)(e(i;j)(rho))) ∈ Type
14. comp I i rho phi u a0 ∈ {a1:A((i1)(rho))| cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1)}
15. (u)subset-trans(I+i;I+j;e(i;j);s(phi)) ∈ {I+j,s(1(phi)) ⊢ _:(A)<e(i;j)(rho)> o iota}
⊢ A(1((i1)(rho))) = A(1((i1)(rho))) ∈ Type
2
.....subterm..... T:t
2:n
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. comp : Gamma ⊢ CompOp(A)
4. I : fset(ℕ)
5. i : {i:ℕ| ¬i ∈ I}
6. j : {j:ℕ| ¬j ∈ I}
7. ∀g:I ⟶ I. ∀rho:Gamma(I+i). ∀phi:𝔽(I). ∀u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}.
∀a0:cubical-path-0(Gamma;A;I;i;rho;phi;u).
((comp I i rho phi u a0 (i1)(rho) g)
= (comp I j g,i=j(rho) g(phi) (u)subset-trans(I+i;I+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
∈ A(g((i1)(rho))))
8. rho : Gamma(I+i)
9. phi : 𝔽(I)
10. u : {I+i,s(phi) ⊢ _:(A)<rho> o iota}
11. a0 : cubical-path-0(Gamma;A;I;i;rho;phi;u)
12. (comp I i rho phi u a0 (i1)(rho) 1)
= (comp I j e(i;j)(rho) 1(phi) (u)subset-trans(I+i;I+j;e(i;j);s(phi)) (a0 (i0)(rho) 1))
∈ A(1((i1)(rho)))
13. A((i1)(rho)) = A((j1)(e(i;j)(rho))) ∈ Type
14. comp I i rho phi u a0 ∈ {a1:A((i1)(rho))| cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1)}
15. (u)subset-trans(I+i;I+j;e(i;j);s(phi)) ∈ {I+j,s(1(phi)) ⊢ _:(A)<e(i;j)(rho)> o iota}
⊢ (comp I i rho phi u a0) = (comp I i rho phi u a0 (i1)(rho) 1) ∈ A(1((i1)(rho)))
3
.....subterm..... T:t
3:n
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. comp : Gamma ⊢ CompOp(A)
4. I : fset(ℕ)
5. i : {i:ℕ| ¬i ∈ I}
6. j : {j:ℕ| ¬j ∈ I}
7. ∀g:I ⟶ I. ∀rho:Gamma(I+i). ∀phi:𝔽(I). ∀u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}.
∀a0:cubical-path-0(Gamma;A;I;i;rho;phi;u).
((comp I i rho phi u a0 (i1)(rho) g)
= (comp I j g,i=j(rho) g(phi) (u)subset-trans(I+i;I+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
∈ A(g((i1)(rho))))
8. rho : Gamma(I+i)
9. phi : 𝔽(I)
10. u : {I+i,s(phi) ⊢ _:(A)<rho> o iota}
11. a0 : cubical-path-0(Gamma;A;I;i;rho;phi;u)
12. (comp I i rho phi u a0 (i1)(rho) 1)
= (comp I j e(i;j)(rho) 1(phi) (u)subset-trans(I+i;I+j;e(i;j);s(phi)) (a0 (i0)(rho) 1))
∈ A(1((i1)(rho)))
13. A((i1)(rho)) = A((j1)(e(i;j)(rho))) ∈ Type
14. comp I i rho phi u a0 ∈ {a1:A((i1)(rho))| cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1)}
15. (u)subset-trans(I+i;I+j;e(i;j);s(phi)) ∈ {I+j,s(1(phi)) ⊢ _:(A)<e(i;j)(rho)> o iota}
⊢ (comp I j e(i;j)(rho) phi (u)subset-trans(I+i;I+j;e(i;j);s(phi)) a0)
= (comp I j e(i;j)(rho) 1(phi) (u)subset-trans(I+i;I+j;e(i;j);s(phi)) (a0 (i0)(rho) 1))
∈ A(1((i1)(rho)))
Latex:
Latex:
1. Gamma : CubicalSet\{j\}
2. A : \{Gamma \mvdash{} \_\}
3. comp : Gamma \mvdash{} CompOp(A)
4. I : fset(\mBbbN{})
5. i : \{i:\mBbbN{}| \mneg{}i \mmember{} I\}
6. j : \{j:\mBbbN{}| \mneg{}j \mmember{} I\}
7. \mforall{}g:I {}\mrightarrow{} I. \mforall{}rho:Gamma(I+i). \mforall{}phi:\mBbbF{}(I). \mforall{}u:\{I+i,s(phi) \mvdash{} \_:(A)<rho> o iota\}.
\mforall{}a0:cubical-path-0(Gamma;A;I;i;rho;phi;u).
((comp I i rho phi u a0 (i1)(rho) g)
= (comp I j g,i=j(rho) g(phi) (u)subset-trans(I+i;I+j;g,i=j;s(phi)) (a0 (i0)(rho) g)))
8. rho : Gamma(I+i)
9. phi : \mBbbF{}(I)
10. u : \{I+i,s(phi) \mvdash{} \_:(A)<rho> o iota\}
11. a0 : cubical-path-0(Gamma;A;I;i;rho;phi;u)
12. (comp I i rho phi u a0 (i1)(rho) 1)
= (comp I j e(i;j)(rho) 1(phi) (u)subset-trans(I+i;I+j;e(i;j);s(phi)) (a0 (i0)(rho) 1))
13. A((i1)(rho)) = A((j1)(e(i;j)(rho)))
14. comp I i rho phi u a0 \mmember{} \{a1:A((i1)(rho))| cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1)\}
15. (u)subset-trans(I+i;I+j;e(i;j);s(phi)) \mmember{} \{I+j,s(1(phi)) \mvdash{} \_:(A)<e(i;j)(rho)> o iota\}
\mvdash{} (comp I i rho phi u a0) = (comp I j e(i;j)(rho) phi (u)subset-trans(I+i;I+j;e(i;j);s(phi)) a0)
By
Latex:
(NthHypEqGen (-4) THEN EqCD THEN Try (Trivial))
Home
Index