mathlib documentation

category_theory.limits.shapes.concrete_category

Facts about limits of functors into concrete categories #

This file doesn't yet attempt to be exhaustive; it just contains lemmas that are useful while comparing categorical limits with existing constructions in concrete categories.