1  λ(a : Type) → { unit = [] : List a } ∧ ./semigroup a : ./../Monoid/Type (List a)