Adhesive categories #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
Main definitions #
Main Results #
Show that the following are adhesive:
- functor categories into adhesive categories
- the categories of sheaves over a site
A convenience formulation for a pushout being a van Kampen colimit.
A category is adhesive if it has pushouts and pullbacks along monomorphisms,
and such pushouts are van Kampen.
Instances of this typeclass