Step
*
1
of Lemma
composition-type-lemma3
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma.𝕀 ⊢ _}
4. {Gamma.𝕀 ⊢ _} ⊆r {Gamma, phi.𝕀 ⊢ _}
5. u : {Gamma, phi.𝕀 ⊢ _:A}
6. I : fset(ℕ)
7. J : fset(ℕ)
8. f : J ⟶ I
9. a : Gamma(I)
10. ∀I:fset(ℕ). ∀[rho:Gamma(I)]. ((s(rho);<new-name(I)>) ∈ Gamma.𝕀(I+new-name(I)))
11. (s(phi(a)))<f,new-name(I)=new-name(J)> = s(phi(f(a))) ∈ 𝔽(J+new-name(J))
12. J+new-name(J),(s(phi(a)))<f,new-name(I)=new-name(J)> = J+new-name(J),s(phi(f(a))) ∈ CubicalSet{j}
13. <(s(f(a));<new-name(J)>)> ∈ J+new-name(J),s(phi(f(a))) j⟶ Gamma, phi.𝕀
14. <(s(f(a));<new-name(J)>)> o iota ∈ J+new-name(J),s(phi(f(a))) j⟶ Gamma, phi.𝕀
15. <(s(a);<new-name(I)>)> o iota ∈ I+new-name(I),s(phi(a)) j⟶ Gamma, phi.𝕀
⊢ (u)<(s(f(a));<new-name(J)>)>
= ((u)<(s(a);<new-name(I)>)> o iota)subset-trans(I+new-name(I);J+new-name(J);f,new-name(I)=new-name(J);s(phi(a)))
∈ {J+new-name(J),s(phi(f(a))) ⊢ _:(A)<(s(f(a));<new-name(J)>)>}
BY
{ Assert ⌜<(s(f(a));<new-name(J)>)> o iota
= <(s(a);<new-name(I)>)> o iota o subset-trans(I+new-name(I);J+new-name(J);f,new-name(I)=new-name(J);
s(phi(a)))
∈ J+new-name(J),s(phi(f(a))) j⟶ Gamma, phi.𝕀⌝⋅ }
1
.....assertion.....
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma.𝕀 ⊢ _}
4. {Gamma.𝕀 ⊢ _} ⊆r {Gamma, phi.𝕀 ⊢ _}
5. u : {Gamma, phi.𝕀 ⊢ _:A}
6. I : fset(ℕ)
7. J : fset(ℕ)
8. f : J ⟶ I
9. a : Gamma(I)
10. ∀I:fset(ℕ). ∀[rho:Gamma(I)]. ((s(rho);<new-name(I)>) ∈ Gamma.𝕀(I+new-name(I)))
11. (s(phi(a)))<f,new-name(I)=new-name(J)> = s(phi(f(a))) ∈ 𝔽(J+new-name(J))
12. J+new-name(J),(s(phi(a)))<f,new-name(I)=new-name(J)> = J+new-name(J),s(phi(f(a))) ∈ CubicalSet{j}
13. <(s(f(a));<new-name(J)>)> ∈ J+new-name(J),s(phi(f(a))) j⟶ Gamma, phi.𝕀
14. <(s(f(a));<new-name(J)>)> o iota ∈ J+new-name(J),s(phi(f(a))) j⟶ Gamma, phi.𝕀
15. <(s(a);<new-name(I)>)> o iota ∈ I+new-name(I),s(phi(a)) j⟶ Gamma, phi.𝕀
⊢ <(s(f(a));<new-name(J)>)> o iota
= <(s(a);<new-name(I)>)> o iota o subset-trans(I+new-name(I);J+new-name(J);f,new-name(I)=new-name(J);s(phi(a)))
∈ J+new-name(J),s(phi(f(a))) j⟶ Gamma, phi.𝕀
2
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma.𝕀 ⊢ _}
4. {Gamma.𝕀 ⊢ _} ⊆r {Gamma, phi.𝕀 ⊢ _}
5. u : {Gamma, phi.𝕀 ⊢ _:A}
6. I : fset(ℕ)
7. J : fset(ℕ)
8. f : J ⟶ I
9. a : Gamma(I)
10. ∀I:fset(ℕ). ∀[rho:Gamma(I)]. ((s(rho);<new-name(I)>) ∈ Gamma.𝕀(I+new-name(I)))
11. (s(phi(a)))<f,new-name(I)=new-name(J)> = s(phi(f(a))) ∈ 𝔽(J+new-name(J))
12. J+new-name(J),(s(phi(a)))<f,new-name(I)=new-name(J)> = J+new-name(J),s(phi(f(a))) ∈ CubicalSet{j}
13. <(s(f(a));<new-name(J)>)> ∈ J+new-name(J),s(phi(f(a))) j⟶ Gamma, phi.𝕀
14. <(s(f(a));<new-name(J)>)> o iota ∈ J+new-name(J),s(phi(f(a))) j⟶ Gamma, phi.𝕀
15. <(s(a);<new-name(I)>)> o iota ∈ I+new-name(I),s(phi(a)) j⟶ Gamma, phi.𝕀
16. <(s(f(a));<new-name(J)>)> o iota
= <(s(a);<new-name(I)>)> o iota o subset-trans(I+new-name(I);J+new-name(J);f,new-name(I)=new-name(J);s(phi(a)))
∈ J+new-name(J),s(phi(f(a))) j⟶ Gamma, phi.𝕀
⊢ (u)<(s(f(a));<new-name(J)>)>
= ((u)<(s(a);<new-name(I)>)> o iota)subset-trans(I+new-name(I);J+new-name(J);f,new-name(I)=new-name(J);s(phi(a)))
∈ {J+new-name(J),s(phi(f(a))) ⊢ _:(A)<(s(f(a));<new-name(J)>)>}
Latex:
Latex:
1. Gamma : CubicalSet\{j\}
2. phi : \{Gamma \mvdash{} \_:\mBbbF{}\}
3. A : \{Gamma.\mBbbI{} \mvdash{} \_\}
4. \{Gamma.\mBbbI{} \mvdash{} \_\} \msubseteq{}r \{Gamma, phi.\mBbbI{} \mvdash{} \_\}
5. u : \{Gamma, phi.\mBbbI{} \mvdash{} \_:A\}
6. I : fset(\mBbbN{})
7. J : fset(\mBbbN{})
8. f : J {}\mrightarrow{} I
9. a : Gamma(I)
10. \mforall{}I:fset(\mBbbN{}). \mforall{}[rho:Gamma(I)]. ((s(rho);<new-name(I)>) \mmember{} Gamma.\mBbbI{}(I+new-name(I)))
11. (s(phi(a)))<f,new-name(I)=new-name(J)> = s(phi(f(a)))
12. J+new-name(J),(s(phi(a)))<f,new-name(I)=new-name(J)> = J+new-name(J),s(phi(f(a)))
13. <(s(f(a));<new-name(J)>)> \mmember{} J+new-name(J),s(phi(f(a))) j{}\mrightarrow{} Gamma, phi.\mBbbI{}
14. <(s(f(a));<new-name(J)>)> o iota \mmember{} J+new-name(J),s(phi(f(a))) j{}\mrightarrow{} Gamma, phi.\mBbbI{}
15. <(s(a);<new-name(I)>)> o iota \mmember{} I+new-name(I),s(phi(a)) j{}\mrightarrow{} Gamma, phi.\mBbbI{}
\mvdash{} (u)<(s(f(a));<new-name(J)>)>
= ((u)<(s(a);<new-name(I)>)> o iota)subset-trans(I+new-name(I);J+new-name(J);
f,new-name(I)=new-name(J);s(phi(a)))
By
Latex:
Assert \mkleeneopen{}<(s(f(a));<new-name(J)>)> o iota
= <(s(a);<new-name(I)>)> o iota o subset-trans(I+new-name(I);J+new-name(J);
f,new-name(I)=new-name(J);s(phi(a)))\mkleeneclose{}\mcdot{}
Home
Index