---

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


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(𝕀)]]}
BY
{ (RepUR ``csm-comp-structure`` 0 THEN RepeatFor 4 (EqCDA) THEN Auto) }

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  cA  :  H:CubicalSet\{j\}
{}\mrightarrow{}  sigma:H.\mBbbI{}  j{}\mrightarrow{}  Gamma
{}\mrightarrow{}  phi:\{H  \mvdash{}  \_:\mBbbF{}\}
{}\mrightarrow{}  u:\{H,  phi.\mBbbI{}  \mvdash{}  \_:(A)sigma\}
{}\mrightarrow{}  a0:\{H  \mvdash{}  \_:((A)sigma)[0(\mBbbI{})][phi  |{}\mrightarrow{}  (u)[0(\mBbbI{})]]\}
{}\mrightarrow{}  \{H  \mvdash{}  \_:((A)sigma)[1(\mBbbI{})][phi  |{}\mrightarrow{}  (u)[1(\mBbbI{})]]\}
4.  uniform-comp-function\{j:l,  i:l\}(Gamma;  A;  cA)
5.  H  :  CubicalSet\{j\}
6.  sigma  :  H.\mBbbI{}  j{}\mrightarrow{}  Gamma
7.  phi  :  \{H  \mvdash{}  \_:\mBbbF{}\}
8.  u  :  \{H,  phi.\mBbbI{}  \mvdash{}  \_:(A)sigma\}
9.  a0  :  \{H  \mvdash{}  \_:((A)sigma)[0(\mBbbI{})][phi  |{}\mrightarrow{}  (u)[0(\mBbbI{})]]\}
\mvdash{}  (cA  H  sigma  phi  u  a0)  =  ((cA)1(Gamma)  H  sigma  phi  u  a0)


By

---

Latex:
(RepUR  ``csm-comp-structure``  0  THEN  RepeatFor  4  (EqCDA)  THEN  Auto)

---

Home Index