---

Step * 2 of Lemma csm-comp-structure_wf

.....set predicate..... 
1. Gamma : CubicalSet{j}
2. Delta : CubicalSet{j}
3. tau : Delta j⟶ Gamma
4. A : {Gamma ⊢ _}
5. cA : composition-function{j:l,i:l}(Gamma;A)
6. uniform-comp-function{j:l, i:l}(Gamma; A; cA)
⊢ uniform-comp-function{j:l, i:l}(Delta; (A)tau; (cA)tau)
BY
{ ((RepeatFor 4 (ParallelLast') THEN (Assert H.𝕀 j⊢ BY Auto))
   THEN RepUR ``csm-comp-structure`` 0
   THEN (D 0 THENA Auto)
   THEN (D -3 With ⌜tau o sigma⌝  THENA Auto)
   THEN (RWO  "csm-comp-type" (-1) THENA Auto)
   THEN ParallelLast
   THEN (Assert sigma ∈ cube_set_map{[j | i]:l}(H, phi.𝕀; Delta) BY
               (SubsumeC ⌜H, phi.𝕀 j⟶ Delta⌝⋅ THEN Auto))
   THEN ParallelOp -2
   THEN ParallelLast) }

1
1. Gamma : CubicalSet{j}
2. Delta : CubicalSet{j}
3. tau : Delta j⟶ Gamma
4. A : {Gamma ⊢ _}
5. cA : composition-function{j:l,i:l}(Gamma;A)
6. H : CubicalSet{j}
7. K : CubicalSet{j}
8. tau@0 : K j⟶ H
9. H.𝕀 j⊢
10. sigma : H.𝕀 j⟶ Delta
11. ∀phi:{H ⊢ _:𝔽}. ∀u:{H, phi.𝕀 ⊢ _:((A)tau)sigma}. ∀a0:{H ⊢ _:(((A)tau)sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}.
      ((cA H tau o sigma phi u a0)tau@0
      = (cA K tau o sigma o tau@0+ (phi)tau@0 (u)tau@0+ (a0)tau@0)
      ∈ {K ⊢ _:((((A)tau)sigma)[1(𝕀)])tau@0[(phi)tau@0 |⟶ ((u)[1(𝕀)])tau@0]})
12. phi : {H ⊢ _:𝔽}
13. ∀u:{H, phi.𝕀 ⊢ _:((A)tau)sigma}. ∀a0:{H ⊢ _:(((A)tau)sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}.
      ((cA H tau o sigma phi u a0)tau@0
      = (cA K tau o sigma o tau@0+ (phi)tau@0 (u)tau@0+ (a0)tau@0)
      ∈ {K ⊢ _:((((A)tau)sigma)[1(𝕀)])tau@0[(phi)tau@0 |⟶ ((u)[1(𝕀)])tau@0]})
14. sigma ∈ cube_set_map{[j | i]:l}(H, phi.𝕀; Delta)
15. u : {H, phi.𝕀 ⊢ _:((A)tau)sigma}
16. ∀a0:{H ⊢ _:(((A)tau)sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
      ((cA H tau o sigma phi u a0)tau@0
      = (cA K tau o sigma o tau@0+ (phi)tau@0 (u)tau@0+ (a0)tau@0)
      ∈ {K ⊢ _:((((A)tau)sigma)[1(𝕀)])tau@0[(phi)tau@0 |⟶ ((u)[1(𝕀)])tau@0]})
17. a0 : {H ⊢ _:(((A)tau)sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
18. (cA H tau o sigma phi u a0)tau@0
= (cA K tau o sigma o tau@0+ (phi)tau@0 (u)tau@0+ (a0)tau@0)
∈ {K ⊢ _:((((A)tau)sigma)[1(𝕀)])tau@0[(phi)tau@0 |⟶ ((u)[1(𝕀)])tau@0]}
⊢ (cA H tau o sigma phi u a0)tau@0
= (cA K tau o sigma o tau@0+ (phi)tau@0 (u)tau@0+ (a0)tau@0)
∈ {K ⊢ _:((((A)tau)sigma)[1(𝕀)])tau@0[(phi)tau@0 |⟶ ((u)[1(𝕀)])tau@0]}

---

Latex:

---

Latex:
.....set  predicate..... 
1.  Gamma  :  CubicalSet\{j\}
2.  Delta  :  CubicalSet\{j\}
3.  tau  :  Delta  j{}\mrightarrow{}  Gamma
4.  A  :  \{Gamma  \mvdash{}  \_\}
5.  cA  :  composition-function\{j:l,i:l\}(Gamma;A)
6.  uniform-comp-function\{j:l,  i:l\}(Gamma;  A;  cA)
\mvdash{}  uniform-comp-function\{j:l,  i:l\}(Delta;  (A)tau;  (cA)tau)


By

---

Latex:
((RepeatFor  4  (ParallelLast')  THEN  (Assert  H.\mBbbI{}  j\mvdash{}  BY  Auto))
  THEN  RepUR  ``csm-comp-structure``  0
  THEN  (D  0  THENA  Auto)
  THEN  (D  -3  With  \mkleeneopen{}tau  o  sigma\mkleeneclose{}    THENA  Auto)
  THEN  (RWO    "csm-comp-type"  (-1)  THENA  Auto)
  THEN  ParallelLast
  THEN  (Assert  sigma  \mmember{}  cube\_set\_map\{[j  |  i]:l\}(H,  phi.\mBbbI{};  Delta)  BY
                          (SubsumeC  \mkleeneopen{}H,  phi.\mBbbI{}  j{}\mrightarrow{}  Delta\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  ParallelOp  -2
  THEN  ParallelLast)

---

Home Index