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.