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 → C and B → 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.