Documentation

Mathlib.CategoryTheory.Extensive

Extensive categories #

Main definitions #

Main Results #

TODO #

Show that the following are finitary extensive:

References #

A category has pullback of inclusions if it has all pullbacks along coproduct injections.

Instances

    A functor preserves pullback of inclusions if it preserves all pullbacks along coproduct injections.

    Instances

      A category is (finitary) pre-extensive if it has finite coproducts, and binary coproducts are universal.

      Instances

        A category is (finitary) extensive if it has finite coproducts, and binary coproducts are van Kampen.

        Instances