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.