Dear all, Let C be an omega-category (strict, globular). Let U be the forgetful functor from strict globular omega-categories to globular sets. And let F be its left adjoint. Let us suppose that we are considering an equivalence relation R on UC (the underlying globular set of C) such that the source and target maps pass to the quotient : i.e. one can deal with the quotient globular set UC/R. The canonical morphism of globular sets UC --> UC/R induces a morphism of omega-categories F(UC) --> F(UC/R) by functoriality of F. Consider the following push-out in the category of omega-categories : F(UC) -----> F(UC/R) | | | | | | v v C ---------> D The morphism F(UC)-->C (the counit of the adjonction) is surjective on the underlying sets. The morphism F(UC)-->F(UC/R) is generally not surjective on the underlying sets : because by taking the quotient by R, one may add composites in F(UC/R) which do not exist in F(UC). However the intuition tells (me) that the morphism F(UC/R)-->D is surjective on the underlying sets : this morphism only adds in F(UC/R) the calculation rules of C : this is precisely what I want by introducing D. But I cannot see why with a rigorous mathematical argument. Thanks in advance. pg.