Мне кажется все что угодно является объектом в какой нибудь категории

Что значит свободный объект?

Начальный?

Кончный?

ну в википедии на универсальном морфизме\сопряжении определеяют https://en.wikipedia.org/wiki/Free_object

В смысле определения выше, которое на википедии

Просто определения очень похожи, но так как я не очень хорошо знаком с большим кол-вом понятий, то может быть не нахожу очевидной связи, поэтому и вопрос

Но замечание остаётся верным, алгебра может быть тривиальной( описываемая константным эндофунктором), тогда любой объект становится свободным для неё

Совсем плохо понимаю, пойду дальше читать, спасибо за ответ.

Есть стандартный шаблон построения алгебраических структур, кратко называющийся "алгебры для монады".
Более развёрнуто, это идея о том, что какая-то алгебраическая структура, это совсем привычное свободное построение (прям аж синтаксическое дерево можно записать), и затем, факторизация.
Факторизацию часто удобно представлять в виде "правил установки равенства". Часто, несложно под это и индуктивно-зависимый тип написать.
Разговор тут, видимо, о том, как бы предствить всю структуру с равенством в виде чего-то "синтаксического".
Индуктивно-зависимый тип как-то почти оно и есть.
Я понял так.

Наверное, очень частый вопрос где почитать подробней? Просто читаю ncatlab плюс разные учебники, но это слишком разрозненно

Нуу, про алгебру, понятное дело, надо читать про фактор-структуры. Может быть, про фактор-алгебры в смысле универсальных алгебр.
Но у нас тут всё за теорию категорий, такштаа — любые материалы про алгебры для монады.
И пробовать примеры. Например, можно начать с построения алгебр для List-монады. Пример простой и имхо поучительный ;-)
Можно потом построить монаду свободной абелевой группы (в хаскеле, достаточно равенства на элементах, т.е., instance Eq, хоть и алгоритмически неэффективно). И посмотреть, что будет алгебрами для этой монады.

Если "про равенства", то берёшь любой язык с зависимыми типами и пробуешь делать тип равенства на элементах.
Idris, Agda, CoQ, Lean — всё это сгодится, ну и многое другое тоже.
Правда, я не вполне уверен, в эту ли сторону был вопрос.
Ну, я ответил, как понял...

А можно как-то на чьих-то ловких гомотопических пальцах объяснить различие между прекатегорией и категорией в HoTT и связи этих понятий с классическим теоркатом?
рандомный саммон

Valery @Comonoid @clayrat

продолжу саммоны
@Elijah_Vlasov @elemir90

Категория это как бы унивалентная прекатегория

С обычной теорией 1-категорий, думаю, нет смысла искать связи

Наверное, есть смысл покопать в сторону Segal spaces, но я не компетентен

category на кубике
https://github.com/groupoid/cubical/blob/master/src/category.ctt

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