Diffusion afp-devel fee517746747

CZH: further results about comma categories and Kan extensions, a variety of…
fee517746747
Actions

Tags

None

Subscribers

None

Description

CZH: further results about comma categories and Kan extensions, a variety of other minor amendments

Details

Provenance

user9716869 <user9716869@gmail.com>

Authored on

Parents

rAFP99b814982902: more generic bit/word lemmas for distribution

Branches

Unknown

Tags

Unknown

Event Timeline

user9716869 <user9716869@gmail.com> committed rAFPfee517746747: CZH: further results about comma categories and Kan extensions, a variety of….Oct 27 2021, 4:44 PM

Changes (12)

Path

Size

thys/

CZH_Elementary_Categories/

czh_ecategories/

CZH_ECAT_Comma.thy

CZH_ECAT_Functor.thy

CZH_ECAT_NTCF.thy

CZH_ECAT_PCategory.thy

CZH_ECAT_Simple.thy

CZH_ECAT_Yoneda.thy

CZH_Foundations/

czh_digraphs/

CZH_DG_DGHM.thy

czh_semicategories/

CZH_SMC_Semifunctor.thy

CZH_Universal_Constructions/

czh_ucategories/

CZH_UCAT_Kan.thy

CZH_UCAT_Limit.thy

CZH_UCAT_PWKan.thy

rAFPfee517746747

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Comma.thy

Loading...

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Functor.thy

Loading...

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_NTCF.thy

Loading...

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_PCategory.thy

Loading...

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Simple.thy

Loading...

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Yoneda.thy

Loading...

thys/CZH_Foundations/czh_digraphs/CZH_DG_DGHM.thy

Loading...

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Semifunctor.thy

Loading...

thys/CZH_Universal_Constructions/ROOT

Loading...

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Kan.thy

Loading...

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Limit.thy

Loading...

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_PWKan.thy

Loading...