---

Step * 1 of Lemma csm-comp-structure_wf


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)
⊢ (cA)tau ∈ composition-function{j:l,i:l}(Delta;(A)tau)
BY
{ (RepUR ``csm-comp-structure composition-function`` 0
   THEN (FunExt THENA Auto)
   THEN Reduce 0
   THEN (Assert H.𝕀 j⊢ BY
               Auto)
   THEN RepeatFor 4 ((FunExt THENA (Auto THEN SubsumeC ⌜H, phi.𝕀 j⟶ Delta⌝⋅ THEN Auto)))
   THEN Reduce 0) }

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. uniform-comp-function{j:l, i:l}(Gamma; A; cA)
7. H : CubicalSet{j}
8. H.𝕀 j⊢
9. sigma : H.𝕀 j⟶ Delta
10. phi : {H ⊢ _:𝔽}
11. u : {H, phi.𝕀 ⊢ _:((A)tau)sigma}
12. a0 : {H ⊢ _:(((A)tau)sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
⊢ cA H tau o sigma phi u a0 ∈ {H ⊢ _:(((A)tau)sigma)[1(𝕀)][phi |⟶ (u)[1(𝕀)]]}

---

Latex:

---

Latex:

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{}  (cA)tau  \mmember{}  composition-function\{j:l,i:l\}(Delta;(A)tau)


By

---

Latex:
(RepUR  ``csm-comp-structure  composition-function``  0
  THEN  (FunExt  THENA  Auto)
  THEN  Reduce  0
  THEN  (Assert  H.\mBbbI{}  j\mvdash{}  BY
                          Auto)
  THEN  RepeatFor  4  ((FunExt  THENA  (Auto  THEN  SubsumeC  \mkleeneopen{}H,  phi.\mBbbI{}  j{}\mrightarrow{}  Delta\mkleeneclose{}\mcdot{}  THEN  Auto)))
  THEN  Reduce  0)

---

Home Index