The interval homotopy operator is coordinate independent

Given: A smooth form $\omega$ up to the endpoints of $M\times [0,1]$.

Integration along the unit interval for a differential form: Let $\omega \in {\mathrm{\Omega }}^k(M\times [0,1])$ be smooth up to the endpoints. For $k\ge 1$, its interval integral is the $(k-1)$-form $K\omega ={\int }_0^1{\beta }_{t}dt$, where $\omega ={\alpha }_t+dt\wedge {\beta }_t$ and both families are tangential to $M$. Set $K=0$ on degree zero and on zero terms. Use the product structure of prop-products-of-smooth-manifolds-have-a-canonical-product-smooth-structure, restricted from $M\times \mathbb{R}$. The families are intrinsically ${\alpha }_t=i_t^{\ast }\omega$ and ${\beta }_t=i_t^{\ast }({\iota }_{{\mathrm{\partial }}_t}\omega )$, using def-interior-product-of-a-form-by-a-vector-field; evaluation on tangential tuples and on $({\mathrm{\partial }}_t,v_1,\dots ,v_{k-1})$ proves existence and uniqueness of the decomposition. The integral is in the fixed finite-dimensional fibre ${\bigwedge }^{k-1}{T}_x^{\ast }M$. Coefficients have smooth local extensions across endpoints. thm-differentiation-under-the-integral-sign-on-a-compact-rectangle supplies parameter differentiation; coordinate independence and full smoothness are proved in lem-the-interval-homotopy-operator-is-coordinate-independent.

Leibniz's rule on a compact rectangle: an interior parameter derivative with a continuous extension may be passed through a Riemann integral: Let $a<b$ and $c<d$. Suppose $g,h:[a,b]\times [c,d]\to \mathbb{R}$ are continuous and, for every fixed $t\in [c,d]$, the function $x\mapsto g(x,t)$ is differentiable on $(a,b)$ with derivative $h(x,t)$. Define $G(x):={\int }_c^{d}g(x,t)dt\mathrm{.}$ Then $G$ is differentiable on $[a,b]$ as a function on that interval and $G^{\mathrm{\prime }}(x)={\int }_c^{d}h(x,t)dt(x\in [a,b])\mathrm{.}$ At $a$ and $b$ the derivative is relative and one-sided. The derivative hypothesis is imposed only for interior parameter values; continuity of $h$ supplies its endpoint values.