---

Step * 1 1 2 1 2 1 1 2 1 of Lemma comp_term-subset


1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 ⊢ Compositon(A)
4. psi : {Gamma ⊢ _:𝔽}
⊢ cA = (cA)1(Gamma, psi)+ ∈ composition-function{j:l,i:l}(Gamma, psi.𝕀;A)
BY
{ (DVar `cA' THEN All (Unfold `composition-function`)) }

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. psi : {Gamma ⊢ _:𝔽}
⊢ cA
= (cA)1(Gamma, psi)+
∈ (H:CubicalSet{j}
  ⟶ sigma:H.𝕀 j⟶ Gamma, psi.𝕀
  ⟶ phi:{H ⊢ _:𝔽}
  ⟶ u:{H, phi.𝕀 ⊢ _:(A)sigma}
  ⟶ a0:{H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
  ⟶ {H ⊢ _:((A)sigma)[1(𝕀)][phi |⟶ (u)[1(𝕀)]]})

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma.\mBbbI{}  \mvdash{}  \_\}
3.  cA  :  Gamma.\mBbbI{}  \mvdash{}  Compositon(A)
4.  psi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
\mvdash{}  cA  =  (cA)1(Gamma,  psi)+


By

---

Latex:
(DVar  `cA'  THEN  All  (Unfold  `composition-function`))

---

Home Index