---

Step * 2 of Lemma composition-structure-subset

.....set predicate..... 
1. Y : CubicalSet{j}
2. X : CubicalSet{j}
3. sub_cubical_set{j:l}(Y; X)
4. B : {X ⊢ _}
5. x : composition-function{j:l,i:l}(X;B)
6. uniform-comp-function{j:l, i:l}(X; B; x)
⊢ uniform-comp-function{j:l, i:l}(Y; B; x)
BY
{ RepeatFor 8 (ParallelLast') }

1
1. Y : CubicalSet{j}
2. X : CubicalSet{j}
3. sub_cubical_set{j:l}(Y; X)
4. B : {X ⊢ _}
5. x : composition-function{j:l,i:l}(X;B)
6. H : CubicalSet{j}
7. K : CubicalSet{j}
8. tau : K j⟶ H
9. sigma : H.𝕀 j⟶ Y
10. phi : {H ⊢ _:𝔽}
11. u : {H, phi.𝕀 ⊢ _:(B)sigma}
12. a0 : {H ⊢ _:((B)sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
13. (x H sigma phi u a0)tau
= (x K sigma o tau+ (phi)tau (u)tau+ (a0)tau)
∈ {K ⊢ _:(((B)sigma)[1(𝕀)])tau[(phi)tau |⟶ ((u)[1(𝕀)])tau]}
⊢ (x H sigma phi u a0)tau
= (x K sigma o tau+ (phi)tau (u)tau+ (a0)tau)
∈ {K ⊢ _:(((B)sigma)[1(𝕀)])tau[(phi)tau |⟶ ((u)[1(𝕀)])tau]}

---

Latex:

---

Latex:
.....set  predicate..... 
1.  Y  :  CubicalSet\{j\}
2.  X  :  CubicalSet\{j\}
3.  sub\_cubical\_set\{j:l\}(Y;  X)
4.  B  :  \{X  \mvdash{}  \_\}
5.  x  :  composition-function\{j:l,i:l\}(X;B)
6.  uniform-comp-function\{j:l,  i:l\}(X;  B;  x)
\mvdash{}  uniform-comp-function\{j:l,  i:l\}(Y;  B;  x)


By

---

Latex:
RepeatFor  8  (ParallelLast')

---

Home Index