Theoremsexists_familyOfElements, familyOfElements_compatible, familyOfElements_ofArrows_mk, pullbackCompatible_iff, toCompatible_coe, compPresheafMap, functorPullback, map, pullback, restrict, sieveExtend, to_sieveCompatible, compPresheafMap, map, compPresheafMap_comp, compPresheafMap_id, comp_of_compatible, compatible_singleton_iff, ext, ext_iff, isAmalgamation_iff_ofArrows, isAmalgamation_singleton_iff, map_apply, map_comp, map_id, restrict_map, singletonEquiv_apply, singletonEquiv_symm_apply, singletonEquiv_symm_apply_self, ext, isSheafFor, functorInclusion_comp_extend, functorInclusion_comp_extend_assoc, hom_ext, isAmalgamation, isSeparatedFor, unique_extend, valid_glue, compatibleEquivGenerateSieveCompatible_apply_coe, compatibleEquivGenerateSieveCompatible_symm_apply_coe, compatible_iff_sieveCompatible, extend_agrees, extend_restrict, extension_iff_amalgamation, isAmalgamation_restrict, isAmalgamation_sieveExtend, isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor, isSeparatedFor_iff_generate, isSeparatedFor_iso, isSeparatedFor_singleton, isSeparatedFor_top, isSheafFor_arrows_iff, isSheafFor_arrows_iff_pullbacks, isSheafFor_bind, isSheafFor_iff_generate, isSheafFor_iff_of_iso, isSheafFor_iff_yonedaSheafCondition, isSheafFor_iso, isSheafFor_ofArrows_iff_bijective_toCompabible, isSheafFor_of_nat_equiv, isSheafFor_over_map_op_comp_iff, isSheafFor_over_map_op_comp_ofArrows_iff, isSheafFor_pullback_iff, isSheafFor_singleton, isSheafFor_singleton_iso, isSheafFor_subsieve, isSheafFor_subsieve_aux, isSheafFor_top, isSheafFor_top_sieve, isSheafFor_trans, is_compatible_of_exists_amalgamation, pullbackCompatible_iff, restrict_extend, restrict_inj | 74 |