Documentation

Mathlib.CategoryTheory.Limits.Set

The functor from Set X to types preserves filtered colimits #

Given X : Type u, the functor Set.functorToTypes : Set X тед Type u which sends A : Set X to its underlying type preserves filtered colimits.