The glueing construction, defined as a certain comma category, is an important tool for reasoning about type theories, logics, and programming languages . Here we extend the construction to accommodate ‘ 2-dimensional theories ’ of types, terms between types, and rewrites between terms . Taking bicategories as the semantic framework for such systems, we define the glueing bicategory and establish a bicategorical version of the well-known construction of cartesian closed structure on a glueing category . As an application, we show that free finite-product bicategories are fully complete relative to free cartesian closed bicategories, thereby establishing that the higher-order equational theory of rewriting in the simply-typed lambda calculus is a conservative extension of the algebraic equational theory of rewriting in the fragment with finite products only.