Basically it's a proof that some primitive has either a limit or colimit (special object, that's why it's called Basetype) in one of their descendant supertypes.