Proposition 7.8. Assuming that:

Then Ceff=(Rel(C)[Eˇ])la is effective regular, and the embedding Rel(C)Rel(C)[Eˇ] restricts to a full and faithful regular functor CCeff which is universal among regular functors CD where D is effective regular.