---

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

.....subterm..... T:t
2:n
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>]}
13. (cA H sigma phi u a0)<a>(1) = cA formal-cube(I) sigma o <a>+ (phi)<a> (u)<a>+ (a0)<a>(1) ∈ ((A)sigma)[1(𝕀)](a)
14. cA formal-cube(I) sigma o <a>+ (phi)<a> (u)<a>+ (a0)<a>(1)
= 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 o <a>+)[1(𝕀)](1)
⊢ <1(a), 1> = <a, 1> ∈ (H.𝕀 I)
BY
{ (RepUR ``cube-context-adjoin functor-ob`` 0 THEN EqCDA THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  cA  :  composition-function\{j:l,i:l\}(Gamma;A)
4.  \mforall{}H,K:j\mvdash{}.  \mforall{}tau:K  j{}\mrightarrow{}  H.  \mforall{}sigma:H.\mBbbI{}  j{}\mrightarrow{}  Gamma.  \mforall{}phi:\{H  \mvdash{}  \_:\mBbbF{}\}.  \mforall{}u:\{H,  phi.\mBbbI{}  \mvdash{}  \_:(A)sigma\}.
      \mforall{}a0:\{H  \mvdash{}  \_:((A)sigma)[0(\mBbbI{})][phi  |{}\mrightarrow{}  (u)[0(\mBbbI{})]]\}.
          ((cA  H  sigma  phi  u  a0)tau  =  (cA  K  sigma  o  tau+  (phi)tau  (u)tau+  (a0)tau))
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)
12.  (cA  H  sigma  phi  u  a0)<a>  =  (cA  formal-cube(I)  sigma  o  <a>+  (phi)<a>  (u)<a>+  (a0)<a>)
13.  (cA  H  sigma  phi  u  a0)<a>(1)  =  cA  formal-cube(I)  sigma  o  <a>+  (phi)<a>  (u)<a>+  (a0)<a>(1)
14.  cA  formal-cube(I)  sigma  o  <a>+  (phi)<a>  (u)<a>+  (a0)<a>(1)
=  cA  formal-cube(I)  <(sigma)(s(a);<new-name(I)>)>  o  cube+(I;new-name(I)) 
    canonical-section(();\mBbbF{};I;\mcdot{};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)
\mvdash{}  ə(a),  1>  =  <a,  1>


By

---

Latex:
(RepUR  ``cube-context-adjoin  functor-ob``  0  THEN  EqCDA  THEN  Auto)

---

Home Index