mathlib3 documentation

category_theory.limits.concrete_category

Facts about (co)limits of functors into concrete categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

An auxiliary equivalence to be used in multiequalizer_equiv below.

Equations