Step
*
1
1
1
1
1
2
3
1
1
1
1
6
1
2
1
1
1
2
1
1
1
of Lemma
comp-op-to-comp-fun-inverse
1. Gamma : CubicalSet{j}
2. A1 : I:fset(ℕ) ⟶ Gamma(I) ⟶ Type
3. A2 : I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:Gamma(I) ⟶ (A1 I a) ⟶ (A1 J f(a))
4. let A,F = <A1, A2>
in (∀I:fset(ℕ). ∀a:Gamma(I). ∀u:A I a. ((F I I 1 a u) = u ∈ (A I a)))
∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:Gamma(I). ∀u:A I a.
((F I K f ⋅ g a u) = (F J K g f(a) (F I J f a u)) ∈ (A K f ⋅ g(a))))
5. cA : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I}
⟶ rho:Gamma(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(<A1, A2>)<rho> o iota}
⟶ cubical-path-0(Gamma;<A1, A2>;I;i;rho;phi;u)
⟶ cubical-path-1(Gamma;<A1, A2>;I;i;rho;phi;u)
6. ∀I,J:fset(ℕ). ∀i:{i:ℕ| ¬i ∈ I} . ∀j:{j:ℕ| ¬j ∈ J} . ∀g:J ⟶ I. ∀rho:Gamma(I+i). ∀phi:𝔽(I).
∀u:{I+i,s(phi) ⊢ _:(<A1, A2>)<rho> o iota}. ∀a0:cubical-path-0(Gamma;<A1, A2>;I;i;rho;phi;u).
((cA I i rho phi u a0 (i1)(rho) g)
= (cA J j g,i=j(rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
∈ <A1, A2>(g((i1)(rho))))
7. I : fset(ℕ)
8. i : {i:ℕ| ¬i ∈ I}
9. rho : Gamma(I+i)
10. phi : 𝔽(I)
11. u : {I+i,s(phi) ⊢ _:(<A1, A2>)<rho>}
12. x : cubical-path-0(Gamma;<A1, A2>;I;i;rho;phi;u)
13. <new-name(I)> ∈ 𝕀(s(1))
14. (cA I i rho phi u x (i1)(rho) 1)
= (cA I new-name(I) 1,i=new-name(I)(rho) 1(phi) (u)subset-trans(I+i;I+new-name(I);1,i=new-name(I);s(phi))
(x (i0)(rho) 1))
∈ <A1, A2>(1((i1)(rho)))
15. ∀xx:Top. ((cube+(I;i) xx (s(1);<new-name(I)>)) = 1,i=new-name(I) ∈ I+new-name(I) ⟶ I+i)
16. (<rho> o cube+(I;i))(s(1);<new-name(I)>) = 1,i=new-name(I)(rho) ∈ Gamma(I+new-name(I))
17. (u)subset-trans(I+i;I+new-name(I);1,i=new-name(I);s(phi))
= ((u)cube+(I;i))<(s(1);<new-name(I)>)>
∈ (I1:fset(ℕ) ⟶ a:I+new-name(I),s((phi)<1>)(I1) ⟶ (<A1, A2>)<1,i=new-name(I)(rho)>(a))
18. I1 : fset(ℕ)
19. J : fset(ℕ)
20. f : J ⟶ I1
21. a : I+new-name(I),(s(phi))<1,i=new-name(I)>(I1)
22. x1 : A1 I1 (<1,i=new-name(I)(rho)> I1 a)
⊢ (A1 J f(<1,i=new-name(I)(rho)> I1 a)) = (A1 J (<1,i=new-name(I)(rho)> J f(a))) ∈ Type
BY
{ EqCDA }
1
.....subterm..... T:t
2:n
1. Gamma : CubicalSet{j}
2. A1 : I:fset(ℕ) ⟶ Gamma(I) ⟶ Type
3. A2 : I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:Gamma(I) ⟶ (A1 I a) ⟶ (A1 J f(a))
4. let A,F = <A1, A2>
in (∀I:fset(ℕ). ∀a:Gamma(I). ∀u:A I a. ((F I I 1 a u) = u ∈ (A I a)))
∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:Gamma(I). ∀u:A I a.
((F I K f ⋅ g a u) = (F J K g f(a) (F I J f a u)) ∈ (A K f ⋅ g(a))))
5. cA : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I}
⟶ rho:Gamma(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(<A1, A2>)<rho> o iota}
⟶ cubical-path-0(Gamma;<A1, A2>;I;i;rho;phi;u)
⟶ cubical-path-1(Gamma;<A1, A2>;I;i;rho;phi;u)
6. ∀I,J:fset(ℕ). ∀i:{i:ℕ| ¬i ∈ I} . ∀j:{j:ℕ| ¬j ∈ J} . ∀g:J ⟶ I. ∀rho:Gamma(I+i). ∀phi:𝔽(I).
∀u:{I+i,s(phi) ⊢ _:(<A1, A2>)<rho> o iota}. ∀a0:cubical-path-0(Gamma;<A1, A2>;I;i;rho;phi;u).
((cA I i rho phi u a0 (i1)(rho) g)
= (cA J j g,i=j(rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
∈ <A1, A2>(g((i1)(rho))))
7. I : fset(ℕ)
8. i : {i:ℕ| ¬i ∈ I}
9. rho : Gamma(I+i)
10. phi : 𝔽(I)
11. u : {I+i,s(phi) ⊢ _:(<A1, A2>)<rho>}
12. x : cubical-path-0(Gamma;<A1, A2>;I;i;rho;phi;u)
13. <new-name(I)> ∈ 𝕀(s(1))
14. (cA I i rho phi u x (i1)(rho) 1)
= (cA I new-name(I) 1,i=new-name(I)(rho) 1(phi) (u)subset-trans(I+i;I+new-name(I);1,i=new-name(I);s(phi))
(x (i0)(rho) 1))
∈ <A1, A2>(1((i1)(rho)))
15. ∀xx:Top. ((cube+(I;i) xx (s(1);<new-name(I)>)) = 1,i=new-name(I) ∈ I+new-name(I) ⟶ I+i)
16. (<rho> o cube+(I;i))(s(1);<new-name(I)>) = 1,i=new-name(I)(rho) ∈ Gamma(I+new-name(I))
17. (u)subset-trans(I+i;I+new-name(I);1,i=new-name(I);s(phi))
= ((u)cube+(I;i))<(s(1);<new-name(I)>)>
∈ (I1:fset(ℕ) ⟶ a:I+new-name(I),s((phi)<1>)(I1) ⟶ (<A1, A2>)<1,i=new-name(I)(rho)>(a))
18. I1 : fset(ℕ)
19. J : fset(ℕ)
20. f : J ⟶ I1
21. a : I+new-name(I),(s(phi))<1,i=new-name(I)>(I1)
22. x1 : A1 I1 (<1,i=new-name(I)(rho)> I1 a)
⊢ f(<1,i=new-name(I)(rho)> I1 a) = (<1,i=new-name(I)(rho)> J f(a)) ∈ Gamma(J)
Latex:
Latex:
1. Gamma : CubicalSet\{j\}
2. A1 : I:fset(\mBbbN{}) {}\mrightarrow{} Gamma(I) {}\mrightarrow{} Type
3. A2 : I:fset(\mBbbN{}) {}\mrightarrow{} J:fset(\mBbbN{}) {}\mrightarrow{} f:J {}\mrightarrow{} I {}\mrightarrow{} a:Gamma(I) {}\mrightarrow{} (A1 I a) {}\mrightarrow{} (A1 J f(a))
4. let A,F = <A1, A2>
in (\mforall{}I:fset(\mBbbN{}). \mforall{}a:Gamma(I). \mforall{}u:A I a. ((F I I 1 a u) = u))
\mwedge{} (\mforall{}I,J,K:fset(\mBbbN{}). \mforall{}f:J {}\mrightarrow{} I. \mforall{}g:K {}\mrightarrow{} J. \mforall{}a:Gamma(I). \mforall{}u:A I a.
((F I K f \mcdot{} g a u) = (F J K g f(a) (F I J f a u))))
5. cA : I:fset(\mBbbN{})
{}\mrightarrow{} i:\{i:\mBbbN{}| \mneg{}i \mmember{} I\}
{}\mrightarrow{} rho:Gamma(I+i)
{}\mrightarrow{} phi:\mBbbF{}(I)
{}\mrightarrow{} u:\{I+i,s(phi) \mvdash{} \_:(<A1, A2>)<rho> o iota\}
{}\mrightarrow{} cubical-path-0(Gamma;<A1, A2>I;i;rho;phi;u)
{}\mrightarrow{} cubical-path-1(Gamma;<A1, A2>I;i;rho;phi;u)
6. \mforall{}I,J:fset(\mBbbN{}). \mforall{}i:\{i:\mBbbN{}| \mneg{}i \mmember{} I\} . \mforall{}j:\{j:\mBbbN{}| \mneg{}j \mmember{} J\} . \mforall{}g:J {}\mrightarrow{} I. \mforall{}rho:Gamma(I+i). \mforall{}phi:\mBbbF{}(I).
\mforall{}u:\{I+i,s(phi) \mvdash{} \_:(<A1, A2>)<rho> o iota\}. \mforall{}a0:cubical-path-0(Gamma;<A1, A2>I;i;rho;phi;u).
((cA I i rho phi u a0 (i1)(rho) g)
= (cA J j g,i=j(rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)(rho) g)))
7. I : fset(\mBbbN{})
8. i : \{i:\mBbbN{}| \mneg{}i \mmember{} I\}
9. rho : Gamma(I+i)
10. phi : \mBbbF{}(I)
11. u : \{I+i,s(phi) \mvdash{} \_:(<A1, A2>)<rho>\}
12. x : cubical-path-0(Gamma;<A1, A2>I;i;rho;phi;u)
13. <new-name(I)> \mmember{} \mBbbI{}(s(1))
14. (cA I i rho phi u x (i1)(rho) 1)
= (cA I new-name(I) 1,i=new-name(I)(rho) 1(phi)
(u)subset-trans(I+i;I+new-name(I);1,i=new-name(I);s(phi))
(x (i0)(rho) 1))
15. \mforall{}xx:Top. ((cube+(I;i) xx (s(1);<new-name(I)>)) = 1,i=new-name(I))
16. (<rho> o cube+(I;i))(s(1);<new-name(I)>) = 1,i=new-name(I)(rho)
17. (u)subset-trans(I+i;I+new-name(I);1,i=new-name(I);s(phi))
= ((u)cube+(I;i))<(s(1);<new-name(I)>)>
18. I1 : fset(\mBbbN{})
19. J : fset(\mBbbN{})
20. f : J {}\mrightarrow{} I1
21. a : I+new-name(I),(s(phi))ə,i=new-name(I)>(I1)
22. x1 : A1 I1 (ə,i=new-name(I)(rho)> I1 a)
\mvdash{} (A1 J f(ə,i=new-name(I)(rho)> I1 a)) = (A1 J (ə,i=new-name(I)(rho)> J f(a)))
By
Latex:
EqCDA
Home
Index