mathlib3

eeb29569 - feat(topology/algebra): relax some `Type*` assumptions to `Sort*` (#12058)

feat(topology/algebra): relax some `Type*` assumptions to `Sort*` (#12058) When working on #11720 I forgot that we have to deal with Prop-indexed infimums quite often, so this PR fixes that.