Basic

📁 Source: Mathlib/CategoryTheory/WithTerminal/Basic.lean

Statistics

Metric	Count
Definitions WithInitial, comp, down, equivComma, homTo, id, incl, inclLift, inclLiftToInitial, instCategory, instUniqueHomStar, liftStar, liftToInitial, liftToInitialUnique, liftUnique, map, mapComp, mapId, map₂, mkCommaMorphism, mkCommaObject, ofCommaMorphism, ofCommaObject, opEquiv, prelaxfunctor, pseudofunctor, starInitial, starIsoInitial, WithTerminal, comp, down, equivComma, homFrom, id, incl, inclLift, inclLiftToTerminal, instCategory, instUniqueHomStar, liftStar, liftToTerminal, liftToTerminalUnique, liftUnique, map, mapComp, mapId, map₂, mkCommaMorphism, mkCommaObject, ofCommaMorphism, ofCommaObject, opEquiv, prelaxfunctor, pseudofunctor, starIsoTerminal, starTerminal, widePullbackShapeEquiv, instInhabitedWithInitial, default, instInhabitedWithTerminal, default	61
Theorems down_comp, down_id, equivComma_counitIso_hom_app_left, equivComma_counitIso_hom_app_right_app, equivComma_counitIso_inv_app_left, equivComma_counitIso_inv_app_right_app, equivComma_functor_map_left, equivComma_functor_map_right_app, equivComma_functor_obj_hom_app, equivComma_functor_obj_left, equivComma_functor_obj_right_map, equivComma_functor_obj_right_obj, equivComma_inverse_map_app, equivComma_inverse_obj_map, equivComma_inverse_obj_obj, equivComma_unitIso_hom_app_app, equivComma_unitIso_inv_app_app, false_of_to_star, false_of_to_star', inclLiftToInitial_hom_app, inclLiftToInitial_inv_app, inclLift_hom_app, inclLift_inv_app, instFaithfulIncl, instFullIncl, instHasInitial, isIso_of_to_star, liftStar_hom, liftStar_inv, liftStar_lift_map, liftToInitialUnique_hom_app, liftToInitialUnique_inv_app, liftToInitial_map, liftToInitial_obj, lift_map, lift_obj, mapComp_hom_app, mapComp_inv_app, mapId_hom_app, mapId_inv_app, map_map, map_obj, map₂_app, mkCommaMorphism_left, mkCommaMorphism_right_app, mkCommaObject_hom_app, mkCommaObject_left, mkCommaObject_right_map, mkCommaObject_right_obj, ofCommaMorphism_app, ofCommaObject_map, ofCommaObject_obj, opEquiv_counitIso_hom_app, opEquiv_counitIso_inv_app, opEquiv_functor_map, opEquiv_functor_obj, opEquiv_inverse_map, opEquiv_inverse_obj, opEquiv_unitIso_hom_app, opEquiv_unitIso_inv_app, prelaxfunctor_toPrelaxFunctorStruct_map₂, prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj, pseudofunctor_mapComp, pseudofunctor_mapId, pseudofunctor_toPrelaxFunctor, starIsoInitial_hom, starIsoInitial_inv, down_comp, down_id, equivComma_counitIso_hom_app_left_app, equivComma_counitIso_hom_app_right, equivComma_counitIso_inv_app_left_app, equivComma_counitIso_inv_app_right, equivComma_functor_map_left_app, equivComma_functor_map_right, equivComma_functor_obj_hom_app, equivComma_functor_obj_left_map, equivComma_functor_obj_left_obj, equivComma_functor_obj_right, equivComma_inverse_map_app, equivComma_inverse_obj_map, equivComma_inverse_obj_obj, equivComma_unitIso_hom_app_app, equivComma_unitIso_inv_app_app, false_of_from_star, false_of_from_star', inclLiftToTerminal_hom_app, inclLiftToTerminal_inv_app, inclLift_hom_app, inclLift_inv_app, instFaithfulIncl, instFullIncl, instHasTerminal, isIso_of_from_star, liftStar_hom, liftStar_inv, liftToTerminalUnique_hom_app, liftToTerminalUnique_inv_app, liftToTerminal_map, liftToTerminal_obj, lift_map, lift_map_liftStar, lift_obj, mapComp_hom_app, mapComp_inv_app, mapId_hom_app, mapId_inv_app, map_map, map_obj, map₂_app, mkCommaMorphism_left_app, mkCommaMorphism_right, mkCommaObject_hom_app, mkCommaObject_left_map, mkCommaObject_left_obj, mkCommaObject_right, ofCommaMorphism_app, ofCommaObject_map, ofCommaObject_obj, opEquiv_counitIso_hom_app, opEquiv_counitIso_inv_app, opEquiv_functor_map, opEquiv_functor_obj, opEquiv_inverse_map, opEquiv_inverse_obj, opEquiv_unitIso_hom_app, opEquiv_unitIso_inv_app, prelaxfunctor_toPrelaxFunctorStruct_map₂, prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj, pseudofunctor_mapComp, pseudofunctor_mapId, pseudofunctor_toPrelaxFunctor, starIsoTerminal_hom, starIsoTerminal_inv, subsingleton_hom, widePullbackShapeEquiv_functor_obj, widePullbackShapeEquiv_inverse_obj	139
Total	200

CategoryTheory

Definitions

Name	Category	Theorems
WithInitial 📖	CompData	142 math math: AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_left, WithInitial.equivComma_functor_obj_right_obj, WithInitial.opEquiv_unitIso_inv_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_map_app, WithInitial.isColimitEquiv_apply_desc_right, WithInitial.liftToInitialUnique_hom_app, WithInitial.coconeEquiv_functor_obj_pt, WithTerminal.opEquiv_inverse_obj, WithInitial.liftToInitial_obj, WithInitial.down_id, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_left, WithInitial.coconeEquiv_inverse_obj_pt_right, WithInitial.opEquiv_functor_map, AugmentedSimplexCategory.eqToHom_toOrderHom, WithInitial.ofCommaObject_obj, WithInitial.opEquiv_counitIso_hom_app, WithInitial.isColimitEquiv_symm_apply_desc, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_map_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompPointIso_hom_app, WithInitial.liftFromUnderComp_inv_app, WithTerminal.opEquiv_counitIso_inv_app, WithInitial.equivComma_functor_obj_right_map, WithInitial.equivComma_counitIso_hom_app_right_app, WithInitial.instFaithfulIncl, WithInitial.coconeEquiv_inverse_obj_pt_hom, WithInitial.inclLift_hom_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_obj_map, WithInitial.mkCommaMorphism_right_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_obj_obj, WithTerminal.opEquiv_unitIso_hom_app, WithTerminal.opEquiv_counitIso_hom_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso_inv_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso_hom_app, WithInitial.mkCommaObject_right_obj, WithInitial.mapId_inv_app, WithInitial.equivComma_counitIso_inv_app_right_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_map_left, WithInitial.coconeEquiv_counitIso_inv_app_hom, WithInitial.mkCommaMorphism_left, WithInitial.opEquiv_inverse_obj, WithInitial.liftStar_lift_map, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_obj, WithInitial.coconeEquiv_functor_obj_ι_app_star, WithInitial.instFullIncl, WithInitial.inclLiftToInitial_inv_app, WithInitial.coconeEquiv_unitIso_hom_app_hom_right, WithInitial.mkCommaObject_hom_app, WithInitial.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj, WithInitial.prelaxfunctor_toPrelaxFunctorStruct_map₂, WithInitial.starIsoInitial_inv, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_right, WithInitial.liftFromUnder_obj_obj, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_left_app, WithInitial.coconeEquiv_functor_map_hom, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_hom_app_app, WithInitial.equivComma_functor_map_left, WithInitial.coconeEquiv_inverse_obj_pt_left_as, WithTerminal.opEquiv_functor_obj, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_right, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompPointIso_inv_app, WithInitial.equivComma_inverse_map_app, WithInitial.equivComma_counitIso_hom_app_left, AugmentedSimplexCategory.id_star_whiskerRight, WithInitial.equivComma_functor_map_right_app, WithInitial.coconeEquiv_inverse_obj_ι_app_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_right, WithInitial.instHasInitial, WithInitial.coconeEquiv_functor_obj_ι_app_of, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_left_app, WithInitial.mkCommaObject_right_map, WithInitial.equivComma_functor_obj_hom_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_right, WithInitial.equivComma_inverse_obj_map, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_left, WithInitial.pseudofunctor_mapId, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_left_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_hom_app_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_hom_app, WithInitial.opEquiv_counitIso_inv_app, WithInitial.map_map, WithInitial.equivComma_unitIso_inv_app_app, WithInitial.equivComma_functor_obj_left, WithInitial.inclLift_inv_app, WithInitial.inclLiftToInitial_hom_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_inv_app_app, WithInitial.equivComma_unitIso_hom_app_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_right, WithInitial.map₂_app, WithInitial.equivComma_inverse_obj_obj, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_hom_app_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_inv_app_app, WithInitial.coconeEquiv_inverse_map_hom_right, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_left, WithInitial.equivComma_counitIso_inv_app_left, WithInitial.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, WithInitial.map_obj, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_left, WithInitial.liftFromUnderComp_hom_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_right, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_inv_app_app, WithInitial.coconeEquiv_counitIso_hom_app_hom, WithInitial.liftFromUnder_map_app, WithInitial.opEquiv_functor_obj, WithInitial.mkCommaObject_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_right_app, WithInitial.lift_map, WithInitial.starIsoInitial_hom, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_right_map, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_right, WithInitial.liftToInitial_map, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_map, WithInitial.ofCommaObject_map, WithInitial.liftFromUnder_obj_map, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_map_right_app, WithInitial.pseudofunctor_mapComp, WithInitial.opEquiv_inverse_map, WithInitial.liftStar_hom, WithInitial.isIso_of_to_star, WithInitial.liftToInitialUnique_inv_app, WithInitial.mapComp_inv_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_inv_app_app, WithInitial.opEquiv_unitIso_hom_app, WithInitial.ofCommaMorphism_app, WithInitial.lift_obj, WithTerminal.opEquiv_unitIso_inv_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_map, WithInitial.down_comp, WithInitial.coconeEquiv_unitIso_inv_app_hom_right, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_hom_app, WithTerminal.opEquiv_functor_map, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_right_obj, WithInitial.mapId_hom_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_obj, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_right_app, WithInitial.mapComp_hom_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_hom_app_app, WithInitial.instIsFilteredOfIsFilteredOrEmpty, WithTerminal.opEquiv_inverse_map, WithInitial.liftStar_inv
WithTerminal 📖	CompData	116 math math: WithTerminal.coneEquiv_unitIso_hom_app_hom_left, WithTerminal.mkCommaObject_right, WithTerminal.equivComma_functor_obj_left_obj, WithTerminal.equivComma_counitIso_hom_app_left_app, WithInitial.opEquiv_unitIso_inv_app, WithTerminal.equivComma_counitIso_inv_app_left_app, WithTerminal.liftStar_inv, WithTerminal.instFaithfulIncl, WithTerminal.opEquiv_inverse_obj, Limits.PreservesLimitsOfShape.ofWidePullbacks, WithTerminal.map₂_app, WithTerminal.coneEquiv_inverse_obj_π_app_left, WithTerminal.mapComp_hom_app, WithInitial.opEquiv_functor_map, WithTerminal.equivComma_inverse_obj_obj, WithTerminal.equivComma_counitIso_hom_app_right, WithInitial.opEquiv_counitIso_hom_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_map_app, WithTerminal.equivComma_functor_obj_left_map, WithTerminal.mkCommaMorphism_left_app, WithTerminal.equivComma_functor_obj_right, WithTerminal.ofCommaObject_obj, WithTerminal.opEquiv_counitIso_inv_app, WithTerminal.liftStar_hom, WithTerminal.coneEquiv_functor_obj_π_app_star, WithTerminal.coneEquiv_counitIso_inv_app_hom, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_left, WithTerminal.down_id, WithTerminal.opEquiv_unitIso_hom_app, WithTerminal.opEquiv_counitIso_hom_app, WithTerminal.lift_map, WithTerminal.inclLift_hom_app, WithTerminal.equivComma_functor_map_right, WithTerminal.liftToTerminal_map, WithInitial.opEquiv_inverse_obj, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_obj, WithTerminal.coneEquiv_functor_obj_π_app_of, WithTerminal.map_map, WithTerminal.lift_obj, WithTerminal.liftToTerminal_obj, WithTerminal.coneEquiv_inverse_obj_pt_left, WithTerminal.mkCommaObject_left_map, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_left_app, WithTerminal.ofCommaMorphism_app, WithTerminal.liftToTerminalUnique_inv_app, WithTerminal.mapComp_inv_app, WithTerminal.mkCommaMorphism_right, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_hom_app_app, WithTerminal.opEquiv_functor_obj, WithTerminal.lift_map_liftStar, WithTerminal.inclLiftToTerminal_inv_app, WithTerminal.equivComma_functor_obj_hom_app, WithTerminal.isLimitEquiv_symm_apply_lift, WithTerminal.liftFromOver_obj_obj, WithTerminal.coneEquiv_inverse_obj_pt_hom, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_right, WithTerminal.starIsoTerminal_inv, WithTerminal.liftFromOverComp_hom_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_left_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_right, WithTerminal.inclLift_inv_app, WithTerminal.ofCommaObject_map, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_left, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_left_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_hom_app, WithTerminal.starIsoTerminal_hom, WithInitial.opEquiv_counitIso_inv_app, WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_map₂, WithTerminal.widePullbackShapeEquiv_inverse_obj, WithTerminal.subsingleton_hom, WithTerminal.instHasTerminal, WithTerminal.instIsCofilteredOfIsCofilteredOrEmpty, WithTerminal.map_obj, WithTerminal.mkCommaObject_hom_app, WithTerminal.mkCommaObject_left_obj, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_hom_app_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_inv_app_app, WithTerminal.mapId_hom_app, WithTerminal.inclLiftToTerminal_hom_app, WithTerminal.liftFromOver_obj_map, WithTerminal.isLimitEquiv_apply_lift_left, WithTerminal.pseudofunctor_mapId, WithTerminal.pseudofunctor_mapComp, WithTerminal.instFullIncl, WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj, WithTerminal.coneEquiv_unitIso_inv_app_hom_left, WithTerminal.equivComma_functor_map_left_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_inv_app_app, WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, WithInitial.opEquiv_functor_obj, WithTerminal.down_comp, WithTerminal.mapId_inv_app, WithTerminal.liftFromOverComp_inv_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_map, WithTerminal.equivComma_inverse_map_app, WithTerminal.equivComma_inverse_obj_map, WithTerminal.liftFromOver_map_app, WithTerminal.coneEquiv_inverse_map_hom_left, WithInitial.opEquiv_inverse_map, WithTerminal.coneEquiv_functor_obj_pt, WithTerminal.equivComma_counitIso_inv_app_right, WithInitial.opEquiv_unitIso_hom_app, WithTerminal.equivComma_unitIso_hom_app_app, WithTerminal.opEquiv_unitIso_inv_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_map, WithTerminal.liftToTerminalUnique_hom_app, WithTerminal.opEquiv_functor_map, WithTerminal.equivComma_unitIso_inv_app_app, WithTerminal.coneEquiv_counitIso_hom_app_hom, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_obj, WithTerminal.widePullbackShapeEquiv_functor_obj, WithTerminal.coneEquiv_inverse_obj_pt_right_as, WithTerminal.opEquiv_inverse_map, WithTerminal.coneEquiv_functor_map_hom, WithTerminal.isIso_of_from_star
instInhabitedWithInitial 📖	CompOp	—
instInhabitedWithTerminal 📖	CompOp	—

CategoryTheory.WithInitial

Definitions

Name	Category	Theorems
comp 📖	CompOp	—
down 📖	CompOp	22 math math: opEquiv_unitIso_inv_app, down_id, AugmentedSimplexCategory.eqToHom_toOrderHom, opEquiv_counitIso_hom_app, CategoryTheory.WithTerminal.opEquiv_counitIso_inv_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_obj_map, CategoryTheory.WithTerminal.opEquiv_unitIso_hom_app, CategoryTheory.WithTerminal.opEquiv_counitIso_hom_app, equivComma_inverse_obj_map, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_hom_app, opEquiv_counitIso_inv_app, map_map, lift_map, liftToInitial_map, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_map, ofCommaObject_map, liftFromUnder_obj_map, opEquiv_inverse_map, opEquiv_unitIso_hom_app, CategoryTheory.WithTerminal.opEquiv_unitIso_inv_app, down_comp, CategoryTheory.WithTerminal.opEquiv_inverse_map
equivComma 📖	CompOp	16 math math: equivComma_functor_obj_right_obj, equivComma_functor_obj_right_map, equivComma_counitIso_hom_app_right_app, equivComma_counitIso_inv_app_right_app, equivComma_functor_map_left, equivComma_inverse_map_app, equivComma_counitIso_hom_app_left, equivComma_functor_map_right_app, equivComma_functor_obj_hom_app, equivComma_inverse_obj_map, equivComma_unitIso_inv_app_app, equivComma_functor_obj_left, equivComma_unitIso_hom_app_app, equivComma_inverse_obj_obj, equivComma_counitIso_inv_app_left, liftFromUnder_map_app
homTo 📖	CompOp	8 math math: AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_left, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_right, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_right, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_left, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_right, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_right
id 📖	CompOp	—
incl 📖	CompOp	39 math math: equivComma_functor_obj_right_obj, liftToInitialUnique_hom_app, equivComma_functor_obj_right_map, equivComma_counitIso_hom_app_right_app, instFaithfulIncl, inclLift_hom_app, mkCommaMorphism_right_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_left, mkCommaObject_right_obj, equivComma_counitIso_inv_app_right_app, liftStar_lift_map, instFullIncl, inclLiftToInitial_inv_app, mkCommaObject_hom_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_right, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_right, equivComma_functor_map_right_app, mkCommaObject_right_map, equivComma_functor_obj_hom_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_hom_app_app, equivComma_unitIso_inv_app_app, inclLift_inv_app, inclLiftToInitial_hom_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_inv_app_app, equivComma_unitIso_hom_app_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_right, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_right_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_right_map, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_right, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_map_right_app, liftToInitialUnique_inv_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_inv_app_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_hom_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_right_obj, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_right_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_hom_app_app
inclLift 📖	CompOp	3 math math: inclLift_hom_app, liftStar_lift_map, inclLift_inv_app
inclLiftToInitial 📖	CompOp	2 math math: inclLiftToInitial_inv_app, inclLiftToInitial_hom_app
instCategory 📖	CompOp	163 math math: AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_left, equivComma_functor_obj_right_obj, AugmentedSimplexCategory.inr_comp_associator, opEquiv_unitIso_inv_app, AugmentedSimplexCategory.inclusion_obj, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_map_app, isColimitEquiv_apply_desc_right, liftToInitialUnique_hom_app, coconeEquiv_functor_obj_pt, AugmentedSimplexCategory.whiskerLeft_id_star, CategoryTheory.WithTerminal.opEquiv_inverse_obj, liftToInitial_obj, down_id, AugmentedSimplexCategory.inr_comp_inl_comp_associator, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_left, AugmentedSimplexCategory.inr_comp_inl_comp_associator_assoc, coconeEquiv_inverse_obj_pt_right, opEquiv_functor_map, AugmentedSimplexCategory.eqToHom_toOrderHom, ofCommaObject_obj, opEquiv_counitIso_hom_app, isColimitEquiv_symm_apply_desc, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_map_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompPointIso_hom_app, liftFromUnderComp_inv_app, CategoryTheory.WithTerminal.opEquiv_counitIso_inv_app, equivComma_functor_obj_right_map, equivComma_counitIso_hom_app_right_app, instFaithfulIncl, coconeEquiv_inverse_obj_pt_hom, inclLift_hom_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_obj_map, mkCommaMorphism_right_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_left, AugmentedSimplexCategory.instHasInitial, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_obj_obj, CategoryTheory.WithTerminal.opEquiv_unitIso_hom_app, CategoryTheory.WithTerminal.opEquiv_counitIso_hom_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso_inv_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso_hom_app, mkCommaObject_right_obj, mapId_inv_app, equivComma_counitIso_inv_app_right_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_map_left, AugmentedSimplexCategory.inl_comp_inl_comp_associator_assoc, coconeEquiv_counitIso_inv_app_hom, mkCommaMorphism_left, opEquiv_inverse_obj, liftStar_lift_map, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_obj, coconeEquiv_functor_obj_ι_app_star, instFullIncl, AugmentedSimplexCategory.tensorObj_hom_ext_iff, inclLiftToInitial_inv_app, AugmentedSimplexCategory.inr_comp_associator_assoc, coconeEquiv_unitIso_hom_app_hom_right, AugmentedSimplexCategory.instFullSimplexCategoryInclusion, mkCommaObject_hom_app, prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj, prelaxfunctor_toPrelaxFunctorStruct_map₂, starIsoInitial_inv, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_right, liftFromUnder_obj_obj, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_left_app, coconeEquiv_functor_map_hom, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_hom_app_app, equivComma_functor_map_left, coconeEquiv_inverse_obj_pt_left_as, CategoryTheory.WithTerminal.opEquiv_functor_obj, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_right, AugmentedSimplexCategory.inl_comp_tensorHom, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompPointIso_inv_app, equivComma_inverse_map_app, equivComma_counitIso_hom_app_left, AugmentedSimplexCategory.id_star_whiskerRight, equivComma_functor_map_right_app, coconeEquiv_inverse_obj_ι_app_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_right, instHasInitial, coconeEquiv_functor_obj_ι_app_of, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_left_app, mkCommaObject_right_map, equivComma_functor_obj_hom_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_right, equivComma_inverse_obj_map, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_left, AugmentedSimplexCategory.inl_comp_inl_comp_associator, pseudofunctor_mapId, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_left_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_hom_app_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_hom_app, AugmentedSimplexCategory.instFaithfulSimplexCategoryInclusion, opEquiv_counitIso_inv_app, map_map, equivComma_unitIso_inv_app_app, equivComma_functor_obj_left, inclLift_inv_app, AugmentedSimplexCategory.tensor_id, inclLiftToInitial_hom_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_inv_app_app, AugmentedSimplexCategory.inclusion_map, equivComma_unitIso_hom_app_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_right, map₂_app, equivComma_inverse_obj_obj, AugmentedSimplexCategory.tensorHom_id, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_hom_app_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_inv_app_app, coconeEquiv_inverse_map_hom_right, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_left, equivComma_counitIso_inv_app_left, prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, AugmentedSimplexCategory.id_tensorHom, map_obj, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_left, liftFromUnderComp_hom_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_right, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_inv_app_app, coconeEquiv_counitIso_hom_app_hom, liftFromUnder_map_app, opEquiv_functor_obj, mkCommaObject_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_right_app, lift_map, starIsoInitial_hom, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_right_map, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_right, liftToInitial_map, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_map, ofCommaObject_map, AugmentedSimplexCategory.inr_comp_tensorHom, liftFromUnder_obj_map, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_map_right_app, AugmentedSimplexCategory.inl_comp_tensorHom_assoc, AugmentedSimplexCategory.inr_comp_tensorHom_assoc, pseudofunctor_mapComp, opEquiv_inverse_map, liftStar_hom, isIso_of_to_star, liftToInitialUnique_inv_app, mapComp_inv_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_inv_app_app, opEquiv_unitIso_hom_app, ofCommaMorphism_app, lift_obj, CategoryTheory.WithTerminal.opEquiv_unitIso_inv_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_map, down_comp, coconeEquiv_unitIso_inv_app_hom_right, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_hom_app, CategoryTheory.WithTerminal.opEquiv_functor_map, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_right_obj, mapId_hom_app, AugmentedSimplexCategory.tensorHom_comp_tensorHom, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_obj, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_right_app, mapComp_hom_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_hom_app_app, instIsFilteredOfIsFilteredOrEmpty, CategoryTheory.WithTerminal.opEquiv_inverse_map, liftStar_inv
instUniqueHomStar 📖	CompOp	—
liftStar 📖	CompOp	3 math math: liftStar_lift_map, liftStar_hom, liftStar_inv
liftToInitial 📖	CompOp	6 math math: liftToInitialUnique_hom_app, liftToInitial_obj, inclLiftToInitial_inv_app, inclLiftToInitial_hom_app, liftToInitial_map, liftToInitialUnique_inv_app
liftToInitialUnique 📖	CompOp	2 math math: liftToInitialUnique_hom_app, liftToInitialUnique_inv_app
liftUnique 📖	CompOp	—
map 📖	CompOp	11 math math: mapId_inv_app, prelaxfunctor_toPrelaxFunctorStruct_map₂, pseudofunctor_mapId, map_map, map₂_app, prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, map_obj, pseudofunctor_mapComp, mapComp_inv_app, mapId_hom_app, mapComp_hom_app
mapComp 📖	CompOp	3 math math: pseudofunctor_mapComp, mapComp_inv_app, mapComp_hom_app
mapId 📖	CompOp	3 math math: mapId_inv_app, pseudofunctor_mapId, mapId_hom_app
map₂ 📖	CompOp	2 math math: prelaxfunctor_toPrelaxFunctorStruct_map₂, map₂_app
mkCommaMorphism 📖	CompOp	14 math math: AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_left, equivComma_counitIso_hom_app_right_app, mkCommaMorphism_right_app, equivComma_counitIso_inv_app_right_app, mkCommaMorphism_left, equivComma_counitIso_hom_app_left, equivComma_unitIso_inv_app_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_inv_app_app, equivComma_unitIso_hom_app_app, equivComma_counitIso_inv_app_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_right_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_right_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_hom_app_app
mkCommaObject 📖	CompOp	22 math math: AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_left, equivComma_counitIso_hom_app_right_app, mkCommaMorphism_right_app, mkCommaObject_right_obj, equivComma_counitIso_inv_app_right_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_map_left, mkCommaMorphism_left, mkCommaObject_hom_app, equivComma_functor_map_left, equivComma_counitIso_hom_app_left, equivComma_functor_map_right_app, mkCommaObject_right_map, equivComma_unitIso_inv_app_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_inv_app_app, equivComma_unitIso_hom_app_app, equivComma_counitIso_inv_app_left, mkCommaObject_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_right_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_map_right_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_right_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_hom_app_app
ofCommaMorphism 📖	CompOp	13 math math: AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_left, equivComma_counitIso_hom_app_right_app, equivComma_counitIso_inv_app_right_app, equivComma_counitIso_hom_app_left, equivComma_unitIso_inv_app_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_inv_app_app, equivComma_unitIso_hom_app_app, equivComma_counitIso_inv_app_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_right_app, ofCommaMorphism_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_right_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_hom_app_app
ofCommaObject 📖	CompOp	17 math math: AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_map_app, ofCommaObject_obj, equivComma_counitIso_hom_app_right_app, equivComma_counitIso_inv_app_right_app, equivComma_inverse_map_app, equivComma_counitIso_hom_app_left, equivComma_unitIso_inv_app_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_inv_app_app, equivComma_unitIso_hom_app_app, equivComma_counitIso_inv_app_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_right_app, ofCommaObject_map, ofCommaMorphism_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_right_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_hom_app_app
opEquiv 📖	CompOp	18 math math: opEquiv_unitIso_inv_app, opEquiv_functor_map, opEquiv_counitIso_hom_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_map_app, opEquiv_inverse_obj, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_left_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_left_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_left_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_hom_app, opEquiv_counitIso_inv_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_hom_app_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_inv_app_app, opEquiv_functor_obj, opEquiv_inverse_map, opEquiv_unitIso_hom_app
prelaxfunctor 📖	CompOp	6 math math: prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj, prelaxfunctor_toPrelaxFunctorStruct_map₂, pseudofunctor_mapId, pseudofunctor_toPrelaxFunctor, prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, pseudofunctor_mapComp
pseudofunctor 📖	CompOp	3 math math: pseudofunctor_mapId, pseudofunctor_toPrelaxFunctor, pseudofunctor_mapComp
starInitial 📖	CompOp	17 math math: opEquiv_unitIso_inv_app, opEquiv_counitIso_hom_app, CategoryTheory.WithTerminal.opEquiv_counitIso_inv_app, CategoryTheory.WithTerminal.opEquiv_unitIso_hom_app, CategoryTheory.WithTerminal.opEquiv_counitIso_hom_app, liftStar_lift_map, mkCommaObject_hom_app, equivComma_functor_obj_hom_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_hom_app, opEquiv_counitIso_inv_app, starIsoInitial_hom, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_map, opEquiv_inverse_map, opEquiv_unitIso_hom_app, CategoryTheory.WithTerminal.opEquiv_unitIso_inv_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_hom_app, CategoryTheory.WithTerminal.opEquiv_functor_map
starIsoInitial 📖	CompOp	2 math math: starIsoInitial_inv, starIsoInitial_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
down_comp 📖	mathematical	—	down CategoryTheory.CategoryStruct.comp CategoryTheory.WithInitial CategoryTheory.Category.toCategoryStruct instCategory of	—	—
down_id 📖	mathematical	—	down CategoryTheory.CategoryStruct.id CategoryTheory.WithInitial CategoryTheory.Category.toCategoryStruct instCategory of	—	—
equivComma_counitIso_hom_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.comp CategoryTheory.WithInitial instCategory ofCommaObject ofCommaMorphism mkCommaObject mkCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Equivalence.counitIso equivComma CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	—
equivComma_counitIso_hom_app_right_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Comma.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.comp CategoryTheory.WithInitial instCategory ofCommaObject ofCommaMorphism mkCommaObject mkCommaMorphism CategoryTheory.CommaMorphism.right CategoryTheory.Iso.hom CategoryTheory.Equivalence.counitIso equivComma CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct incl CategoryTheory.Comma.left	—	—
equivComma_counitIso_inv_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.comp CategoryTheory.WithInitial instCategory ofCommaObject ofCommaMorphism mkCommaObject mkCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Equivalence.counitIso equivComma CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	—
equivComma_counitIso_inv_app_right_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Comma.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.comp CategoryTheory.WithInitial instCategory ofCommaObject ofCommaMorphism mkCommaObject mkCommaMorphism CategoryTheory.CommaMorphism.right CategoryTheory.Iso.inv CategoryTheory.Equivalence.counitIso equivComma CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct incl CategoryTheory.Comma.left	—	—
equivComma_functor_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id mkCommaObject CategoryTheory.Functor.map CategoryTheory.WithInitial instCategory CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor equivComma CategoryTheory.NatTrans.app star	—	—
equivComma_functor_map_right_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.WithInitial instCategory incl CategoryTheory.CommaMorphism.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id mkCommaObject CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor equivComma CategoryTheory.Functor.obj	—	—
equivComma_functor_obj_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.WithInitial instCategory star CategoryTheory.Functor.id CategoryTheory.Functor.comp incl CategoryTheory.Comma.hom CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor equivComma CategoryTheory.Functor.map CategoryTheory.Limits.IsInitial.to starInitial of	—	—
equivComma_functor_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.WithInitial instCategory CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor equivComma star	—	—
equivComma_functor_obj_right_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Comma.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.WithInitial instCategory CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor equivComma incl	—	—
equivComma_functor_obj_right_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.WithInitial instCategory CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor equivComma incl	—	—
equivComma_inverse_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithInitial instCategory ofCommaObject CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse equivComma Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.left CategoryTheory.CommaMorphism.right CategoryTheory.CommaMorphism.left	—	—
equivComma_inverse_obj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.WithInitial instCategory CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse equivComma Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Comma.left down CategoryTheory.NatTrans.app CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id	—	—
equivComma_inverse_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.WithInitial instCategory CategoryTheory.Comma CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse equivComma CategoryTheory.Comma.right CategoryTheory.Comma.left	—	—
equivComma_unitIso_hom_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithInitial instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Comma CategoryTheory.Functor.const CategoryTheory.commaCategory mkCommaObject mkCommaMorphism ofCommaObject ofCommaMorphism CategoryTheory.Iso.hom CategoryTheory.Equivalence.unitIso equivComma incl star CategoryTheory.Iso CategoryTheory.Iso.app CategoryTheory.Iso.refl	—	—
equivComma_unitIso_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithInitial instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Comma CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.commaCategory mkCommaObject mkCommaMorphism ofCommaObject ofCommaMorphism CategoryTheory.Iso.inv CategoryTheory.Equivalence.unitIso equivComma incl star CategoryTheory.Iso CategoryTheory.Iso.app CategoryTheory.Iso.refl	—	—
false_of_to_star 📖	—	—	—	—	—
false_of_to_star' 📖	—	—	—	—	—
inclLiftToInitial_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.WithInitial instCategory incl lift CategoryTheory.Limits.IsInitial.to CategoryTheory.Functor.obj CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category liftToInitial inclLiftToInitial CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
inclLiftToInitial_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.WithInitial instCategory incl lift CategoryTheory.Limits.IsInitial.to CategoryTheory.Functor.obj CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category liftToInitial inclLiftToInitial CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
inclLift_hom_app 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.WithInitial instCategory incl lift CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category inclLift CategoryTheory.CategoryStruct.id	—	—
inclLift_inv_app 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.WithInitial instCategory incl lift CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category inclLift CategoryTheory.CategoryStruct.id	—	—
instFaithfulIncl 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.WithInitial instCategory incl	—	—
instFullIncl 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.WithInitial instCategory incl	—	—
instHasInitial 📖	mathematical	—	CategoryTheory.Limits.HasInitial CategoryTheory.WithInitial instCategory	—	CategoryTheory.Limits.hasInitial_of_unique Unique.instSubsingleton
isIso_of_to_star 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.WithInitial instCategory star	—	—
liftStar_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.Iso.hom CategoryTheory.WithInitial instCategory lift star liftStar CategoryTheory.CategoryStruct.id	—	—
liftStar_inv 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.Iso.inv CategoryTheory.WithInitial instCategory lift star liftStar CategoryTheory.CategoryStruct.id	—	—
liftStar_lift_map 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.WithInitial instCategory lift star incl CategoryTheory.Iso.hom liftStar CategoryTheory.Limits.IsInitial.to starInitial CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category inclLift	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
liftToInitialUnique_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithInitial instCategory lift CategoryTheory.Limits.IsInitial.to CategoryTheory.Functor.obj CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category liftToInitial liftToInitialUnique CategoryTheory.Iso CategoryTheory.Iso.app CategoryTheory.Functor.comp incl	—	—
liftToInitialUnique_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithInitial instCategory lift CategoryTheory.Limits.IsInitial.to CategoryTheory.Functor.obj CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category liftToInitial liftToInitialUnique CategoryTheory.Iso CategoryTheory.Iso.app CategoryTheory.Functor.comp incl	—	—
liftToInitial_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.WithInitial instCategory liftToInitial Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj down CategoryTheory.Limits.IsInitial.to CategoryTheory.CategoryStruct.id	—	—
liftToInitial_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.WithInitial instCategory liftToInitial	—	—
lift_map 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.WithInitial instCategory lift Quiver.Hom CategoryTheory.CategoryStruct.toQuiver down CategoryTheory.CategoryStruct.id star	—	—
lift_obj 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.WithInitial instCategory lift	—	—
mapComp_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithInitial instCategory map CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category mapComp of CategoryTheory.Functor.obj star CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
mapComp_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithInitial instCategory CategoryTheory.Functor.comp map CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category mapComp of CategoryTheory.Functor.obj star CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
mapId_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithInitial instCategory map CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category mapId of star CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
mapId_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithInitial instCategory CategoryTheory.Functor.id map CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category mapId of star CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
map_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.WithInitial instCategory map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct of CategoryTheory.Functor.obj star down	—	—
map_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.WithInitial instCategory map of star	—	—
map₂_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithInitial instCategory map map₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.id star	—	—
mkCommaMorphism_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id mkCommaObject mkCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.WithInitial instCategory star	—	—
mkCommaMorphism_right_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.WithInitial instCategory incl CategoryTheory.CommaMorphism.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id mkCommaObject mkCommaMorphism CategoryTheory.Functor.obj	—	—
mkCommaObject_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.WithInitial instCategory star CategoryTheory.Functor.id CategoryTheory.Functor.comp incl CategoryTheory.Comma.hom mkCommaObject CategoryTheory.Functor.map CategoryTheory.Limits.IsInitial.to starInitial of	—	—
mkCommaObject_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id mkCommaObject CategoryTheory.Functor.obj CategoryTheory.WithInitial instCategory star	—	—
mkCommaObject_right_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Comma.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id mkCommaObject CategoryTheory.WithInitial instCategory CategoryTheory.Functor.obj incl	—	—
mkCommaObject_right_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id mkCommaObject CategoryTheory.WithInitial instCategory incl	—	—
ofCommaMorphism_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithInitial instCategory ofCommaObject ofCommaMorphism Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.CommaMorphism.right CategoryTheory.CommaMorphism.left	—	—
ofCommaObject_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.WithInitial instCategory ofCommaObject Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.Comma.left down CategoryTheory.NatTrans.app CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id	—	—
ofCommaObject_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.WithInitial instCategory ofCommaObject CategoryTheory.Comma.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.id CategoryTheory.Comma.left	—	—
opEquiv_counitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithTerminal Opposite CategoryTheory.WithTerminal.instCategory CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.WithInitial instCategory Opposite.op of Opposite.unop star Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct down CategoryTheory.WithTerminal.of CategoryTheory.WithTerminal.star CategoryTheory.Limits.IsInitial.to starInitial CategoryTheory.CategoryStruct.id CategoryTheory.CategoryStruct.opposite Quiver.Hom.op CategoryTheory.WithTerminal.down CategoryTheory.Limits.IsTerminal.from CategoryTheory.WithTerminal.starTerminal CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso opEquiv CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
opEquiv_counitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithTerminal Opposite CategoryTheory.WithTerminal.instCategory CategoryTheory.Category.opposite CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.WithInitial instCategory Opposite.op of Opposite.unop star Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct down CategoryTheory.WithTerminal.of CategoryTheory.WithTerminal.star CategoryTheory.Limits.IsInitial.to starInitial CategoryTheory.CategoryStruct.id CategoryTheory.CategoryStruct.opposite Quiver.Hom.op CategoryTheory.WithTerminal.down CategoryTheory.Limits.IsTerminal.from CategoryTheory.WithTerminal.starTerminal CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso opEquiv CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
opEquiv_functor_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.WithInitial CategoryTheory.Category.opposite instCategory CategoryTheory.WithTerminal CategoryTheory.WithTerminal.instCategory CategoryTheory.Equivalence.functor opEquiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.WithTerminal.of Opposite.op CategoryTheory.WithTerminal.star Quiver.Hom.op CategoryTheory.WithTerminal.down CategoryTheory.Limits.IsTerminal.from CategoryTheory.WithTerminal.starTerminal CategoryTheory.CategoryStruct.id	—	—
opEquiv_functor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.WithInitial CategoryTheory.Category.opposite instCategory CategoryTheory.WithTerminal CategoryTheory.WithTerminal.instCategory CategoryTheory.Equivalence.functor opEquiv Opposite.unop CategoryTheory.WithTerminal.of Opposite.op CategoryTheory.WithTerminal.star	—	—
opEquiv_inverse_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.WithTerminal Opposite CategoryTheory.WithTerminal.instCategory CategoryTheory.Category.opposite CategoryTheory.WithInitial instCategory CategoryTheory.Equivalence.inverse opEquiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.op of Opposite.unop star down CategoryTheory.Limits.IsInitial.to starInitial CategoryTheory.CategoryStruct.id CategoryTheory.CategoryStruct.opposite	—	—
opEquiv_inverse_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.WithTerminal Opposite CategoryTheory.WithTerminal.instCategory CategoryTheory.Category.opposite CategoryTheory.WithInitial instCategory CategoryTheory.Equivalence.inverse opEquiv Opposite.op of Opposite.unop star	—	—
opEquiv_unitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.WithInitial CategoryTheory.Category.opposite instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.WithTerminal CategoryTheory.WithTerminal.instCategory CategoryTheory.WithTerminal.of Opposite.op CategoryTheory.WithTerminal.star Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.op CategoryTheory.WithTerminal.down CategoryTheory.Limits.IsTerminal.from CategoryTheory.WithTerminal.starTerminal of CategoryTheory.CategoryStruct.id star Opposite.unop down CategoryTheory.Limits.IsInitial.to starInitial CategoryTheory.CategoryStruct.opposite CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso opEquiv CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
opEquiv_unitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.WithInitial CategoryTheory.Category.opposite instCategory CategoryTheory.Functor.comp CategoryTheory.WithTerminal CategoryTheory.WithTerminal.instCategory CategoryTheory.WithTerminal.of Opposite.op CategoryTheory.WithTerminal.star Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.op CategoryTheory.WithTerminal.down CategoryTheory.Limits.IsTerminal.from CategoryTheory.WithTerminal.starTerminal of CategoryTheory.CategoryStruct.id star Opposite.unop down CategoryTheory.Limits.IsInitial.to starInitial CategoryTheory.CategoryStruct.opposite CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso opEquiv CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
prelaxfunctor_toPrelaxFunctorStruct_map₂ 📖	mathematical	—	CategoryTheory.PrelaxFunctorStruct.map₂ CategoryTheory.Cat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct prelaxfunctor CategoryTheory.NatTrans.toCatHom₂ CategoryTheory.WithInitial CategoryTheory.Bundled.α CategoryTheory.Category instCategory CategoryTheory.Cat.str map CategoryTheory.Cat.Hom.toFunctor map₂ CategoryTheory.Cat.Hom₂.toNatTrans	—	—
prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map 📖	mathematical	—	Prefunctor.map CategoryTheory.Cat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct prelaxfunctor CategoryTheory.Functor.toCatHom CategoryTheory.WithInitial CategoryTheory.Bundled.α CategoryTheory.Category instCategory CategoryTheory.Cat.str map CategoryTheory.Cat.Hom.toFunctor	—	—
prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj 📖	mathematical	—	Prefunctor.obj CategoryTheory.Cat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct prelaxfunctor CategoryTheory.Cat.of CategoryTheory.WithInitial CategoryTheory.Bundled.α CategoryTheory.Category instCategory CategoryTheory.Cat.str	—	—
pseudofunctor_mapComp 📖	mathematical	—	CategoryTheory.Pseudofunctor.mapComp CategoryTheory.Cat CategoryTheory.Cat.bicategory pseudofunctor CategoryTheory.Cat.Hom.isoMk CategoryTheory.WithInitial CategoryTheory.Bundled.α CategoryTheory.Category instCategory CategoryTheory.Cat.str map CategoryTheory.Cat.Hom.toFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Functor.comp Prefunctor.obj CategoryTheory.CategoryStruct.toQuiver CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct prelaxfunctor Prefunctor.map mapComp	—	—
pseudofunctor_mapId 📖	mathematical	—	CategoryTheory.Pseudofunctor.mapId CategoryTheory.Cat CategoryTheory.Cat.bicategory pseudofunctor CategoryTheory.Cat.Hom.isoMk CategoryTheory.WithInitial CategoryTheory.Bundled.α CategoryTheory.Category instCategory CategoryTheory.Cat.str map CategoryTheory.Cat.Hom.toFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Functor.id Prefunctor.obj CategoryTheory.CategoryStruct.toQuiver CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct prelaxfunctor mapId	—	—
pseudofunctor_toPrelaxFunctor 📖	mathematical	—	CategoryTheory.Pseudofunctor.toPrelaxFunctor CategoryTheory.Cat CategoryTheory.Cat.bicategory pseudofunctor prelaxfunctor	—	—
starIsoInitial_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.WithInitial instCategory star CategoryTheory.Limits.initial instHasInitial starIsoInitial CategoryTheory.Limits.IsInitial.to starInitial	—	instHasInitial
starIsoInitial_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.WithInitial instCategory star CategoryTheory.Limits.initial instHasInitial starIsoInitial CategoryTheory.Limits.IsInitial.to CategoryTheory.Limits.initialIsInitial	—	instHasInitial

CategoryTheory.WithTerminal

Definitions

Name	Category	Theorems
comp 📖	CompOp	—
down 📖	CompOp	21 math math: CategoryTheory.WithInitial.opEquiv_unitIso_inv_app, CategoryTheory.WithInitial.opEquiv_functor_map, CategoryTheory.WithInitial.opEquiv_counitIso_hom_app, opEquiv_counitIso_inv_app, down_id, opEquiv_unitIso_hom_app, opEquiv_counitIso_hom_app, lift_map, liftToTerminal_map, map_map, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_left_app, ofCommaObject_map, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_left_app, CategoryTheory.WithInitial.opEquiv_counitIso_inv_app, liftFromOver_obj_map, down_comp, equivComma_inverse_obj_map, CategoryTheory.WithInitial.opEquiv_unitIso_hom_app, opEquiv_unitIso_inv_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_map, opEquiv_functor_map
equivComma 📖	CompOp	25 math math: equivComma_functor_obj_left_obj, equivComma_counitIso_hom_app_left_app, equivComma_counitIso_inv_app_left_app, equivComma_inverse_obj_obj, equivComma_counitIso_hom_app_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_map_app, equivComma_functor_obj_left_map, equivComma_functor_obj_right, equivComma_functor_map_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_left_app, equivComma_functor_obj_hom_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_left_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_left_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_hom_app_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_inv_app_app, equivComma_functor_map_left_app, equivComma_inverse_map_app, equivComma_inverse_obj_map, liftFromOver_map_app, equivComma_counitIso_inv_app_right, equivComma_unitIso_hom_app_app, equivComma_unitIso_inv_app_app
homFrom 📖	CompOp	—
id 📖	CompOp	—
incl 📖	CompOp	33 math math: equivComma_functor_obj_left_obj, equivComma_counitIso_hom_app_left_app, equivComma_counitIso_inv_app_left_app, instFaithfulIncl, equivComma_functor_obj_left_map, mkCommaMorphism_left_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_left, inclLift_hom_app, mkCommaObject_left_map, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_left_app, liftToTerminalUnique_inv_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_hom_app_app, lift_map_liftStar, inclLiftToTerminal_inv_app, equivComma_functor_obj_hom_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_left_app, inclLift_inv_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_left, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_left_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_hom_app, mkCommaObject_hom_app, mkCommaObject_left_obj, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_hom_app_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_inv_app_app, inclLiftToTerminal_hom_app, instFullIncl, equivComma_functor_map_left_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_inv_app_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_map, equivComma_unitIso_hom_app_app, liftToTerminalUnique_hom_app, equivComma_unitIso_inv_app_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_obj
inclLift 📖	CompOp	3 math math: inclLift_hom_app, lift_map_liftStar, inclLift_inv_app
inclLiftToTerminal 📖	CompOp	2 math math: inclLiftToTerminal_inv_app, inclLiftToTerminal_hom_app
instCategory 📖	CompOp	115 math math: coneEquiv_unitIso_hom_app_hom_left, mkCommaObject_right, equivComma_functor_obj_left_obj, equivComma_counitIso_hom_app_left_app, CategoryTheory.WithInitial.opEquiv_unitIso_inv_app, equivComma_counitIso_inv_app_left_app, liftStar_inv, instFaithfulIncl, opEquiv_inverse_obj, CategoryTheory.Limits.PreservesLimitsOfShape.ofWidePullbacks, map₂_app, coneEquiv_inverse_obj_π_app_left, mapComp_hom_app, CategoryTheory.WithInitial.opEquiv_functor_map, equivComma_inverse_obj_obj, equivComma_counitIso_hom_app_right, CategoryTheory.WithInitial.opEquiv_counitIso_hom_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_map_app, equivComma_functor_obj_left_map, mkCommaMorphism_left_app, equivComma_functor_obj_right, ofCommaObject_obj, opEquiv_counitIso_inv_app, liftStar_hom, coneEquiv_functor_obj_π_app_star, coneEquiv_counitIso_inv_app_hom, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_left, down_id, opEquiv_unitIso_hom_app, opEquiv_counitIso_hom_app, lift_map, inclLift_hom_app, equivComma_functor_map_right, liftToTerminal_map, CategoryTheory.WithInitial.opEquiv_inverse_obj, coneEquiv_functor_obj_π_app_of, map_map, lift_obj, liftToTerminal_obj, coneEquiv_inverse_obj_pt_left, mkCommaObject_left_map, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_left_app, ofCommaMorphism_app, liftToTerminalUnique_inv_app, mapComp_inv_app, mkCommaMorphism_right, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_hom_app_app, opEquiv_functor_obj, lift_map_liftStar, inclLiftToTerminal_inv_app, equivComma_functor_obj_hom_app, isLimitEquiv_symm_apply_lift, liftFromOver_obj_obj, coneEquiv_inverse_obj_pt_hom, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_right, starIsoTerminal_inv, liftFromOverComp_hom_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_left_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_right, inclLift_inv_app, ofCommaObject_map, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_left, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_left_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_hom_app, starIsoTerminal_hom, CategoryTheory.WithInitial.opEquiv_counitIso_inv_app, prelaxfunctor_toPrelaxFunctorStruct_map₂, widePullbackShapeEquiv_inverse_obj, subsingleton_hom, instHasTerminal, instIsCofilteredOfIsCofilteredOrEmpty, map_obj, mkCommaObject_hom_app, mkCommaObject_left_obj, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_hom_app_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_inv_app_app, mapId_hom_app, inclLiftToTerminal_hom_app, liftFromOver_obj_map, isLimitEquiv_apply_lift_left, pseudofunctor_mapId, pseudofunctor_mapComp, instFullIncl, prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj, coneEquiv_unitIso_inv_app_hom_left, equivComma_functor_map_left_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_inv_app_app, prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, CategoryTheory.WithInitial.opEquiv_functor_obj, down_comp, mapId_inv_app, liftFromOverComp_inv_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_map, equivComma_inverse_map_app, equivComma_inverse_obj_map, liftFromOver_map_app, coneEquiv_inverse_map_hom_left, CategoryTheory.WithInitial.opEquiv_inverse_map, coneEquiv_functor_obj_pt, equivComma_counitIso_inv_app_right, CategoryTheory.WithInitial.opEquiv_unitIso_hom_app, equivComma_unitIso_hom_app_app, opEquiv_unitIso_inv_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_map, liftToTerminalUnique_hom_app, opEquiv_functor_map, equivComma_unitIso_inv_app_app, coneEquiv_counitIso_hom_app_hom, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_obj, widePullbackShapeEquiv_functor_obj, coneEquiv_inverse_obj_pt_right_as, opEquiv_inverse_map, coneEquiv_functor_map_hom, isIso_of_from_star
instUniqueHomStar 📖	CompOp	—
liftStar 📖	CompOp	3 math math: liftStar_inv, liftStar_hom, lift_map_liftStar
liftToTerminal 📖	CompOp	6 math math: liftToTerminal_map, liftToTerminal_obj, liftToTerminalUnique_inv_app, inclLiftToTerminal_inv_app, inclLiftToTerminal_hom_app, liftToTerminalUnique_hom_app
liftToTerminalUnique 📖	CompOp	2 math math: liftToTerminalUnique_inv_app, liftToTerminalUnique_hom_app
liftUnique 📖	CompOp	—
map 📖	CompOp	11 math math: map₂_app, mapComp_hom_app, map_map, mapComp_inv_app, prelaxfunctor_toPrelaxFunctorStruct_map₂, map_obj, mapId_hom_app, pseudofunctor_mapId, pseudofunctor_mapComp, prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, mapId_inv_app
mapComp 📖	CompOp	3 math math: mapComp_hom_app, mapComp_inv_app, pseudofunctor_mapComp
mapId 📖	CompOp	3 math math: mapId_hom_app, pseudofunctor_mapId, mapId_inv_app
map₂ 📖	CompOp	2 math math: map₂_app, prelaxfunctor_toPrelaxFunctorStruct_map₂
mkCommaMorphism 📖	CompOp	8 math math: equivComma_counitIso_hom_app_left_app, equivComma_counitIso_inv_app_left_app, equivComma_counitIso_hom_app_right, mkCommaMorphism_left_app, mkCommaMorphism_right, equivComma_counitIso_inv_app_right, equivComma_unitIso_hom_app_app, equivComma_unitIso_inv_app_app
mkCommaObject 📖	CompOp	14 math math: mkCommaObject_right, equivComma_counitIso_hom_app_left_app, equivComma_counitIso_inv_app_left_app, equivComma_counitIso_hom_app_right, mkCommaMorphism_left_app, equivComma_functor_map_right, mkCommaObject_left_map, mkCommaMorphism_right, mkCommaObject_hom_app, mkCommaObject_left_obj, equivComma_functor_map_left_app, equivComma_counitIso_inv_app_right, equivComma_unitIso_hom_app_app, equivComma_unitIso_inv_app_app
ofCommaMorphism 📖	CompOp	7 math math: equivComma_counitIso_hom_app_left_app, equivComma_counitIso_inv_app_left_app, equivComma_counitIso_hom_app_right, ofCommaMorphism_app, equivComma_counitIso_inv_app_right, equivComma_unitIso_hom_app_app, equivComma_unitIso_inv_app_app
ofCommaObject 📖	CompOp	10 math math: equivComma_counitIso_hom_app_left_app, equivComma_counitIso_inv_app_left_app, equivComma_counitIso_hom_app_right, ofCommaObject_obj, ofCommaMorphism_app, ofCommaObject_map, equivComma_inverse_map_app, equivComma_counitIso_inv_app_right, equivComma_unitIso_hom_app_app, equivComma_unitIso_inv_app_app
opEquiv 📖	CompOp	8 math math: opEquiv_inverse_obj, opEquiv_counitIso_inv_app, opEquiv_unitIso_hom_app, opEquiv_counitIso_hom_app, opEquiv_functor_obj, opEquiv_unitIso_inv_app, opEquiv_functor_map, opEquiv_inverse_map
prelaxfunctor 📖	CompOp	6 math math: prelaxfunctor_toPrelaxFunctorStruct_map₂, pseudofunctor_toPrelaxFunctor, pseudofunctor_mapId, pseudofunctor_mapComp, prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj, prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map
pseudofunctor 📖	CompOp	3 math math: pseudofunctor_toPrelaxFunctor, pseudofunctor_mapId, pseudofunctor_mapComp
starIsoTerminal 📖	CompOp	2 math math: starIsoTerminal_inv, starIsoTerminal_hom
starTerminal 📖	CompOp	16 math math: CategoryTheory.WithInitial.opEquiv_unitIso_inv_app, CategoryTheory.WithInitial.opEquiv_functor_map, CategoryTheory.WithInitial.opEquiv_counitIso_hom_app, opEquiv_counitIso_inv_app, opEquiv_unitIso_hom_app, opEquiv_counitIso_hom_app, lift_map_liftStar, equivComma_functor_obj_hom_app, starIsoTerminal_inv, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_hom_app, CategoryTheory.WithInitial.opEquiv_counitIso_inv_app, mkCommaObject_hom_app, CategoryTheory.WithInitial.opEquiv_unitIso_hom_app, opEquiv_unitIso_inv_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_map, opEquiv_inverse_map
widePullbackShapeEquiv 📖	CompOp	2 math math: widePullbackShapeEquiv_inverse_obj, widePullbackShapeEquiv_functor_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
down_comp 📖	mathematical	—	down CategoryTheory.CategoryStruct.comp CategoryTheory.WithTerminal CategoryTheory.Category.toCategoryStruct instCategory of	—	—
down_id 📖	mathematical	—	down CategoryTheory.CategoryStruct.id CategoryTheory.WithTerminal CategoryTheory.Category.toCategoryStruct instCategory of	—	—
equivComma_counitIso_hom_app_left_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.const CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.comp CategoryTheory.WithTerminal instCategory ofCommaObject ofCommaMorphism mkCommaObject mkCommaMorphism CategoryTheory.CommaMorphism.left CategoryTheory.Iso.hom CategoryTheory.Equivalence.counitIso equivComma CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct incl CategoryTheory.Comma.right	—	—
equivComma_counitIso_hom_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.const CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.comp CategoryTheory.WithTerminal instCategory ofCommaObject ofCommaMorphism mkCommaObject mkCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Equivalence.counitIso equivComma CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	—
equivComma_counitIso_inv_app_left_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.const CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.comp CategoryTheory.WithTerminal instCategory ofCommaObject ofCommaMorphism mkCommaObject mkCommaMorphism CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.Equivalence.counitIso equivComma CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct incl CategoryTheory.Comma.right	—	—
equivComma_counitIso_inv_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.const CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor.comp CategoryTheory.WithTerminal instCategory ofCommaObject ofCommaMorphism mkCommaObject mkCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Equivalence.counitIso equivComma CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	—
equivComma_functor_map_left_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.WithTerminal instCategory incl CategoryTheory.CommaMorphism.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.const mkCommaObject CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor equivComma CategoryTheory.Functor.obj	—	—
equivComma_functor_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.const mkCommaObject CategoryTheory.Functor.map CategoryTheory.WithTerminal instCategory CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor equivComma CategoryTheory.NatTrans.app star	—	—
equivComma_functor_obj_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.WithTerminal instCategory incl CategoryTheory.Functor.const star CategoryTheory.Comma.hom CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor equivComma CategoryTheory.Functor.map CategoryTheory.Limits.IsTerminal.from starTerminal of	—	—
equivComma_functor_obj_left_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.const CategoryTheory.Functor.obj CategoryTheory.WithTerminal instCategory CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor equivComma incl	—	—
equivComma_functor_obj_left_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.const CategoryTheory.WithTerminal instCategory CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor equivComma incl	—	—
equivComma_functor_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.const CategoryTheory.Functor.obj CategoryTheory.WithTerminal instCategory CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor equivComma star	—	—
equivComma_inverse_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithTerminal instCategory ofCommaObject CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.const CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse equivComma Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CommaMorphism.left CategoryTheory.CommaMorphism.right	—	—
equivComma_inverse_obj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.WithTerminal instCategory CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.const CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse equivComma Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Comma.right down CategoryTheory.NatTrans.app CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id	—	—
equivComma_inverse_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.WithTerminal instCategory CategoryTheory.Comma CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.const CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse equivComma CategoryTheory.Comma.left CategoryTheory.Comma.right	—	—
equivComma_unitIso_hom_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithTerminal instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Comma CategoryTheory.Functor.const CategoryTheory.commaCategory mkCommaObject mkCommaMorphism ofCommaObject ofCommaMorphism CategoryTheory.Iso.hom CategoryTheory.Equivalence.unitIso equivComma incl star CategoryTheory.Iso CategoryTheory.Iso.app CategoryTheory.Iso.refl	—	—
equivComma_unitIso_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithTerminal instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Comma CategoryTheory.Functor.id CategoryTheory.Functor.const CategoryTheory.commaCategory mkCommaObject mkCommaMorphism ofCommaObject ofCommaMorphism CategoryTheory.Iso.inv CategoryTheory.Equivalence.unitIso equivComma incl star CategoryTheory.Iso CategoryTheory.Iso.app CategoryTheory.Iso.refl	—	—
false_of_from_star 📖	—	—	—	—	—
false_of_from_star' 📖	—	—	—	—	—
inclLiftToTerminal_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.WithTerminal instCategory incl lift CategoryTheory.Limits.IsTerminal.from CategoryTheory.Functor.obj CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category liftToTerminal inclLiftToTerminal CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
inclLiftToTerminal_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.WithTerminal instCategory incl lift CategoryTheory.Limits.IsTerminal.from CategoryTheory.Functor.obj CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category liftToTerminal inclLiftToTerminal CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
inclLift_hom_app 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.WithTerminal instCategory incl lift CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category inclLift CategoryTheory.CategoryStruct.id	—	—
inclLift_inv_app 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.WithTerminal instCategory incl lift CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category inclLift CategoryTheory.CategoryStruct.id	—	—
instFaithfulIncl 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.WithTerminal instCategory incl	—	—
instFullIncl 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.WithTerminal instCategory incl	—	—
instHasTerminal 📖	mathematical	—	CategoryTheory.Limits.HasTerminal CategoryTheory.WithTerminal instCategory	—	CategoryTheory.Limits.hasTerminal_of_unique Unique.instSubsingleton
isIso_of_from_star 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.WithTerminal instCategory star	—	—
liftStar_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.Iso.hom CategoryTheory.WithTerminal instCategory lift star liftStar CategoryTheory.CategoryStruct.id	—	—
liftStar_inv 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.Iso.inv CategoryTheory.WithTerminal instCategory lift star liftStar CategoryTheory.CategoryStruct.id	—	—
liftToTerminalUnique_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithTerminal instCategory lift CategoryTheory.Limits.IsTerminal.from CategoryTheory.Functor.obj CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category liftToTerminal liftToTerminalUnique CategoryTheory.Iso CategoryTheory.Iso.app CategoryTheory.Functor.comp incl	—	—
liftToTerminalUnique_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithTerminal instCategory lift CategoryTheory.Limits.IsTerminal.from CategoryTheory.Functor.obj CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category liftToTerminal liftToTerminalUnique CategoryTheory.Iso CategoryTheory.Iso.app CategoryTheory.Functor.comp incl	—	—
liftToTerminal_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.WithTerminal instCategory liftToTerminal Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj down CategoryTheory.Limits.IsTerminal.from CategoryTheory.CategoryStruct.id	—	—
liftToTerminal_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.WithTerminal instCategory liftToTerminal	—	—
lift_map 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.WithTerminal instCategory lift Quiver.Hom CategoryTheory.CategoryStruct.toQuiver down CategoryTheory.CategoryStruct.id	—	—
lift_map_liftStar 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.WithTerminal instCategory lift incl star CategoryTheory.Limits.IsTerminal.from starTerminal CategoryTheory.Iso.hom liftStar CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category inclLift	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
lift_obj 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.WithTerminal instCategory lift	—	—
mapComp_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithTerminal instCategory map CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category mapComp of CategoryTheory.Functor.obj star CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
mapComp_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithTerminal instCategory CategoryTheory.Functor.comp map CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category mapComp of CategoryTheory.Functor.obj star CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
mapId_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithTerminal instCategory map CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category mapId of star CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
mapId_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithTerminal instCategory CategoryTheory.Functor.id map CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category mapId of star CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
map_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.WithTerminal instCategory map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct of CategoryTheory.Functor.obj star down	—	—
map_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.WithTerminal instCategory map of star	—	—
map₂_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithTerminal instCategory map map₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.id star	—	—
mkCommaMorphism_left_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.WithTerminal instCategory incl CategoryTheory.CommaMorphism.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.const mkCommaObject mkCommaMorphism CategoryTheory.Functor.obj	—	—
mkCommaMorphism_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.const mkCommaObject mkCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.WithTerminal instCategory star	—	—
mkCommaObject_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.WithTerminal instCategory incl CategoryTheory.Functor.const star CategoryTheory.Comma.hom mkCommaObject CategoryTheory.Functor.map CategoryTheory.Limits.IsTerminal.from starTerminal of	—	—
mkCommaObject_left_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.const mkCommaObject CategoryTheory.WithTerminal instCategory CategoryTheory.Functor.obj incl	—	—
mkCommaObject_left_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.const mkCommaObject CategoryTheory.WithTerminal instCategory incl	—	—
mkCommaObject_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.const mkCommaObject CategoryTheory.Functor.obj CategoryTheory.WithTerminal instCategory star	—	—
ofCommaMorphism_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithTerminal instCategory ofCommaObject ofCommaMorphism Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.const CategoryTheory.Comma.right CategoryTheory.CommaMorphism.left CategoryTheory.CommaMorphism.right	—	—
ofCommaObject_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.WithTerminal instCategory ofCommaObject Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.const CategoryTheory.Comma.right down CategoryTheory.NatTrans.app CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id	—	—
ofCommaObject_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.WithTerminal instCategory ofCommaObject CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.const CategoryTheory.Comma.right	—	—
opEquiv_counitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithInitial Opposite CategoryTheory.WithInitial.instCategory CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.WithTerminal instCategory Opposite.op of Opposite.unop star Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial.down CategoryTheory.WithInitial.of CategoryTheory.WithInitial.star CategoryTheory.Limits.IsTerminal.from starTerminal CategoryTheory.CategoryStruct.id CategoryTheory.CategoryStruct.opposite Quiver.Hom.op down CategoryTheory.Limits.IsInitial.to CategoryTheory.WithInitial.starInitial CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso opEquiv CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
opEquiv_counitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.WithInitial Opposite CategoryTheory.WithInitial.instCategory CategoryTheory.Category.opposite CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.WithTerminal instCategory Opposite.op of Opposite.unop star Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial.down CategoryTheory.WithInitial.of CategoryTheory.WithInitial.star CategoryTheory.Limits.IsTerminal.from starTerminal CategoryTheory.CategoryStruct.id CategoryTheory.CategoryStruct.opposite Quiver.Hom.op down CategoryTheory.Limits.IsInitial.to CategoryTheory.WithInitial.starInitial CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso opEquiv CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
opEquiv_functor_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.WithTerminal CategoryTheory.Category.opposite instCategory CategoryTheory.WithInitial CategoryTheory.WithInitial.instCategory CategoryTheory.Equivalence.functor opEquiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.WithInitial.of Opposite.op CategoryTheory.WithInitial.star Quiver.Hom.op down CategoryTheory.Limits.IsInitial.to CategoryTheory.WithInitial.starInitial CategoryTheory.CategoryStruct.id	—	—
opEquiv_functor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.WithTerminal CategoryTheory.Category.opposite instCategory CategoryTheory.WithInitial CategoryTheory.WithInitial.instCategory CategoryTheory.Equivalence.functor opEquiv Opposite.unop CategoryTheory.WithInitial.of Opposite.op CategoryTheory.WithInitial.star	—	—
opEquiv_inverse_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.WithInitial Opposite CategoryTheory.WithInitial.instCategory CategoryTheory.Category.opposite CategoryTheory.WithTerminal instCategory CategoryTheory.Equivalence.inverse opEquiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.op of Opposite.unop star CategoryTheory.WithInitial.down CategoryTheory.Limits.IsTerminal.from starTerminal CategoryTheory.CategoryStruct.id CategoryTheory.CategoryStruct.opposite	—	—
opEquiv_inverse_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.WithInitial Opposite CategoryTheory.WithInitial.instCategory CategoryTheory.Category.opposite CategoryTheory.WithTerminal instCategory CategoryTheory.Equivalence.inverse opEquiv Opposite.op of Opposite.unop star	—	—
opEquiv_unitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.WithTerminal CategoryTheory.Category.opposite instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.WithInitial CategoryTheory.WithInitial.instCategory CategoryTheory.WithInitial.of Opposite.op CategoryTheory.WithInitial.star Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.op down CategoryTheory.Limits.IsInitial.to CategoryTheory.WithInitial.starInitial of CategoryTheory.CategoryStruct.id star Opposite.unop CategoryTheory.WithInitial.down CategoryTheory.Limits.IsTerminal.from starTerminal CategoryTheory.CategoryStruct.opposite CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso opEquiv CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
opEquiv_unitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.WithTerminal CategoryTheory.Category.opposite instCategory CategoryTheory.Functor.comp CategoryTheory.WithInitial CategoryTheory.WithInitial.instCategory CategoryTheory.WithInitial.of Opposite.op CategoryTheory.WithInitial.star Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.op down CategoryTheory.Limits.IsInitial.to CategoryTheory.WithInitial.starInitial of CategoryTheory.CategoryStruct.id star Opposite.unop CategoryTheory.WithInitial.down CategoryTheory.Limits.IsTerminal.from starTerminal CategoryTheory.CategoryStruct.opposite CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso opEquiv CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
prelaxfunctor_toPrelaxFunctorStruct_map₂ 📖	mathematical	—	CategoryTheory.PrelaxFunctorStruct.map₂ CategoryTheory.Cat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct prelaxfunctor CategoryTheory.NatTrans.toCatHom₂ CategoryTheory.WithTerminal CategoryTheory.Bundled.α CategoryTheory.Category instCategory CategoryTheory.Cat.str map CategoryTheory.Cat.Hom.toFunctor map₂ CategoryTheory.Cat.Hom₂.toNatTrans	—	—
prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map 📖	mathematical	—	Prefunctor.map CategoryTheory.Cat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct prelaxfunctor CategoryTheory.Functor.toCatHom CategoryTheory.WithTerminal CategoryTheory.Bundled.α CategoryTheory.Category instCategory CategoryTheory.Cat.str map CategoryTheory.Cat.Hom.toFunctor	—	—
prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj 📖	mathematical	—	Prefunctor.obj CategoryTheory.Cat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct prelaxfunctor CategoryTheory.Cat.of CategoryTheory.WithTerminal CategoryTheory.Bundled.α CategoryTheory.Category instCategory CategoryTheory.Cat.str	—	—
pseudofunctor_mapComp 📖	mathematical	—	CategoryTheory.Pseudofunctor.mapComp CategoryTheory.Cat CategoryTheory.Cat.bicategory pseudofunctor CategoryTheory.Cat.Hom.isoMk CategoryTheory.WithTerminal CategoryTheory.Bundled.α CategoryTheory.Category instCategory CategoryTheory.Cat.str map CategoryTheory.Cat.Hom.toFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Functor.comp Prefunctor.obj CategoryTheory.CategoryStruct.toQuiver CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct prelaxfunctor Prefunctor.map mapComp	—	—
pseudofunctor_mapId 📖	mathematical	—	CategoryTheory.Pseudofunctor.mapId CategoryTheory.Cat CategoryTheory.Cat.bicategory pseudofunctor CategoryTheory.Cat.Hom.isoMk CategoryTheory.WithTerminal CategoryTheory.Bundled.α CategoryTheory.Category instCategory CategoryTheory.Cat.str map CategoryTheory.Cat.Hom.toFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Functor.id Prefunctor.obj CategoryTheory.CategoryStruct.toQuiver CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct prelaxfunctor mapId	—	—
pseudofunctor_toPrelaxFunctor 📖	mathematical	—	CategoryTheory.Pseudofunctor.toPrelaxFunctor CategoryTheory.Cat CategoryTheory.Cat.bicategory pseudofunctor prelaxfunctor	—	—
starIsoTerminal_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.WithTerminal instCategory star CategoryTheory.Limits.terminal instHasTerminal starIsoTerminal CategoryTheory.Limits.IsTerminal.from CategoryTheory.Limits.terminalIsTerminal	—	instHasTerminal
starIsoTerminal_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.WithTerminal instCategory star CategoryTheory.Limits.terminal instHasTerminal starIsoTerminal CategoryTheory.Limits.IsTerminal.from starTerminal	—	instHasTerminal
subsingleton_hom 📖	mathematical	—	Quiver.IsThin CategoryTheory.WithTerminal CategoryTheory.Discrete CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.discreteCategory	—	—
widePullbackShapeEquiv_functor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.WithTerminal CategoryTheory.Discrete instCategory CategoryTheory.discreteCategory CategoryTheory.Equivalence.functor widePullbackShapeEquiv of star	—	—
widePullbackShapeEquiv_inverse_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.WithTerminal CategoryTheory.Discrete instCategory CategoryTheory.discreteCategory CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Equivalence.inverse widePullbackShapeEquiv DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	—

CategoryTheory.instInhabitedWithInitial

Definitions

Name	Category	Theorems
default 📖	CompOp	—

CategoryTheory.instInhabitedWithTerminal

Definitions

Name	Category	Theorems
default 📖	CompOp	—

---

← Back to Index