The length of joins in Lambek calculus

In 1992, M. Pentus established a criterion for the existence of a type $C$ such that for given types $A$ and $B$ the sequents $A\to C$ and $B\to C$ are derivable in the Lambek calculus. In this paper we give an algorithm for construction of such a type $C$ (provided it exists) and prove a quadratic upper bound for its length.