(* Copyright 2021 (C) Mihails Milehins *) theory CZH_UCAT_Conclusions imports CZH_UCAT_Universal CZH_UCAT_Limit CZH_UCAT_Limit_IT CZH_UCAT_Limit_Product CZH_UCAT_Limit_Pullback CZH_UCAT_Limit_Equalizer CZH_UCAT_Pointed CZH_UCAT_Representable CZH_UCAT_Complete CZH_UCAT_Comma CZH_UCAT_Set CZH_UCAT_Adjoints CZH_UCAT_Kan CZH_UCAT_PWKan CZH_UCAT_PWKan_Example begin end