Surely your monoid example should be a Sigma type (`exists`), not a Pi type (`forall`), since a monoid is a specification of data for a single type A, not for a

Surely your monoid example should be a Sigma type (`exists`), not a Pi type (`forall`), since a monoid is a specification of data for a single type A, not for all types A. Indeed, the empty type has no monoid structure, so the Pi type you wrote down is necessarily empty.