Write an instance of `Homogenization` for hyperplanes

[ooovi]

probably looks something like

instance {weight : W →ₗ[R] R} (hw : weight ≠ 0) :
    letI : Nonempty (AffineSubspace.comap weight.toAffineMap (affineSpan R {(1 : R)})) := sorry
    Homogenization R (AffineSubspace.comap weight.toAffineMap (affineSpan R {(1 : R)})) W where

can probably never be inferred. so Homogenization should not be a class. right?

[martinwintermath]

At least this should not be an instance. But I tend to agree that we maybe dont need a class.