Documentation

Mathlib.CategoryTheory.ChosenFiniteProducts

Categories with chosen finite products #

We introduce a class, ChosenFiniteProducts, which bundles explicit choices for a terminal object and binary products in a category C. This is primarily useful for categories which have finite products with good definitional properties, such as the category of types.

Given a category with such an instance, we also provide the associated symmetric monoidal structure so that one can write X āŠ— Y for the explicit binary product and šŸ™_ C for the explicit terminal object.

Projects #

An instance of ChosenFiniteProducts C bundles an explicit choice of a binary product of two objects of C, and a terminal object in C.

Users should use the monoidal notation: X āŠ— Y for the product and šŸ™_ C for the terminal object.

Instances
    @[instance 100]
    Equations
    • One or more equations did not get rendered due to their size.
    @[instance 100]
    Equations
    • One or more equations did not get rendered due to their size.

    The unique map to the terminal object.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      This lemma follows from the preexisting Unique instance, but it is often convenient to use it directly as apply toUnit_unique forcing lean to do the necessary elaboration.

      Construct an instance of ChosenFiniteProducts C given an instance of HasFiniteProducts C.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For