---

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

No Annotations
∀Gamma:j⊢. ∀A:{Gamma ⊢ _}.
  ∀[comp:composition-function{j:l,i:l}(Gamma;A)]
    (cfun-to-cop(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)
     ⟶ cubical-path-1(Gamma;A;I;i;rho;phi;u))
BY
{ (Intros
   THEN Unfold `comp-fun-to-comp-op` 0
   THEN RepeatFor 6 ((MemCD THENA Auto))
   THEN BLemma_o (ioid Obid: constrained-cubical-term-to-cubical-path-1)⋅
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}Gamma:j\mvdash{}.  \mforall{}A:\{Gamma  \mvdash{}  \_\}.
    \mforall{}[comp:composition-function\{j:l,i:l\}(Gamma;A)]
        (cfun-to-cop(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{}  cubical-path-1(Gamma;A;I;i;rho;phi;u))


By

---

Latex:
(Intros
  THEN  Unfold  `comp-fun-to-comp-op`  0
  THEN  RepeatFor  6  ((MemCD  THENA  Auto))
  THEN  BLemma\_o  (ioid  Obid:  constrained-cubical-term-to-cubical-path-1)\mcdot{}
  THEN  Auto)

---

Home Index