Differential forms

so basically, treat dx, dy as formal symbols? you can multiply them by scalar, add them up
NOTE in agda it would be just n-form with ordered requirement? or just a subset?

f(x, y, z) dx ^ dy ^ dx – integrated over volume, gives volume
d operation – exterior derivative, results in k+1 form

ok so treat dx, dy, dz formally in form expression

https://en.wikipedia.org/wiki/Antisymmetric_tensor
a completely antisymmetric covariant tensor – p-form; contravarian – p-vector
https://en.wikipedia.org/wiki/Volume_form#Riemannian_volume_form

https://math.stackexchange.com/questions/664648/what-does-dx-mean-in-differential-form/664674#664674
dx₁ is a differential 1-form, linear map acting on tangent space. Action is: (1, 0, …. 0)

dx_i is a covector field. {dx_i}_i span all covector fields. For f ∈ Rⁿ -> R, you can write df = [f₁(x) f₂(x) .. f_n(x)] as f₁(x) dx₁ + … + f_n(x) dx_n
in that sense, dx₁ is the derivative of coordinate function f(x_1…xn) = x₁

Examples of how you can picture contravariant and covariant vectors. A contravari-ant vector is a “stick” with a direction to it.  Its “worth” (or “magnitude”) is proportional tothe length of the stick.  A covariant vector is like “lasagna.”  Its worth is proportional to thedensity of noodles; that is, the closer together are the sheets, the larger is the magnitude ofthe covector.  These and other pictorial examples of visualizing contravariant and covariantvectors are discussed in Am.J.Phys.65(1997)1037.Figure  3:   Pictorial  representation  of  the  innerproduct between a contravariant vector and a co-variant  vector.   The  “stick”  is  imbedded  in  the“lasagna”  and  the  inner  product  is  equal  to  thenumber of noodles pierced by the stick.  The in-ner product shown has the value 5.

Пусть {\displaystyle M} M — гладкое многообразие и {\displaystyle f\colon M\to \mathbb {R} } {\displaystyle f\colon M\to \mathbb {R} } гладкая функция. Дифференциал {\displaystyle f} f представляет собой 1-форму на {\displaystyle M} M, обычно обозначается {\displaystyle df} df и определяется соотношением
{\displaystyle df(X)=d_{p}f(X)=Xf,} {\displaystyle df(X)=d_{p}f(X)=Xf,}
где {\displaystyle Xf} Xf обозначает производную {\displaystyle f} f по направлению касательного вектора {\displaystyle X} X в точке {\displaystyle p\in M} p\in M.

hmm, that actually makes sense too!

1. Idea
Differentiation is the process that assigns to a function f:X→Y f : X \to Y its derivative, sometimes denoted df d f. The derivative is a function that, roughly speaking, assigns to each point x∈X x \in X the linear transformation dfx d f_x that maps infinitesimal differences y−x y - x (for points y y infinitesimally close to x x) to infinitesimal differences f(y)−f(x) f(y) - f(x).

https://math.stackexchange.com/questions/240491/what-is-a-covector-and-what-is-it-used-for

https://en.wikipedia.org/wiki/Closed_and_exact_differential_forms

 In mathematics, especially vector calculus and differential topology, a closed form is a differential form α whose exterior derivative is zero (dα = 0), and an exact form is a differential form, α, that is the exterior derivative of another differential form β. Thus, an exact form is in the image of d, and a closed form is in the kernel of d.

For an exact form α, α = dβ for some differential form β of degree one less than that of α. The form β is called a "potential form" or "primitive" for α. Since the exterior derivative of a closed form is zero, β is not unique, but can be modified by the addition of any closed form of degree one less than that of α.

Because d2 = 0, any exact form is necessarily closed. The question of whether every closed form is exact depends on the topology of the domain of interest. On a contractible domain, every closed form is exact by the Poincaré lemma. More general questions of this kind on an arbitrary differentiable manifold are the subject of de Rham cohomology, which allows one to obtain purely topological information using differential methods.

https://www.springer.com/us/book/9783319969916