---

Step * 1 of Lemma composition-type-lemma4


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. rho : Gamma(I)
10. (u)<(s(f(rho));<new-name(J)>)> o iota
= ((u)<(s(rho);<new-name(I)>)> o iota)subset-trans(I+new-name(I);J+new-name(J);f,new-name(I)=new-name(J);s(phi(rho)))
∈ {J+new-name(J),s(phi(f(rho))) ⊢ _:(A)<(s(f(rho));<new-name(J)>)> o iota}
11. K : fset(ℕ)
12. g : J,phi(f(rho))(K)
13. Z : {J+new-name(J),s(phi(f(rho))) ⊢ _:(A)<(s(f(rho));<new-name(J)>)> o iota}
⊢ Z((new-name(J)0) ⋅ g) ∈ A(g((new-name(J)0)((s(f(rho));<new-name(J)>))))
BY
{ InferEqualType }

1
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. rho : Gamma(I)
10. (u)<(s(f(rho));<new-name(J)>)> o iota
= ((u)<(s(rho);<new-name(I)>)> o iota)subset-trans(I+new-name(I);J+new-name(J);f,new-name(I)=new-name(J);s(phi(rho)))
∈ {J+new-name(J),s(phi(f(rho))) ⊢ _:(A)<(s(f(rho));<new-name(J)>)> o iota}
11. K : fset(ℕ)
12. g : J,phi(f(rho))(K)
13. Z : {J+new-name(J),s(phi(f(rho))) ⊢ _:(A)<(s(f(rho));<new-name(J)>)> o iota}
⊢ (A)<(s(f(rho));<new-name(J)>)> o iota((new-name(J)0) ⋅ g) = A(g((new-name(J)0)((s(f(rho));<new-name(J)>)))) ∈ Type

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. rho : Gamma(I)
10. (u)<(s(f(rho));<new-name(J)>)> o iota
= ((u)<(s(rho);<new-name(I)>)> o iota)subset-trans(I+new-name(I);J+new-name(J);f,new-name(I)=new-name(J);s(phi(rho)))
∈ {J+new-name(J),s(phi(f(rho))) ⊢ _:(A)<(s(f(rho));<new-name(J)>)> o iota}
11. K : fset(ℕ)
12. g : J,phi(f(rho))(K)
13. Z : {J+new-name(J),s(phi(f(rho))) ⊢ _:(A)<(s(f(rho));<new-name(J)>)> o iota}
14. (A)<(s(f(rho));<new-name(J)>)> o iota((new-name(J)0) ⋅ g) = A(g((new-name(J)0)((s(f(rho));<new-name(J)>)))) ∈ Type
⊢ Z((new-name(J)0) ⋅ g) ∈ (A)<(s(f(rho));<new-name(J)>)> o iota((new-name(J)0) ⋅ g)

---

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.  rho  :  Gamma(I)
10.  (u)<(s(f(rho));<new-name(J)>)>  o  iota
=  ((u)<(s(rho);<new-name(I)>)>  o  iota)subset-trans(I+new-name(I);J+new-name(J);
                                                                                                      f,new-name(I)=new-name(J);s(phi(rho)))
11.  K  :  fset(\mBbbN{})
12.  g  :  J,phi(f(rho))(K)
13.  Z  :  \{J+new-name(J),s(phi(f(rho)))  \mvdash{}  \_:(A)<(s(f(rho));<new-name(J)>)>  o  iota\}
\mvdash{}  Z((new-name(J)0)  \mcdot{}  g)  \mmember{}  A(g((new-name(J)0)((s(f(rho));<new-name(J)>))))


By

---

Latex:
InferEqualType

---

Home Index