---

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

No Annotations
∀Gamma:j⊢. ∀A:{Gamma ⊢ _}.
  ∀[comp:composition-function{j:l,i:l}(Gamma;A)]
    (comp-fun-to-comp-op1(Gamma;A;comp) ∈ I:fset(ℕ)
     ⟶ i:{i:ℕ| ¬i ∈ I} 
     ⟶ rho:Gamma(I+i)
     ⟶ phi:𝔽(I)
     ⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
     ⟶ cubical-path-0(Gamma;A;I;i;rho;phi;u)
     ⟶ {formal-cube(I) ⊢ _:((A)<rho> o cube+(I;i))[1(𝕀)][canonical-section(();𝔽;I;⋅;phi) |⟶ ((u)cube+(I;i))[1(𝕀)]]})
BY
{ (Intros THEN Unfold `comp-fun-to-comp-op1` 0 THEN RepeatFor 6 ((MemCD THENA Auto))) }

1
.....subterm..... T:t
1:n
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. comp : composition-function{j:l,i:l}(Gamma;A)
4. I : fset(ℕ)
5. i : {i:ℕ| ¬i ∈ I} 
6. rho : Gamma(I+i)
7. phi : 𝔽(I)
8. u : {I+i,s(phi) ⊢ _:(A)<rho> o iota}
9. a0 : cubical-path-0(Gamma;A;I;i;rho;phi;u)
⊢ 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)
  ∈ {formal-cube(I) ⊢ _:((A)<rho> o cube+(I;i))[1(𝕀)][canonical-section(();𝔽;I;⋅;phi) |⟶ ((u)cube+(I;i))[1(𝕀)]]}

---

Latex:

---

Latex:
No  Annotations
\mforall{}Gamma:j\mvdash{}.  \mforall{}A:\{Gamma  \mvdash{}  \_\}.
    \mforall{}[comp:composition-function\{j:l,i:l\}(Gamma;A)]
        (comp-fun-to-comp-op1(Gamma;A;comp)  \mmember{}  I:fset(\mBbbN{})
          {}\mrightarrow{}  i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
          {}\mrightarrow{}  rho:Gamma(I+i)
          {}\mrightarrow{}  phi:\mBbbF{}(I)
          {}\mrightarrow{}  u:\{I+i,s(phi)  \mvdash{}  \_:(A)<rho>  o  iota\}
          {}\mrightarrow{}  cubical-path-0(Gamma;A;I;i;rho;phi;u)
          {}\mrightarrow{}  \{formal-cube(I)  \mvdash{}  \_:((A)<rho>  o  cube+(I;i))[1(\mBbbI{})][canonical-section(();\mBbbF{};I;\mcdot{};phi) 
                                                        |{}\mrightarrow{}  ((u)cube+(I;i))[1(\mBbbI{})]]\})


By

---

Latex:
(Intros  THEN  Unfold  `comp-fun-to-comp-op1`  0  THEN  RepeatFor  6  ((MemCD  THENA  Auto)))

---

Home Index