Theoremsinitial_pre, coconesEquiv_counitIso, coconesEquiv_functor, coconesEquiv_inverse, coconesEquiv_unitIso, colimitCoconeComp_cocone, colimitCoconeComp_isColimit, colimitCoconeOfComp_cocone, colimitCoconeOfComp_isColimit, colimitIso_hom, colimitIso_inv, colimit_cocone_comp_aux, colimit_pre_isIso, comp_hasColimit, comp_preservesColimit, comp_reflectsColimit, extendCocone_map_hom, extendCocone_obj_pt, extendCocone_obj_ι_app, extendCocone_obj_ι_app', hasColimit_comp_iff, hasColimit_of_comp, hasColimitsOfShape_of_final, instNonemptyStructuredArrow, out, preservesColimit_of_comp, preservesColimitsOfShape_of_final, reflectsColimit_of_comp, reflectsColimitsOfShape_of_final, zigzag_of_eqvGen_colimitTypeRel, ι_colimitIso_hom, ι_colimitIso_hom_assoc, ι_colimitIso_inv, ι_colimitIso_inv_assoc, comp_hasLimit, comp_preservesLimit, comp_reflectsLimit, conesEquiv_counitIso, conesEquiv_functor, conesEquiv_inverse, conesEquiv_unitIso, extendCone_map_hom, extendCone_obj_pt, extendCone_obj_π_app, extendCone_obj_π_app', hasLimit_comp_iff, hasLimit_of_comp, hasLimitsOfShape_of_initial, instNonemptyCostructuredArrow, limitConeComp_cone, limitConeComp_isLimit, limitConeOfComp_cone, limitConeOfComp_isLimit, limitIso_hom, limitIso_inv, limit_cone_comp_aux, limit_pre_isIso, out, preservesLimit_of_comp, preservesLimitsOfShape_of_initial, reflectsLimit_of_comp, reflectsLimitsOfShape_of_initial, final_comp, final_comp_equivalence, final_equivalence_comp, final_fromPUnit_of_isTerminal, final_iff_comp_equivalence, final_iff_comp_final_full_faithful, final_iff_equivalence_comp, final_iff_final_comp, final_iff_isIso_colimit_pre, final_natIso_iff, final_of_adjunction, final_of_colimit_comp_coyoneda_iso_pUnit, final_of_comp_full_faithful, final_of_comp_full_faithful', final_of_equivalence_comp, final_of_final_comp, final_of_initial_op, final_of_isRightAdjoint, final_of_isTerminal_colimit_comp_yoneda, final_of_natIso, final_op_of_initial, initial_comp, initial_comp_equivalence, initial_equivalence_comp, initial_fromPUnit_of_isInitial, initial_iff_comp_equivalence, initial_iff_comp_initial_full_faithful, initial_iff_equivalence_comp, initial_iff_initial_comp, initial_natIso_iff, initial_of_adjunction, initial_of_comp_full_faithful, initial_of_comp_full_faithful', initial_of_equivalence_comp, initial_of_final_op, initial_of_initial_comp, initial_of_isLeftAdjoint, initial_of_natIso, initial_op_of_final, instFinalOppositeLeftOpOfInitial, instFinalOppositeRightOpOfInitial, instInitialOppositeLeftOpOfFinal, instInitialOppositeRightOpOfFinal, final_map, final_pre, of_initial, of_initial, of_final, of_final, initial_ι, final_pre, instFinalProdProd, instInitialCostructuredArrowOverToOver, instInitialProdProd | 116 |