The curry-howard isomorphism is the idea that formal logics and programming languages (usually typed lambda calculi) are so related that they're almost the same thing. There's a more elaborate version that creates a three-way correspondence between formal logic, programming languages and categories. The most well known correspondence goes like Intuitionistic Logic <=> Simply Typed Lambda Calculus <=> Cartesian Closed Categories (cf. [0]). In particular, the types of the programming language are the objects, and terms in the language with a given context are morphisms in the category: in `t : A -> B`, A is the context and B is the type of the term t, i.e. t can contain free variables of A, with a minor note [1].
Now, the programming languages being examined here have more structure than that. They handle this by considering internal categories. Usually categories are defined with sets of objects and sets of morphisms. Internal categories are such that there is some fancier structure on both. In this case, there is a relation "X is more dynamic than Y", for both types and terms. The definition isn't too hard of a leap from plain categories: The term composition operation should respect the dynamism relation.
A functor is a map between categories: It sends objects (types) to objects and sends morphisms (terms) to morphisms while respecting the algebra of categories, which corresponds to being compatible with term substitution for programming languages. Translating via curry-howard, a functor is a parametric construction of some sort: you can carry it out without knowing anything about the particulars of the term you're translating. Generics are a form of parametric construction, for example. `map` in various languages internalizes the compatibility with the construction.
A profunctor is a bit gnarlier, but it bears a similar relation to functors as relations do to functions. The prototypical profunctor is Hom(-, --), which is defined such that Hom(A, B) is the set of morphisms between objects A and B. In good situations, the data of a profunctor is equivalent to the data of a functor, much the same way that functions and cofunctions are special kinds of relations [2]. This situation is called a representable profunctor.
In really good situations, a profunctor can have two non-equivalent descriptions as a functor. In such a case the functors are specially related: They are adjoint [3]. Adjoint functors are constructions that are dual to each other in a technical sense which makes them really useful to calculate with. The upshot is that the data of the profunctor boils down to two fundamental parametric operations which are dual to each other.
In this case, "dynamism" boils down to two canonical operations: upcasting and downcasting. That's really intuitive, and the usefulness here is that the category theory has essentially captured this intuition while also stating exactly how upcasting / downcasting interact with terms, this is the part about "proarrow equipments". Turning intuition into a precise, technical tool is the core strength of category theory.
The conclusion is an application: Using this machinery to construct abstract models of the semantics of such a lanugage. I haven't read the details, but the post describes two semantics where type errors are the same as a diverging program, and one where they are different. The latter is interesting because there you could conceivably extend the semantics further to model exception handling for type errors.
[0] https://existentialtype.wordpress.com/2011/03/27/the-holy-tr...
[1] What about multiple free variables in the term? The simplest way to handle contexts with multiple variables is to conflate them with contexts of a single cartesian product of values. In this construction, the authors are going all the way and fully distinguishing cartesian products inside the programming language from the idea of complex contexts, hence "virtual cartesian preorder categories".
[2] By cofunction I mean functions where the domain and the range have been swapped. Technically speaking, a profunctor can be represented either as Hom(f -, --) or Hom(-, f --) for a functor f.