Documentation

Mathlib.CategoryTheory.Limits.Shapes.Countable

Countable limits and colimits #

A typeclass for categories with all countable (co)limits.

We also prove that all cofiltered limits over countable preorders are isomorphic to sequential limits, see sequentialFunctor_initial.

Projects #

A category has all countable limits if every functor J ⥤ C with a CountableCategory J instance and J : Type has a limit.

Instances

    A category has countable products if it has all products indexed by countable types.

    Instances

      A category has all countable colimits if every functor J ⥤ C with a CountableCategory J instance and J : Type has a colimit.

      Instances

        A category has countable coproducts if it has all coproducts indexed by countable types.

        Instances

          The initial functor ℕᵒᵖ ⥤ J, which allows us to turn cofiltered limits over countable preorders into sequential limits.

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

            The initial functor ℕᵒᵖ ⥤ J, which allows us to turn cofiltered limits over countable preorders into sequential limits.

            TODO: redefine this as (IsFiltered.sequentialFunctor Jᵒᵖ).leftOp. This would need API for initial/ final functors of the form leftOp/rightOp.

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