Diffusion afp-devel 68412a363595

creation and preservation of limits; a variety of auxiliary results and…
68412a363595
Actions

Tags

None

Subscribers

None

Description

creation and preservation of limits; a variety of auxiliary results and amendments

Details

Provenance

user9716869 <user9716869@gmail.com>

Authored on

Parents

rAFPa3f22844a82d: patched a broken proof

Branches

Unknown

Tags

Unknown

Event Timeline

user9716869 <user9716869@gmail.com> committed rAFP68412a363595: creation and preservation of limits; a variety of auxiliary results and….May 16 2022, 1:04 AM

Changes (73)

Path

Size

CZH_Elementary_Categories

czh_ecategories

CZH_DG_FUNCT.thy

CZH_ECAT_CAT.thy

CZH_ECAT_Category.thy

CZH_ECAT_Comma.thy

CZH_ECAT_Conclusions.thy

CZH_ECAT_Cone.thy

CZH_ECAT_FUNCT.thy

CZH_ECAT_Functor.thy

CZH_ECAT_GRPH.thy

CZH_ECAT_Introduction.thy

CZH_ECAT_NTCF.thy

CZH_ECAT_PCategory.thy

CZH_ECAT_Par.thy

CZH_ECAT_Parallel.thy

CZH_ECAT_Rel.thy

CZH_ECAT_SS.thy

CZH_ECAT_SemiCAT.thy

CZH_ECAT_Set.thy

CZH_ECAT_Simple.thy

CZH_ECAT_Small_Cone.thy

CZH_ECAT_Small_NTCF.thy

CZH_ECAT_Structure_Example.thy

CZH_ECAT_Subcategory.thy

CZH_ECAT_Yoneda.thy

CZH_Foundations/

czh_digraphs/

CZH_DG_DGHM.thy

CZH_DG_Digraph.thy

CZH_DG_GRPH.thy

CZH_DG_Introduction.thy

czh_introduction/

CZH_Introduction.thy

czh_semicategories/

CZH_SMC_GRPH.thy

CZH_SMC_Par.thy

CZH_SMC_Rel.thy

CZH_SMC_Semicategory.thy

CZH_SMC_Semifunctor.thy

CZH_SMC_Set.thy

czh_sets/

CZH_Sets_BRelations.thy

CZH_Sets_FBRelations.thy

CZH_Sets_FSequences.thy

CZH_Sets_IF.thy

CZH_Sets_Introduction.thy

CZH_Sets_NOP.thy

CZH_Sets_Nat.thy

CZH_Sets_Sets.thy

CZH_Sets_VNHS.thy

CZH_Sets_ZQR.thy

ex/

CZH_EX_Algebra.thy

document/

CZH_Universal_Constructions

czh_ucategories

CZH_UCAT_Adjoints.thy

CZH_UCAT_Comma.thy

CZH_UCAT_Complete.thy

CZH_UCAT_Conclusions.thy

CZH_UCAT_Kan.thy

CZH_UCAT_Limit.thy

CZH_UCAT_Limit_Equalizer.thy

CZH_UCAT_Limit_IT.thy

CZH_UCAT_Limit_Product.thy

CZH_UCAT_Limit_Pullback.thy

CZH_UCAT_PWKan.thy

CZH_UCAT_PWKan_Example.thy

CZH_UCAT_Pointed.thy

CZH_UCAT_Representable.thy

CZH_UCAT_Set.thy

CZH_UCAT_Universal.thy

rAFP68412a363595

thys/CZH_Elementary_Categories/czh_ecategories/CZH_DG_CAT.thy

Loading...

thys/CZH_Elementary_Categories/czh_ecategories/CZH_DG_FUNCT.thy

Loading...

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_CAT.thy

Loading...

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Category.thy

Loading...

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Comma.thy

Loading...

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Conclusions.thy

Loading...

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Cone.thy

Loading...

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_FUNCT.thy

Loading...

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Functor.thy

Loading...

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_GRPH.thy

Loading...

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Introduction.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_Par.thy

Loading...

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Parallel.thy

Loading...

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Rel.thy

Loading...

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_SS.thy

Loading...

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_SemiCAT.thy

Loading...

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Set.thy

Loading...

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Simple.thy

Loading...

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Small_Cone.thy

Loading...

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Small_NTCF.thy

Loading...

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Structure_Example.thy

Loading...

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Subcategory.thy

Loading...

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Yoneda.thy

Loading...

thys/CZH_Foundations/ROOT

Loading...

thys/CZH_Foundations/czh_digraphs/CZH_DG_DGHM.thy

Loading...

thys/CZH_Foundations/czh_digraphs/CZH_DG_Digraph.thy

Loading...

thys/CZH_Foundations/czh_digraphs/CZH_DG_GRPH.thy

Loading...

thys/CZH_Foundations/czh_digraphs/CZH_DG_Introduction.thy

Loading...

thys/CZH_Foundations/czh_digraphs/CZH_DG_Par.thy

Loading...

thys/CZH_Foundations/czh_digraphs/CZH_DG_Rel.thy

Loading...

thys/CZH_Foundations/czh_digraphs/CZH_DG_Set.thy

Loading...

thys/CZH_Foundations/czh_introduction/CZH_Introduction.thy

Loading...

thys/CZH_Foundations/czh_semicategories/CZH_SMC_GRPH.thy

Loading...

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Par.thy

Loading...

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Rel.thy

Loading...

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Semicategory.thy

Loading...

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Semifunctor.thy

Loading...

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Set.thy

Loading...

thys/CZH_Foundations/czh_sets/CZH_Sets_BRelations.thy

Loading...

thys/CZH_Foundations/czh_sets/CZH_Sets_FBRelations.thy

Loading...

thys/CZH_Foundations/czh_sets/CZH_Sets_FSequences.thy

Loading...

thys/CZH_Foundations/czh_sets/CZH_Sets_IF.thy

Loading...

thys/CZH_Foundations/czh_sets/CZH_Sets_Introduction.thy

Loading...

thys/CZH_Foundations/czh_sets/CZH_Sets_NOP.thy

Loading...

thys/CZH_Foundations/czh_sets/CZH_Sets_Nat.thy

Loading...

thys/CZH_Foundations/czh_sets/CZH_Sets_Sets.thy

Loading...

thys/CZH_Foundations/czh_sets/CZH_Sets_VNHS.thy

Loading...

thys/CZH_Foundations/czh_sets/CZH_Sets_ZQR.thy

Loading...

thys/CZH_Foundations/czh_sets/ex/CZH_EX_Algebra.thy

Loading...

thys/CZH_Foundations/document/root.bib

Loading...

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Adjoints.thy

Loading...

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Comma.thy

Loading...

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Complete.thy

Loading...

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Conclusions.thy

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_Limit_Equalizer.thy

Loading...

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Limit_IT.thy

Loading...

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Limit_Product.thy

Loading...

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Limit_Pullback.thy

Loading...

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_PWKan.thy

Loading...

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_PWKan_Example.thy

Loading...

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Pointed.thy

Loading...

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Representable.thy

Loading...

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Set.thy

Loading...

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Universal.thy

Loading...