---

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


1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : 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)
4. composition-uniformity(Gamma;A;cA)
5. I : fset(ℕ)
6. i : {i:ℕ| ¬i ∈ I} 
7. rho : Gamma(I+i)
8. phi : 𝔽(I)
9. u : {I+i,s(phi) ⊢ _:(A)<rho> o iota}
10. x : cubical-path-0(Gamma;A;I;i;rho;phi;u)
⊢ (cA I i rho phi u x) = (cfun-to-cop(Gamma;A;cop-to-cfun(cA)) I i rho phi u x) ∈ cubical-path-1(Gamma;A;I;i;rho;phi;u)
BY
{ (Assert <new-name(I)> ∈ 𝕀(s(1)) BY
         ((RWO  "interval-type-at" 0 THENA Auto) THEN RepUR ``interval-presheaf`` 0 THEN Auto)) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : 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)
4. composition-uniformity(Gamma;A;cA)
5. I : fset(ℕ)
6. i : {i:ℕ| ¬i ∈ I} 
7. rho : Gamma(I+i)
8. phi : 𝔽(I)
9. u : {I+i,s(phi) ⊢ _:(A)<rho> o iota}
10. x : cubical-path-0(Gamma;A;I;i;rho;phi;u)
11. <new-name(I)> ∈ 𝕀(s(1))
⊢ (cA I i rho phi u x) = (cfun-to-cop(Gamma;A;cop-to-cfun(cA)) I i rho phi u x) ∈ cubical-path-1(Gamma;A;I;i;rho;phi;u)

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  cA  :  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)
4.  composition-uniformity(Gamma;A;cA)
5.  I  :  fset(\mBbbN{})
6.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
7.  rho  :  Gamma(I+i)
8.  phi  :  \mBbbF{}(I)
9.  u  :  \{I+i,s(phi)  \mvdash{}  \_:(A)<rho>  o  iota\}
10.  x  :  cubical-path-0(Gamma;A;I;i;rho;phi;u)
\mvdash{}  (cA  I  i  rho  phi  u  x)  =  (cfun-to-cop(Gamma;A;cop-to-cfun(cA))  I  i  rho  phi  u  x)


By

---

Latex:
(Assert  <new-name(I)>  \mmember{}  \mBbbI{}(s(1))  BY
              ((RWO    "interval-type-at"  0  THENA  Auto)  THEN  RepUR  ``interval-presheaf``  0  THEN  Auto))

---

Home Index