(* We require that the host language (but NOT the guest language) be pure, i.e. all morphisms central, to simplify
* things. If this doesn't suit you, just consider the "host language" here to be the pure sublanguage of the
* host language, and toss on the inclusion functor to the full language *)
(* We require that the host language (but NOT the guest language) be pure, i.e. all morphisms central, to simplify
* things. If this doesn't suit you, just consider the "host language" here to be the pure sublanguage of the
* host language, and toss on the inclusion functor to the full language *)