---

Step * of Lemma comp-fun-to-comp-op_wf

No Annotations
∀Gamma:j⊢. ∀A:{Gamma ⊢ _}.  ∀[comp:Gamma ⊢ Compositon(A)]. (cfun-to-cop(Gamma;A;comp) ∈ Gamma ⊢ CompOp(A))
BY
{ (Auto
   THEN D -1
   THEN MemTypeCD
   THEN Auto
   THEN D 0
   THEN Auto
   THEN RepUR ``comp-fun-to-comp-op comp-fun-to-comp-op1`` 0
   THEN (D 4 With ⌜formal-cube(I)⌝  THENA Auto)
   THEN (InstHyp [⌜formal-cube(J)⌝;⌜<g>⌝;⌜<rho> o cube+(I;i)⌝;⌜canonical-section(();𝔽;I;⋅;phi)⌝] (-1)⋅ THENA Auto)
   THEN Thin (-2)) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. comp : composition-function{j:l,i:l}(Gamma;A)
4. I : fset(ℕ)
5. J : fset(ℕ)
6. i : {i:ℕ| ¬i ∈ I} 
7. j : {j:ℕ| ¬j ∈ J} 
8. g : J ⟶ I
9. rho : Gamma(I+i)
10. phi : 𝔽(I)
11. u : {I+i,s(phi) ⊢ _:(A)<rho> o iota}
12. a0 : cubical-path-0(Gamma;A;I;i;rho;phi;u)
13. ∀u:{formal-cube(I), canonical-section(();𝔽;I;⋅;phi).𝕀 ⊢ _:(A)<rho> o cube+(I;i)}.
    ∀a0:{formal-cube(I) ⊢ _:((A)<rho> o cube+(I;i))[0(𝕀)][canonical-section(();𝔽;I;⋅;phi) |⟶ (u)[0(𝕀)]]}.
      ((comp formal-cube(I) <rho> o cube+(I;i) canonical-section(();𝔽;I;⋅;phi) u a0)<g>
      = (comp formal-cube(J) <rho> o cube+(I;i) o <g>+ (canonical-section(();𝔽;I;⋅;phi))<g> (u)<g>+ (a0)<g>)
      ∈ {formal-cube(J) ⊢ _:(((A)<rho> o cube+(I;i))[1(𝕀)])<g>[(canonical-section(();𝔽;I;⋅;phi))<g> 
                            |⟶ ((u)[1(𝕀)])<g>]})
⊢ (comp formal-cube(I) <rho> o cube+(I;i) canonical-section(();𝔽;I;⋅;phi) (u)cube+(I;i) 
   canonical-section(Gamma;A;I;(i0)(rho);a0)(1) (i1)(rho) g)
= comp formal-cube(J) <g,i=j(rho)> o cube+(J;j) canonical-section(();𝔽;J;⋅;g(phi)) 
  ((u)subset-trans(I+i;J+j;g,i=j;s(phi)))cube+(J;j) 
  canonical-section(Gamma;A;J;(j0)(g,i=j(rho));(a0 (i0)(rho) g))(1)
∈ A(g((i1)(rho)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}Gamma:j\mvdash{}.  \mforall{}A:\{Gamma  \mvdash{}  \_\}.
    \mforall{}[comp:Gamma  \mvdash{}  Compositon(A)].  (cfun-to-cop(Gamma;A;comp)  \mmember{}  Gamma  \mvdash{}  CompOp(A))


By

---

Latex:
(Auto
  THEN  D  -1
  THEN  MemTypeCD
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  RepUR  ``comp-fun-to-comp-op  comp-fun-to-comp-op1``  0
  THEN  (D  4  With  \mkleeneopen{}formal-cube(I)\mkleeneclose{}    THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}formal-cube(J)\mkleeneclose{};\mkleeneopen{}<g>\mkleeneclose{};\mkleeneopen{}<rho>  o  cube+(I;i)\mkleeneclose{};\mkleeneopen{}canonical-section(();\mBbbF{};I;\mcdot{};phi)\mkleeneclose{}]  (-1)\mcdot{}
              THENA  Auto
              )
  THEN  Thin  (-2))

---

Home Index