Theory CZH_ECAT_Introduction

(* Copyright 2021 (C) Mihails Milehins *)

section‹Introduction›
theory CZH_ECAT_Introduction
  imports CZH_Foundations.CZH_DG_Introduction
begin



subsection‹Background›


text‹
This article provides a 
formalization of the elementary theory of 1-categories without
an additional structure. For further information see 
chapter Introduction in \<^cite>‹"milehins_category_2021"›.
›



subsection‹Preliminaries›

named_theorems cat_op_simps
named_theorems cat_op_intros

named_theorems cat_cs_simps
named_theorems cat_cs_intros

named_theorems cat_arrow_cs_intros



subsection‹CS setup for foundations›

lemmas (in 𝒵) [cat_cs_intros] = 𝒵_β
  
text‹\newpage›

end