Признаки и типы являются двумя возможными способами классификации явлений, относящихся к формализации грамматики и семантики естественного языка. Признаки часто используются в лингвистически ориентированных теориях. Однако они плохо согласуются с теоретико-типовой семантикой из-за понятия подтипа, к которому они приводят. В статье предлагается способ согласования этих двух подходов путем определения типов, основанных на классификации по признакам. Способ демонстрируется на примере формализации небольшого фрагмента английского языка. Построена общая формальная теория синтаксиса и семантики такого фрагмента, которая также имеет самостоятельное значение. Формализация проводится в языке Агда (Agda). Агда служит одновременно как: (1) метаязык, на котором формализуется синтаксис естественного языка, и (2) семантический/онтологический язык, на котором интерпретируется естественный язык. Это позволяет формализовать интерпретацию как функцию, переводящую выражения Агды, представляющие синтаксис, в формулы Агды, образующие семантику. Понятие подтипа опирается на понятие коэрсии или приведения типов, причем определение типов на основе признаков позволяет определить коэрсию автоматически. Механизм аргументов экземпляров (instance arguments) Агды позволяет во многих случаях проводить коэрсию автоматически. В конце статьи приведены примеры формализации языковых выражений, демонстрирующие работу построенной теории. Несмотря на то, что Агда как язык ориентирована прежде всего на математику, она содержит средства, позволяющие эффективно использовать ее в исследованиях естественного языка в рамках теоретико-типовой семантики.