Theory CZH_UCAT_Introduction

(* Copyright 2021 (C) Mihails Milehins *)

section‹Introduction›
theory CZH_UCAT_Introduction
  imports CZH_Elementary_Categories.CZH_ECAT_Introduction
begin

text‹
This article provides a formalization of further elements of the
theory of 1-categories without an additional structure.
More specifically, this article explores canonical universal
constructions \<^cite>‹"noauthor_nlab_nodate"›\footnote{
\url{https://ncatlab.org/nlab/show/universal+construction}
} and their properties, building upon the formalization
of the foundations of category theory in \<^cite>‹"milehins_category_2021"›.
›

text‹\newpage›

end