---

Step * 2 1 of Lemma composition-structure-subset


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]}
BY
{ (NthHypSq (-1) THEN CsmUnfolding THEN Auto) }

---

Latex:

---

Latex:

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.  H  :  CubicalSet\{j\}
7.  K  :  CubicalSet\{j\}
8.  tau  :  K  j{}\mrightarrow{}  H
9.  sigma  :  H.\mBbbI{}  j{}\mrightarrow{}  Y
10.  phi  :  \{H  \mvdash{}  \_:\mBbbF{}\}
11.  u  :  \{H,  phi.\mBbbI{}  \mvdash{}  \_:(B)sigma\}
12.  a0  :  \{H  \mvdash{}  \_:((B)sigma)[0(\mBbbI{})][phi  |{}\mrightarrow{}  (u)[0(\mBbbI{})]]\}
13.  (x  H  sigma  phi  u  a0)tau  =  (x  K  sigma  o  tau+  (phi)tau  (u)tau+  (a0)tau)
\mvdash{}  (x  H  sigma  phi  u  a0)tau  =  (x  K  sigma  o  tau+  (phi)tau  (u)tau+  (a0)tau)


By

---

Latex:
(NthHypSq  (-1)  THEN  CsmUnfolding  THEN  Auto)

---

Home Index