mathlib documentation

category_theory.limits.concrete_category

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

An auxiliary equivalence to be used in multiequalizer_equiv below.

Equations