The category of types satisfies Grothendieck's AB5 axiom

This is of course just the well-known fact that filtered colimits commute with finite limits in the category of types.

instance CategoryTheory.Limits.instAB5Type : AB5 (Type v)