Step
*
1
1
1
2
2
1
1
1
1
2
1
2
1
1
2
1
1
1
2
of Lemma
comp-fun-to-comp-op-inverse
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : composition-function{j:l,i:l}(Gamma;A)
4. ∀H,K:j⊢. ∀tau:K j⟶ H. ∀sigma:H.𝕀 j⟶ Gamma. ∀phi:{H ⊢ _:𝔽}. ∀u:{H, phi.𝕀 ⊢ _:(A)sigma}.
∀a0:{H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}.
((cA H sigma phi u a0)tau
= (cA K sigma o tau+ (phi)tau (u)tau+ (a0)tau)
∈ {K ⊢ _:(((A)sigma)[1(𝕀)])tau[(phi)tau |⟶ ((u)[1(𝕀)])tau]})
5. H : CubicalSet{j}
6. sigma : H.𝕀 j⟶ Gamma
7. phi : {H ⊢ _:𝔽}
8. u : {H, phi.𝕀 ⊢ _:(A)sigma}
9. a0 : {H ⊢ _:((A)sigma)[0(𝕀)]}
10. (u)[0(𝕀)] = a0 ∈ {H, phi ⊢ _:((A)sigma)[0(𝕀)]}
11. I : fset(ℕ)
12. a : H(I)
13. (cA H sigma phi u a0)<a>
= (cA formal-cube(I) sigma o <a>+ (phi)<a> (u)<a>+ (a0)<a>)
∈ {formal-cube(I) ⊢ _:(((A)sigma)[1(𝕀)])<a>[(phi)<a> |⟶ ((u)[1(𝕀)])<a>]}
14. (cA H sigma phi u a0)<a>(1) = cA formal-cube(I) sigma o <a>+ (phi)<a> (u)<a>+ (a0)<a>(1) ∈ ((A)sigma)[1(𝕀)](a)
15. (a;0) = (new-name(I)0)((s(a);<new-name(I)>)) ∈ H.𝕀(I)
16. {formal-cube(I) ⊢ _:(((A)sigma)[0(𝕀)])<a>} = {formal-cube(I) ⊢ _:((A)sigma o <a>+)[0(𝕀)]} ∈ 𝕌{[i' | j']}
17. I1 : fset(ℕ)
18. a1 : I1 ⟶ I
19. (sigma)(a;0) = (new-name(I)0)((sigma)(s(a);<new-name(I)>)) ∈ Gamma(I)
20. (sigma)(a;0)
= (new-name(I)0)((sigma)(s(a);<new-name(I)>))
∈ {z:Gamma(I)| (z = (sigma)(a;0) ∈ Gamma(I)) ∧ (z = (new-name(I)0)((sigma)(s(a);<new-name(I)>)) ∈ Gamma(I))}
21. (a0(a) (sigma)(a;0) a1) = (a0(a) (new-name(I)0)((sigma)(s(a);<new-name(I)>)) a1) ∈ (((A)sigma)[0(𝕀)])<a>(a1)
⊢ a0(a1(a)) = (a0(a) (new-name(I)0)((sigma)(s(a);<new-name(I)>)) a1) ∈ (((A)sigma)[0(𝕀)])<a>(a1)
BY
{ (Assert ⌜a0(a1(a)) = (a0(a) (sigma)(a;0) a1) ∈ (((A)sigma)[0(𝕀)])<a>(a1)⌝⋅ THENM Eq) }
1
.....assertion.....
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : composition-function{j:l,i:l}(Gamma;A)
4. ∀H,K:j⊢. ∀tau:K j⟶ H. ∀sigma:H.𝕀 j⟶ Gamma. ∀phi:{H ⊢ _:𝔽}. ∀u:{H, phi.𝕀 ⊢ _:(A)sigma}.
∀a0:{H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}.
((cA H sigma phi u a0)tau
= (cA K sigma o tau+ (phi)tau (u)tau+ (a0)tau)
∈ {K ⊢ _:(((A)sigma)[1(𝕀)])tau[(phi)tau |⟶ ((u)[1(𝕀)])tau]})
5. H : CubicalSet{j}
6. sigma : H.𝕀 j⟶ Gamma
7. phi : {H ⊢ _:𝔽}
8. u : {H, phi.𝕀 ⊢ _:(A)sigma}
9. a0 : {H ⊢ _:((A)sigma)[0(𝕀)]}
10. (u)[0(𝕀)] = a0 ∈ {H, phi ⊢ _:((A)sigma)[0(𝕀)]}
11. I : fset(ℕ)
12. a : H(I)
13. (cA H sigma phi u a0)<a>
= (cA formal-cube(I) sigma o <a>+ (phi)<a> (u)<a>+ (a0)<a>)
∈ {formal-cube(I) ⊢ _:(((A)sigma)[1(𝕀)])<a>[(phi)<a> |⟶ ((u)[1(𝕀)])<a>]}
14. (cA H sigma phi u a0)<a>(1) = cA formal-cube(I) sigma o <a>+ (phi)<a> (u)<a>+ (a0)<a>(1) ∈ ((A)sigma)[1(𝕀)](a)
15. (a;0) = (new-name(I)0)((s(a);<new-name(I)>)) ∈ H.𝕀(I)
16. {formal-cube(I) ⊢ _:(((A)sigma)[0(𝕀)])<a>} = {formal-cube(I) ⊢ _:((A)sigma o <a>+)[0(𝕀)]} ∈ 𝕌{[i' | j']}
17. I1 : fset(ℕ)
18. a1 : I1 ⟶ I
19. (sigma)(a;0) = (new-name(I)0)((sigma)(s(a);<new-name(I)>)) ∈ Gamma(I)
20. (sigma)(a;0)
= (new-name(I)0)((sigma)(s(a);<new-name(I)>))
∈ {z:Gamma(I)| (z = (sigma)(a;0) ∈ Gamma(I)) ∧ (z = (new-name(I)0)((sigma)(s(a);<new-name(I)>)) ∈ Gamma(I))}
21. (a0(a) (sigma)(a;0) a1) = (a0(a) (new-name(I)0)((sigma)(s(a);<new-name(I)>)) a1) ∈ (((A)sigma)[0(𝕀)])<a>(a1)
⊢ a0(a1(a)) = (a0(a) (sigma)(a;0) a1) ∈ (((A)sigma)[0(𝕀)])<a>(a1)
Latex:
Latex:
1. Gamma : CubicalSet\{j\}
2. A : \{Gamma \mvdash{} \_\}
3. cA : composition-function\{j:l,i:l\}(Gamma;A)
4. \mforall{}H,K:j\mvdash{}. \mforall{}tau:K j{}\mrightarrow{} H. \mforall{}sigma:H.\mBbbI{} j{}\mrightarrow{} Gamma. \mforall{}phi:\{H \mvdash{} \_:\mBbbF{}\}. \mforall{}u:\{H, phi.\mBbbI{} \mvdash{} \_:(A)sigma\}.
\mforall{}a0:\{H \mvdash{} \_:((A)sigma)[0(\mBbbI{})][phi |{}\mrightarrow{} (u)[0(\mBbbI{})]]\}.
((cA H sigma phi u a0)tau = (cA K sigma o tau+ (phi)tau (u)tau+ (a0)tau))
5. H : CubicalSet\{j\}
6. sigma : H.\mBbbI{} j{}\mrightarrow{} Gamma
7. phi : \{H \mvdash{} \_:\mBbbF{}\}
8. u : \{H, phi.\mBbbI{} \mvdash{} \_:(A)sigma\}
9. a0 : \{H \mvdash{} \_:((A)sigma)[0(\mBbbI{})]\}
10. (u)[0(\mBbbI{})] = a0
11. I : fset(\mBbbN{})
12. a : H(I)
13. (cA H sigma phi u a0)<a> = (cA formal-cube(I) sigma o <a>+ (phi)<a> (u)<a>+ (a0)<a>)
14. (cA H sigma phi u a0)<a>(1) = cA formal-cube(I) sigma o <a>+ (phi)<a> (u)<a>+ (a0)<a>(1)
15. (a;0) = (new-name(I)0)((s(a);<new-name(I)>))
16. \{formal-cube(I) \mvdash{} \_:(((A)sigma)[0(\mBbbI{})])<a>\} = \{formal-cube(I) \mvdash{} \_:((A)sigma o <a>+)[0(\mBbbI{})]\}
17. I1 : fset(\mBbbN{})
18. a1 : I1 {}\mrightarrow{} I
19. (sigma)(a;0) = (new-name(I)0)((sigma)(s(a);<new-name(I)>))
20. (sigma)(a;0) = (new-name(I)0)((sigma)(s(a);<new-name(I)>))
21. (a0(a) (sigma)(a;0) a1) = (a0(a) (new-name(I)0)((sigma)(s(a);<new-name(I)>)) a1)
\mvdash{} a0(a1(a)) = (a0(a) (new-name(I)0)((sigma)(s(a);<new-name(I)>)) a1)
By
Latex:
(Assert \mkleeneopen{}a0(a1(a)) = (a0(a) (sigma)(a;0) a1)\mkleeneclose{}\mcdot{} THENM Eq)
Home
Index