---

Step * 1 of Lemma csm-comp-structure-id


1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : Gamma ⊢ Compositon(A)
⊢ (cA)1(Gamma) = cA ∈ Gamma ⊢ Compositon(A)
BY
{ (DVar `cA'
   THEN Symmetry
   THEN MemTypeCD
   THEN Auto
   THEN All (Unfold `composition-function`)
   THEN RepeatFor 5 ((FunExt THENA Auto))) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : H:CubicalSet{j}
⟶ sigma:H.𝕀 j⟶ Gamma
⟶ phi:{H ⊢ _:𝔽}
⟶ u:{H, phi.𝕀 ⊢ _:(A)sigma}
⟶ a0:{H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
⟶ {H ⊢ _:((A)sigma)[1(𝕀)][phi |⟶ (u)[1(𝕀)]]}
4. uniform-comp-function{j:l, i:l}(Gamma; A; cA)
5. H : CubicalSet{j}
6. sigma : H.𝕀 j⟶ Gamma
7. phi : {H ⊢ _:𝔽}
8. u : {H, phi.𝕀 ⊢ _:(A)sigma}
9. a0 : {H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
⊢ (cA H sigma phi u a0) = ((cA)1(Gamma) H sigma phi u a0) ∈ {H ⊢ _:((A)sigma)[1(𝕀)][phi |⟶ (u)[1(𝕀)]]}

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  cA  :  Gamma  \mvdash{}  Compositon(A)
\mvdash{}  (cA)1(Gamma)  =  cA


By

---

Latex:
(DVar  `cA'
  THEN  Symmetry
  THEN  MemTypeCD
  THEN  Auto
  THEN  All  (Unfold  `composition-function`)
  THEN  RepeatFor  5  ((FunExt  THENA  Auto)))

---

Home Index