---

Step * 1 1 of Lemma comp-fun-to-comp-op-inverse


1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : composition-function{j:l,i:l}(Gamma;A)
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(𝕀)]]}
10. I : fset(ℕ)
11. a : H(I)
⊢ (cA H sigma phi u a0 I a) = (cop-to-cfun(cfun-to-cop(Gamma;A;cA)) H sigma phi u a0 I a) ∈ ((A)sigma)[1(𝕀)](a)
BY
{ (RepUR ``comp-fun-to-comp-op comp-op-to-comp-fun comp-fun-to-comp-op1`` 0
   THEN RepUR ``composition-term csm-composition`` 0
   THEN UnfoldTopAb 4
   THEN (InstHyp [⌜H⌝;⌜formal-cube(I)⌝;⌜<a>⌝;⌜sigma⌝;⌜phi⌝;⌜u⌝;⌜a0⌝] 4⋅ THENA Auto)) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : composition-function{j:l,i:l}(Gamma;A)
4. ∀H,K:j⊢. ∀tau:K j⟶ H. ∀sigma:H.𝕀 j⟶ Gamma. ∀phi:{H ⊢ _:𝔽}. ∀u:{H, phi.𝕀 ⊢ _:(A)sigma}.
   ∀a0:{H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}.
     ((cA H sigma phi u a0)tau
     = (cA K sigma o tau+ (phi)tau (u)tau+ (a0)tau)
     ∈ {K ⊢ _:(((A)sigma)[1(𝕀)])tau[(phi)tau |⟶ ((u)[1(𝕀)])tau]})
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(𝕀)]]}
10. I : fset(ℕ)
11. a : H(I)
12. (cA H sigma phi u a0)<a>
= (cA formal-cube(I) sigma o <a>+ (phi)<a> (u)<a>+ (a0)<a>)
∈ {formal-cube(I) ⊢ _:(((A)sigma)[1(𝕀)])<a>[(phi)<a> |⟶ ((u)[1(𝕀)])<a>]}
⊢ (cA H sigma phi u a0 I a)
= cA formal-cube(I) <(sigma)(s(a);<new-name(I)>)> o cube+(I;new-name(I)) canonical-section(();𝔽;I;⋅;phi(a)) 
  ((u)<(s(a);<new-name(I)>)> o iota)cube+(I;new-name(I)) 
  canonical-section(Gamma;A;I;(new-name(I)0)((sigma)(s(a);<new-name(I)>));a0(a))(1)
∈ ((A)sigma)[1(𝕀)](a)

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  cA  :  composition-function\{j:l,i:l\}(Gamma;A)
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{})]]\}
10.  I  :  fset(\mBbbN{})
11.  a  :  H(I)
\mvdash{}  (cA  H  sigma  phi  u  a0  I  a)  =  (cop-to-cfun(cfun-to-cop(Gamma;A;cA))  H  sigma  phi  u  a0  I  a)


By

---

Latex:
(RepUR  ``comp-fun-to-comp-op  comp-op-to-comp-fun  comp-fun-to-comp-op1``  0
  THEN  RepUR  ``composition-term  csm-composition``  0
  THEN  UnfoldTopAb  4
  THEN  (InstHyp  [\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}formal-cube(I)\mkleeneclose{};\mkleeneopen{}<a>\mkleeneclose{};\mkleeneopen{}sigma\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}a0\mkleeneclose{}]  4\mcdot{}  THENA  Auto))

---

Home Index