Documentation

Mathlib.CategoryTheory.Countable

Countable categories #

A category is countable in this sense if it has countably many objects and countably many morphisms.

A category with countably many objects and morphisms.

Instances
    @[reducible, inline]

    A countable category α is equivalent to a category with objects in Type.

    Equations

    The constructed category is indeed equivalent to α.

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

    The opposite of a countable category is countable.

    Applying ULift to morphisms and objects of a category preserves countability.