Adhesive structure on slice categories

The slice category Over B inherits the property of being adhesive from the base category, and dually so does the coslice category Under B.

instance CategoryTheory.adhesive_over {C : Type u_1} [Category.{v_1, u_1} C] [Adhesive C] [Limits.HasPullbacks C] [Limits.HasPushouts C] (B : C) : Adhesive (Over B)

Slices of adhesive categories are adhesive. See [LS04], Proposition 8 (ii).

instance CategoryTheory.adhesive_under {C : Type u_1} [Category.{v_1, u_1} C] [Adhesive C] [Limits.HasPullbacks C] [Limits.HasPushouts C] (B : C) : Adhesive (Under B)

Coslices of adhesive categories are adhesive. See [LS04], Proposition 8 (ii).