Гомоморфный образ группы
До победы коммунизма
Изоморфен факторгруппе
По ядру гомоморфизма
(с) творчество приматов (прикладная математика) из 80-х

Это базовая теорема о гомоморфизмах групп из абстрактной алгебры.
Если у нас есть отображение между двумя группами (гомоморфизм), то образ этого отображения изоморфен (по сути одинаков) факторгруппе (группе классов эквивалентности исходной группы по нормальной подгруппе) по ядру (множеству элементов, отображающихся в единицу группы) гомоморфизма (отображение между группами, сохраняющее операцию). Факторгруппа строится из элементов исходной группы, разбитых на классы эквивалентности по отношению принадлежности к одному смежному классу относительно ядра.

Так, думаю, понятнее 😁

Смотрите, как я первым в мире даю эту легендарную теорему в терминах HoTT =>

Эквивалентность двух типов/способов описания одного и того же математического объекта конструируется через взаимно обратные функции с путями, доказывающими, что их композиции гомотопны тождественным функциям.

Сигма-тип результата функции
До прихода унивалентности
Эквивалентен quotient type-у
По fiber-ам эквивалентности 🤓

p.s. Как пройдёте мой трек по гомотопической теории, так сразу это станет понятным, и даже код на питончике сможете такой писать.