Comma

📁 Source: Mathlib/CategoryTheory/MorphismProperty/Comma.lean

Statistics

Metric	Count
Definitions Comma, hom, comp, hom, toCommaMorphism, changeProp, forget, forgetFullyFaithful, fullyFaithfulChangeProp, homFromCommaOfIsIso, id, instCategory, isoFromComma, isoMk, mapLeft, mapLeftComp, mapLeftEq, mapLeftId, mapLeftIso, mapRight, mapRightComp, mapRightEq, mapRightId, mapRightIso, toComma, forget, homMk, mk, toOver, mk, changeProp, forget, homMk, isoMk, mk, Under, mk, forget, homMk, isoMk, mk, commaObj, costructuredArrowObj, over, overObj, structuredArrowObj, under, underObj	48
Theorems comp_left, comp_right, ext, ext', ext'_iff, ext_iff, hom_left, hom_mk, hom_right, prop_hom_left, prop_hom_right, comp_hom, comp_left, comp_left_assoc, comp_right, comp_right_assoc, eqToHom_left, eqToHom_right, ext, ext_iff, forget_map, forget_obj, homFromCommaOfIsIso_hom, hom_homFromCommaOfIsIso, id_hom, id_left, id_right, instFaithfulChangeProp, instFaithfulCommaForget, instFullChangeProp, instFullTopCommaForget, instIsIsoCommaHom, instIsIsoHomFromCommaOfIsIso, instReflectsIsomorphismsCommaForgetOfRespectsIso, inv_hom, isoFromComma_hom, isoFromComma_inv, isoMk_hom_left, isoMk_hom_right, isoMk_inv_left, isoMk_inv_right, lift_map_hom, lift_obj_toComma, mapLeftComp_hom_app_left, mapLeftComp_hom_app_right, mapLeftComp_inv_app_left, mapLeftComp_inv_app_right, mapLeftEq_hom_app_left, mapLeftEq_hom_app_right, mapLeftEq_inv_app_left, mapLeftEq_inv_app_right, mapLeftId_hom_app_left, mapLeftId_hom_app_right, mapLeftId_inv_app_left, mapLeftId_inv_app_right, mapLeftIso_counitIso_hom_app_left, mapLeftIso_counitIso_hom_app_right, mapLeftIso_counitIso_inv_app_left, mapLeftIso_counitIso_inv_app_right, mapLeftIso_functor_map_left, mapLeftIso_functor_map_right, mapLeftIso_functor_obj_hom, mapLeftIso_functor_obj_left, mapLeftIso_functor_obj_right, mapLeftIso_inverse_map_left, mapLeftIso_inverse_map_right, mapLeftIso_inverse_obj_hom, mapLeftIso_inverse_obj_left, mapLeftIso_inverse_obj_right, mapLeftIso_unitIso_hom_app_left, mapLeftIso_unitIso_hom_app_right, mapLeftIso_unitIso_inv_app_left, mapLeftIso_unitIso_inv_app_right, mapLeft_map_left, mapLeft_map_right, mapLeft_obj_hom, mapLeft_obj_left, mapLeft_obj_right, mapRightComp_hom_app_left, mapRightComp_hom_app_right, mapRightComp_inv_app_left, mapRightComp_inv_app_right, mapRightEq_hom_app_left, mapRightEq_hom_app_right, mapRightEq_inv_app_left, mapRightEq_inv_app_right, mapRightId_hom_app_left, mapRightId_hom_app_right, mapRightId_inv_app_left, mapRightId_inv_app_right, mapRightIso_counitIso_hom_app_left, mapRightIso_counitIso_hom_app_right, mapRightIso_counitIso_inv_app_left, mapRightIso_counitIso_inv_app_right, mapRightIso_functor_map_left, mapRightIso_functor_map_right, mapRightIso_functor_obj_hom, mapRightIso_functor_obj_left, mapRightIso_functor_obj_right, mapRightIso_inverse_map_left, mapRightIso_inverse_map_right, mapRightIso_inverse_obj_hom, mapRightIso_inverse_obj_left, mapRightIso_inverse_obj_right, mapRightIso_unitIso_hom_app_left, mapRightIso_unitIso_hom_app_right, mapRightIso_unitIso_inv_app_left, mapRightIso_unitIso_inv_app_right, mapRight_map_left, mapRight_map_right, mapRight_obj_hom, mapRight_obj_left, mapRight_obj_right, prop, toCommaMorphism_eq_hom, ext, ext_iff, homMk_left, mk_hom, mk_left, toOver_map, toOver_obj, over, ext, ext_iff, mk_hom, changeProp_obj_hom, changeProp_obj_left, forget_comp_forget_map, homMk_hom, isoMk_hom_left, isoMk_inv_left, mk_hom, mk_left, w, w_assoc, ext, ext_iff, mk_hom, forget_comp_forget_map, homMk_hom, isoMk_hom_right, isoMk_inv_right, mk_hom, mk_left, w, w_assoc, commaObj_iff, costructuredArrowObj_iff, costructuredArrow_iso_iff, instFaithfulCostructuredArrowTopOverToOver, instFaithfulOverTopOverForget, instFaithfulUnderTopUnderForget, instFullCostructuredArrowTopOverToOver, instFullOverTopOverForget, instFullUnderTopUnderForget, instIsClosedUnderIsomorphismsCommaCommaObjOfRespectsIso, instIsClosedUnderIsomorphismsCostructuredArrowCostructuredArrowObjOfRespectsIso, instIsClosedUnderIsomorphismsOverOverObjOfRespectsIso, instIsClosedUnderIsomorphismsStructuredArrowStructuredArrowObjOfRespectsIso, instIsClosedUnderIsomorphismsUnderUnderObjOfRespectsIso, overObj_iff, over_eq_inverseImage, over_iff, over_iso_iff, structuredArrowObj_iff, underObj_iff, under_eq_inverseImage, under_iff	169
Total	217

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
Comma 📖	CompData	99 math math: Comma.mapRightIso_functor_map_right, Comma.mapRightComp_hom_app_left, Comma.mapRightIso_counitIso_inv_app_left, Comma.mapRightIso_unitIso_inv_app_right, Comma.mapRightIso_functor_obj_right, Comma.instFaithfulChangeProp, Comma.mapLeftIso_inverse_obj_left, Comma.eqToHom_left, Comma.mapLeftEq_inv_app_right, Comma.comp_right, Comma.mapRightIso_counitIso_hom_app_right, Comma.instFullChangeProp, Comma.mapLeftEq_inv_app_left, Comma.mapRightIso_counitIso_inv_app_right, Comma.isoMk_hom_left, Comma.mapRightIso_functor_map_left, Comma.comp_left_assoc, Comma.mapLeftIso_unitIso_inv_app_right, Comma.mapRightId_inv_app_right, Comma.mapLeft_obj_hom, Comma.instFullTopCommaForget, Comma.isoFromComma_hom, Comma.mapLeftIso_counitIso_hom_app_right, Comma.mapLeftComp_hom_app_left, Comma.mapLeftIso_functor_map_left, Comma.mapRightEq_hom_app_left, Comma.mapLeftComp_inv_app_left, Comma.isoMk_hom_right, Comma.mapLeftIso_inverse_obj_hom, Comma.mapLeftIso_inverse_obj_right, Comma.mapLeftIso_functor_map_right, Comma.isoMk_inv_left, Comma.mapRight_obj_left, Comma.mapLeftIso_inverse_map_left, Comma.lift_obj_toComma, Comma.comp_right_assoc, Comma.mapRightComp_hom_app_right, Comma.mapRightEq_inv_app_right, Comma.mapLeft_map_right, Comma.mapRightId_inv_app_left, Comma.mapRightIso_unitIso_inv_app_left, Comma.mapLeft_obj_left, Comma.mapRightId_hom_app_right, Comma.mapRightIso_counitIso_hom_app_left, Comma.forget_obj, Comma.mapRightIso_inverse_obj_hom, Comma.mapLeftId_inv_app_right, Comma.mapRight_obj_right, Comma.mapRightIso_inverse_map_left, Comma.mapRight_map_right, Comma.forget_map, Comma.mapLeftIso_functor_obj_left, Comma.mapRightComp_inv_app_left, Comma.comp_left, Comma.id_hom, Comma.isoFromComma_inv, Comma.isoMk_inv_right, Comma.mapLeftIso_counitIso_inv_app_right, Comma.mapRight_map_left, Comma.hasColimitsOfShape_of_closedUnderColimitsOfShape, Comma.mapRightIso_inverse_map_right, Comma.instFaithfulCommaForget, Comma.mapRight_obj_hom, Comma.mapRightIso_unitIso_hom_app_left, Comma.mapLeftIso_functor_obj_right, Comma.mapRightIso_unitIso_hom_app_right, Comma.mapLeftId_hom_app_left, Comma.mapLeftId_hom_app_right, Comma.hasColimit_of_closedUnderColimitsOfShape, Comma.mapLeftIso_unitIso_inv_app_left, Comma.mapLeftIso_functor_obj_hom, Comma.mapLeft_obj_right, Comma.mapLeftIso_counitIso_hom_app_left, Comma.mapRightId_hom_app_left, Comma.mapRightIso_functor_obj_left, Comma.inv_hom, Comma.instReflectsIsomorphismsCommaForgetOfRespectsIso, Comma.instIsIsoHomFromCommaOfIsIso, Comma.mapLeftId_inv_app_left, Comma.mapLeftIso_counitIso_inv_app_left, Comma.eqToHom_right, Comma.comp_hom, Comma.mapLeftIso_inverse_map_right, Comma.lift_map_hom, Comma.mapRightIso_inverse_obj_left, Comma.mapLeftEq_hom_app_right, Comma.mapLeftComp_hom_app_right, Comma.mapLeft_map_left, Comma.mapLeftEq_hom_app_left, Comma.mapRightIso_inverse_obj_right, Comma.mapRightIso_functor_obj_hom, Comma.hasLimitsOfShape_of_closedUnderLimitsOfShape, Comma.mapRightComp_inv_app_right, Comma.mapLeftComp_inv_app_right, Comma.mapLeftIso_unitIso_hom_app_left, Comma.mapRightEq_inv_app_left, Comma.hasLimit_of_closedUnderLimitsOfShape, Comma.mapRightEq_hom_app_right, Comma.mapLeftIso_unitIso_hom_app_right
Under 📖	CompOp	10 math math: underEquivOfIsTerminal_inverse, underEquivOfIsTerminal_counitIso, Under.isoMk_inv_right, Under.isoMk_hom_right, instFullUnderTopUnderForget, underEquivOfIsTerminal_unitIso, underEquivOfIsTerminal_functor, Under.forget_comp_forget_map, essentiallySmall_of_le, instFaithfulUnderTopUnderForget
commaObj 📖	CompOp	2 math math: commaObj_iff, instIsClosedUnderIsomorphismsCommaCommaObjOfRespectsIso
costructuredArrowObj 📖	CompOp	4 math math: CategoryTheory.CostructuredArrow.closedUnderLimitsOfShape_discrete_empty, instIsClosedUnderIsomorphismsCostructuredArrowCostructuredArrowObjOfRespectsIso, CategoryTheory.CostructuredArrow.isClosedUnderColimitsOfShape, costructuredArrowObj_iff
over 📖	CompOp	8 math math: over_eq_inverseImage, HasFactorization.over, HomotopicalAlgebra.trivialFibrations_over_eq, HomotopicalAlgebra.trivialCofibrations_over_eq, HomotopicalAlgebra.fibrations_over_def, HomotopicalAlgebra.cofibrations_over_def, over_iff, HomotopicalAlgebra.weakEquivalences_over_def
overObj 📖	CompOp	4 math math: instIsClosedUnderIsomorphismsOverOverObjOfRespectsIso, overObj_iff, CategoryTheory.Over.closedUnderLimitsOfShape_pullback, CategoryTheory.Over.closedUnderLimitsOfShape_discrete_empty
structuredArrowObj 📖	CompOp	2 math math: instIsClosedUnderIsomorphismsStructuredArrowStructuredArrowObjOfRespectsIso, structuredArrowObj_iff
under 📖	CompOp	2 math math: under_iff, under_eq_inverseImage
underObj 📖	CompOp	5 math math: instIsClosedUnderIsomorphismsUnderUnderObjOfRespectsIso, ind_iff_ind_underMk, ind_underObj_pushout, underObj_ind_eq_ind_underObj, underObj_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commaObj_iff 📖	mathematical	—	commaObj CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
costructuredArrowObj_iff 📖	mathematical	—	costructuredArrowObj CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
costructuredArrow_iso_iff 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	comma_iso_iff
instFaithfulCostructuredArrowTopOverToOver 📖	mathematical	—	CategoryTheory.Functor.Faithful CostructuredArrow Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit IsMultiplicative.instTop Over CategoryTheory.Functor.id CostructuredArrow.toOver	—	IsMultiplicative.instTop CostructuredArrow.Hom.ext CategoryTheory.Functor.map_injective
instFaithfulOverTopOverForget 📖	mathematical	—	CategoryTheory.Functor.Faithful Over Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit IsMultiplicative.instTop CategoryTheory.Over CategoryTheory.instCategoryOver Over.forget	—	—
instFaithfulUnderTopUnderForget 📖	mathematical	—	CategoryTheory.Functor.Faithful Under Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id IsMultiplicative.instTop CategoryTheory.Under CategoryTheory.instCategoryUnder Under.forget	—	—
instFullCostructuredArrowTopOverToOver 📖	mathematical	—	CategoryTheory.Functor.Full CostructuredArrow Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit IsMultiplicative.instTop Over CategoryTheory.Functor.id CostructuredArrow.toOver	—	IsMultiplicative.instTop CategoryTheory.Functor.map_preimage CategoryTheory.Category.comp_id CategoryTheory.CommaMorphism.w Over.Hom.ext Over.homMk.congr_simp
instFullOverTopOverForget 📖	mathematical	—	CategoryTheory.Functor.Full Over Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit IsMultiplicative.instTop CategoryTheory.Over CategoryTheory.instCategoryOver Over.forget	—	—
instFullUnderTopUnderForget 📖	mathematical	—	CategoryTheory.Functor.Full Under Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id IsMultiplicative.instTop CategoryTheory.Under CategoryTheory.instCategoryUnder Under.forget	—	—
instIsClosedUnderIsomorphismsCommaCommaObjOfRespectsIso 📖	mathematical	—	CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms CategoryTheory.Comma CategoryTheory.commaCategory commaObj	—	commaObj_iff cancel_left_of_respectsIso CategoryTheory.Functor.map_isIso CategoryTheory.Comma.instIsIsoLeft CategoryTheory.Iso.isIso_hom CategoryTheory.CommaMorphism.w cancel_right_of_respectsIso CategoryTheory.Comma.instIsIsoRight
instIsClosedUnderIsomorphismsCostructuredArrowCostructuredArrowObjOfRespectsIso 📖	mathematical	—	CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow costructuredArrowObj	—	—
instIsClosedUnderIsomorphismsOverOverObjOfRespectsIso 📖	mathematical	—	CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms CategoryTheory.Over CategoryTheory.instCategoryOver overObj	—	—
instIsClosedUnderIsomorphismsStructuredArrowStructuredArrowObjOfRespectsIso 📖	mathematical	—	CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow structuredArrowObj	—	—
instIsClosedUnderIsomorphismsUnderUnderObjOfRespectsIso 📖	mathematical	—	CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms CategoryTheory.Under CategoryTheory.instCategoryUnder underObj	—	—
overObj_iff 📖	mathematical	—	overObj CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
over_eq_inverseImage 📖	mathematical	—	over inverseImage CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.forget	—	—
over_iff 📖	mathematical	—	over CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.CommaMorphism.left	—	—
over_iso_iff 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	comma_iso_iff
structuredArrowObj_iff 📖	mathematical	—	structuredArrowObj CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
underObj_iff 📖	mathematical	—	underObj CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
under_eq_inverseImage 📖	mathematical	—	under inverseImage CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Under.forget	—	—
under_iff 📖	mathematical	—	under CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.CommaMorphism.right	—	—

CategoryTheory.MorphismProperty.Comma

Definitions

Name	Category	Theorems
changeProp 📖	CompOp	2 math math: instFaithfulChangeProp, instFullChangeProp
forget 📖	CompOp	5 math math: instFullTopCommaForget, forget_obj, forget_map, instFaithfulCommaForget, instReflectsIsomorphismsCommaForgetOfRespectsIso
forgetFullyFaithful 📖	CompOp	—
fullyFaithfulChangeProp 📖	CompOp	—
homFromCommaOfIsIso 📖	CompOp	5 math math: isoFromComma_hom, homFromCommaOfIsIso_hom, hom_homFromCommaOfIsIso, isoFromComma_inv, instIsIsoHomFromCommaOfIsIso
id 📖	CompOp	2 math math: id_left, id_right
instCategory 📖	CompOp	192 math math: CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_inducedTopology, mapRightIso_functor_map_right, mapRightComp_hom_app_left, CategoryTheory.MorphismProperty.underEquivOfIsTerminal_inverse, mapRightIso_counitIso_inv_app_left, mapRightIso_unitIso_inv_app_right, mapRightIso_functor_obj_right, CategoryTheory.MorphismProperty.Over.hasPullbacks, CategoryTheory.MorphismProperty.overEquivOfIsInitial_counitIso, instFaithfulChangeProp, mapLeftIso_inverse_obj_left, CategoryTheory.MorphismProperty.Over.instHasTerminalTopOfContainsIdentities, eqToHom_left, mapLeftEq_inv_app_right, AlgebraicGeometry.instHasColimitOverSchemeTopMorphismProperty, CategoryTheory.MorphismProperty.Over.map_obj_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd_assoc, CategoryTheory.MorphismProperty.Over.pullbackComp_hom_app_left, AlgebraicGeometry.Scheme.locallyCoverDense_of_le, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.isPullback, comp_right, AlgebraicGeometry.instIsOpenImmersionLeftSchemeDiscretePUnitMapWalkingSpanOverTopMorphismPropertySpan, mapRightIso_counitIso_hom_app_right, CategoryTheory.MorphismProperty.Over.mapCongr_inv_app_left, instFullChangeProp, CategoryTheory.MorphismProperty.Over.pullbackMapHomPullback_app, mapLeftEq_inv_app_left, mapRightIso_counitIso_inv_app_right, CategoryTheory.MorphismProperty.Over.pullback_obj_left, CategoryTheory.MorphismProperty.Over.map_map_left, isoMk_hom_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap, mapRightIso_functor_map_left, comp_left_assoc, CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst, mapLeftIso_unitIso_inv_app_right, CategoryTheory.MorphismProperty.Over.mapPullbackAdj_counit_app, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst_assoc, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_f, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_pt, CategoryTheory.MorphismProperty.instFaithfulOverTopOverForget, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_id, mapRightId_inv_app_right, CategoryTheory.MorphismProperty.Over.map_comp, mapLeft_obj_hom, instFullTopCommaForget, isoFromComma_hom, CategoryTheory.MorphismProperty.Over.instPreservesFiniteLimitsTopPullback, mapLeftIso_counitIso_hom_app_right, CategoryTheory.MorphismProperty.Over.isoMk_inv_left, mapLeftComp_hom_app_left, mapLeftIso_functor_map_left, CategoryTheory.MorphismProperty.underEquivOfIsTerminal_counitIso, CategoryTheory.MorphismProperty.Over.mapPullbackAdj_unit_app, mapRightEq_hom_app_left, mapLeftComp_inv_app_left, CategoryTheory.MorphismProperty.Under.isoMk_inv_right, CategoryTheory.MorphismProperty.Over.changeProp_obj_left, CategoryTheory.MorphismProperty.Over.mapId_inv_app_left, isoMk_hom_right, mapLeftIso_inverse_obj_hom, CategoryTheory.MorphismProperty.Under.isoMk_hom_right, mapLeftIso_inverse_obj_right, CategoryTheory.MorphismProperty.Over.mapCongr_hom_app_left, mapLeftIso_functor_map_right, isoMk_inv_left, mapRight_obj_left, mapLeftIso_inverse_map_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι, CategoryTheory.MorphismProperty.Over.forget_comp_forget_map, CategoryTheory.MorphismProperty.Over.changeProp_obj_hom, CategoryTheory.MorphismProperty.Over.pullbackComp_inv_app_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_ι_app, lift_obj_toComma, comp_right_assoc, mapRightComp_hom_app_right, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_X, mapRightEq_inv_app_right, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_f, mapLeft_map_right, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι_assoc, mapRightId_inv_app_left, AlgebraicGeometry.Scheme.smallGrothendieckTopologyOfLE_eq_toGrothendieck_smallPretopology, CategoryTheory.MorphismProperty.instFullUnderTopUnderForget, mapRightIso_unitIso_inv_app_left, CategoryTheory.MorphismProperty.instIsLeftAdjointOverTopMapOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong, mapLeft_obj_left, mapRightId_hom_app_right, CategoryTheory.MorphismProperty.Over.mapComp_hom_app_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap_assoc, CategoryTheory.MorphismProperty.Over.instHasFiniteLimitsTopOfHasFiniteWidePullbacks, mapRightIso_counitIso_hom_app_left, CategoryTheory.MorphismProperty.overEquivOfIsInitial_inverse, forget_obj, mapRightIso_inverse_obj_hom, CategoryTheory.MorphismProperty.instFaithfulCostructuredArrowTopOverToOver, AlgebraicGeometry.instIsOpenImmersionMapSchemeCompOverOverTopMorphismPropertyForgetForget, CategoryTheory.MorphismProperty.underEquivOfIsTerminal_unitIso, CategoryTheory.MorphismProperty.CostructuredArrow.toOver_map, AlgebraicGeometry.instHasCoproductsOfShapeOverSchemeTopMorphismPropertyOfSmall, mapLeftId_inv_app_right, mapRight_obj_right, AlgebraicGeometry.instIsOpenImmersionLeftSchemeDiscretePUnitιOverTopMorphismProperty, CategoryTheory.MorphismProperty.CostructuredArrow.toOver_obj, mapRightIso_inverse_map_left, mapRight_map_right, forget_map, mapLeftIso_functor_obj_left, mapRightComp_inv_app_left, CategoryTheory.MorphismProperty.underEquivOfIsTerminal_functor, comp_left, id_hom, isoFromComma_inv, isoMk_inv_right, AlgebraicGeometry.Scheme.Cover.hasColimit_of_locallyDirected, mapLeftIso_counitIso_inv_app_right, CategoryTheory.MorphismProperty.Over.instPreservesFiniteLimitsTopOverForget, mapRight_map_left, CategoryTheory.MorphismProperty.Under.forget_comp_forget_map, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_X, CategoryTheory.MorphismProperty.instFullOverTopOverForget, CategoryTheory.MorphismProperty.exists_map_eq_of_presieve, hasColimitsOfShape_of_closedUnderColimitsOfShape, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.trans_app_left, AlgebraicGeometry.Scheme.instLocallyCoverDenseOverTopMorphismPropertyOverForgetOverGrothendieckTopology, CategoryTheory.MorphismProperty.locallyCoverDense_forget_of_le, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_comp, mapRightIso_inverse_map_right, instFaithfulCommaForget, mapRight_obj_hom, mapRightIso_unitIso_hom_app_left, mapLeftIso_functor_obj_right, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.gluedCocone_pt, mapRightIso_unitIso_hom_app_right, mapLeftId_hom_app_left, mapLeftId_hom_app_right, hasColimit_of_closedUnderColimitsOfShape, AlgebraicGeometry.Scheme.smallGrothendieckTopology_eq_toGrothendieck_smallPretopology, CategoryTheory.MorphismProperty.Over.pullback_map_left, mapLeftIso_unitIso_inv_app_left, mapLeftIso_functor_obj_hom, mapLeft_obj_right, AlgebraicGeometry.instIsLocallyDirectedCompSchemeOverOverTopMorphismPropertyForgetForgetForget, mapLeftIso_counitIso_hom_app_left, mapRightId_hom_app_left, mapRightIso_functor_obj_left, inv_hom, instReflectsIsomorphismsCommaForgetOfRespectsIso, CategoryTheory.MorphismProperty.Over.pullback_obj_hom, CategoryTheory.MorphismProperty.Over.mapComp_inv_app_left, instIsIsoHomFromCommaOfIsIso, CategoryTheory.MorphismProperty.instFullCostructuredArrowTopOverToOver, mapLeftId_inv_app_left, AlgebraicGeometry.Scheme.mem_smallGrothendieckTopology, mapLeftIso_counitIso_inv_app_left, CategoryTheory.MorphismProperty.overEquivOfIsInitial_functor, CategoryTheory.MorphismProperty.Over.isoMk_hom_left, eqToHom_right, comp_hom, mapLeftIso_inverse_map_right, lift_map_hom, CategoryTheory.MorphismProperty.overEquivOfIsInitial_unitIso, essentiallySmall_of_le, AlgebraicGeometry.instPreservesColimitOverSchemeTopMorphismPropertyOverForget, mapRightIso_inverse_obj_left, AlgebraicGeometry.instMonoObjWalkingSpanCompOverSchemeTopMorphismPropertySpanOverForgetForgetForgetNoneWalkingPairSomeMapInitOfIsOpenImmersionLeftDiscretePUnit, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_map, mapLeftEq_hom_app_right, mapLeftComp_hom_app_right, mapLeft_map_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_obj, mapLeftEq_hom_app_left, mapRightIso_inverse_obj_right, mapRightIso_functor_obj_hom, AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology, CategoryTheory.MorphismProperty.Over.mapId_hom_app_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.relativeGluingData_natTrans_app, CategoryTheory.MorphismProperty.Over.pullbackComp_left_fst_fst, hasLimitsOfShape_of_closedUnderLimitsOfShape, mapRightComp_inv_app_right, mapLeftComp_inv_app_right, AlgebraicGeometry.instHasFiniteCoproductsOverSchemeTopMorphismProperty, mapLeftIso_unitIso_hom_app_left, CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst_assoc, mapRightEq_inv_app_left, hasLimit_of_closedUnderLimitsOfShape, CategoryTheory.MorphismProperty.Over.map_obj_hom, mapRightEq_hom_app_right, CategoryTheory.MorphismProperty.instFaithfulUnderTopUnderForget, mapLeftIso_unitIso_hom_app_right
isoFromComma 📖	CompOp	2 math math: isoFromComma_hom, isoFromComma_inv
isoMk 📖	CompOp	4 math math: isoMk_hom_left, isoMk_hom_right, isoMk_inv_left, isoMk_inv_right
mapLeft 📖	CompOp	25 math math: mapLeftEq_inv_app_right, mapLeftEq_inv_app_left, mapLeftIso_unitIso_inv_app_right, mapLeft_obj_hom, mapLeftIso_counitIso_hom_app_right, mapLeftComp_hom_app_left, mapLeftComp_inv_app_left, mapLeft_map_right, mapLeft_obj_left, mapLeftId_inv_app_right, mapLeftIso_counitIso_inv_app_right, mapLeftId_hom_app_left, mapLeftId_hom_app_right, mapLeftIso_unitIso_inv_app_left, mapLeft_obj_right, mapLeftIso_counitIso_hom_app_left, mapLeftId_inv_app_left, mapLeftIso_counitIso_inv_app_left, mapLeftEq_hom_app_right, mapLeftComp_hom_app_right, mapLeft_map_left, mapLeftEq_hom_app_left, mapLeftComp_inv_app_right, mapLeftIso_unitIso_hom_app_left, mapLeftIso_unitIso_hom_app_right
mapLeftComp 📖	CompOp	4 math math: mapLeftComp_hom_app_left, mapLeftComp_inv_app_left, mapLeftComp_hom_app_right, mapLeftComp_inv_app_right
mapLeftEq 📖	CompOp	4 math math: mapLeftEq_inv_app_right, mapLeftEq_inv_app_left, mapLeftEq_hom_app_right, mapLeftEq_hom_app_left
mapLeftId 📖	CompOp	4 math math: mapLeftId_inv_app_right, mapLeftId_hom_app_left, mapLeftId_hom_app_right, mapLeftId_inv_app_left
mapLeftIso 📖	CompOp	18 math math: mapLeftIso_inverse_obj_left, mapLeftIso_unitIso_inv_app_right, mapLeftIso_counitIso_hom_app_right, mapLeftIso_functor_map_left, mapLeftIso_inverse_obj_hom, mapLeftIso_inverse_obj_right, mapLeftIso_functor_map_right, mapLeftIso_inverse_map_left, mapLeftIso_functor_obj_left, mapLeftIso_counitIso_inv_app_right, mapLeftIso_functor_obj_right, mapLeftIso_unitIso_inv_app_left, mapLeftIso_functor_obj_hom, mapLeftIso_counitIso_hom_app_left, mapLeftIso_counitIso_inv_app_left, mapLeftIso_inverse_map_right, mapLeftIso_unitIso_hom_app_left, mapLeftIso_unitIso_hom_app_right
mapRight 📖	CompOp	25 math math: mapRightComp_hom_app_left, mapRightIso_counitIso_inv_app_left, mapRightIso_unitIso_inv_app_right, mapRightIso_counitIso_hom_app_right, mapRightIso_counitIso_inv_app_right, mapRightId_inv_app_right, mapRightEq_hom_app_left, mapRight_obj_left, mapRightComp_hom_app_right, mapRightEq_inv_app_right, mapRightId_inv_app_left, mapRightIso_unitIso_inv_app_left, mapRightId_hom_app_right, mapRightIso_counitIso_hom_app_left, mapRight_obj_right, mapRight_map_right, mapRightComp_inv_app_left, mapRight_map_left, mapRight_obj_hom, mapRightIso_unitIso_hom_app_left, mapRightIso_unitIso_hom_app_right, mapRightId_hom_app_left, mapRightComp_inv_app_right, mapRightEq_inv_app_left, mapRightEq_hom_app_right
mapRightComp 📖	CompOp	4 math math: mapRightComp_hom_app_left, mapRightComp_hom_app_right, mapRightComp_inv_app_left, mapRightComp_inv_app_right
mapRightEq 📖	CompOp	4 math math: mapRightEq_hom_app_left, mapRightEq_inv_app_right, mapRightEq_inv_app_left, mapRightEq_hom_app_right
mapRightId 📖	CompOp	4 math math: mapRightId_inv_app_right, mapRightId_inv_app_left, mapRightId_hom_app_right, mapRightId_hom_app_left
mapRightIso 📖	CompOp	18 math math: mapRightIso_functor_map_right, mapRightIso_counitIso_inv_app_left, mapRightIso_unitIso_inv_app_right, mapRightIso_functor_obj_right, mapRightIso_counitIso_hom_app_right, mapRightIso_counitIso_inv_app_right, mapRightIso_functor_map_left, mapRightIso_unitIso_inv_app_left, mapRightIso_counitIso_hom_app_left, mapRightIso_inverse_obj_hom, mapRightIso_inverse_map_left, mapRightIso_inverse_map_right, mapRightIso_unitIso_hom_app_left, mapRightIso_unitIso_hom_app_right, mapRightIso_functor_obj_left, mapRightIso_inverse_obj_left, mapRightIso_inverse_obj_right, mapRightIso_functor_obj_hom
toComma 📖	CompOp	173 math math: mapRightIso_functor_map_right, mapRightComp_hom_app_left, mapRightIso_counitIso_inv_app_left, Hom.ext_iff, mapRightIso_unitIso_inv_app_right, mapRightIso_functor_obj_right, mapLeftIso_inverse_obj_left, eqToHom_left, mapLeftEq_inv_app_right, CategoryTheory.MorphismProperty.Over.map_obj_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd_assoc, CategoryTheory.MorphismProperty.Over.pullbackComp_hom_app_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.isPullback, CategoryTheory.MorphismProperty.Under.mk_hom, comp_right, AlgebraicGeometry.instIsOpenImmersionLeftSchemeDiscretePUnitMapWalkingSpanOverTopMorphismPropertySpan, CategoryTheory.MorphismProperty.CostructuredArrow.homMk_left, mapRightIso_counitIso_hom_app_right, CategoryTheory.MorphismProperty.Over.mapCongr_inv_app_left, CategoryTheory.MorphismProperty.Over.pullbackMapHomPullback_app, mapLeftEq_inv_app_left, mapRightIso_counitIso_inv_app_right, CategoryTheory.MorphismProperty.Over.mk_hom, CategoryTheory.MorphismProperty.Over.pullback_obj_left, CategoryTheory.MorphismProperty.Over.map_map_left, isoMk_hom_left, mapRightIso_functor_map_left, CategoryTheory.MorphismProperty.Over.Hom.ext_iff, comp_left_assoc, CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst, mapLeftIso_unitIso_inv_app_right, CategoryTheory.MorphismProperty.Over.mapPullbackAdj_counit_app, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst_assoc, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_f, AlgebraicGeometry.Scheme.ProEt.forget_obj, mapRightId_inv_app_right, mapLeft_obj_hom, isoFromComma_hom, mapLeftIso_counitIso_hom_app_right, CategoryTheory.MorphismProperty.Over.isoMk_inv_left, mapLeftComp_hom_app_left, mapLeftIso_functor_map_left, CategoryTheory.MorphismProperty.Over.mapPullbackAdj_unit_app, mapRightEq_hom_app_left, mapLeftComp_inv_app_left, CategoryTheory.MorphismProperty.Under.isoMk_inv_right, CategoryTheory.MorphismProperty.Over.changeProp_obj_left, CategoryTheory.MorphismProperty.Over.mapId_inv_app_left, isoMk_hom_right, mapLeftIso_inverse_obj_hom, CategoryTheory.MorphismProperty.Under.isoMk_hom_right, mapLeftIso_inverse_obj_right, CategoryTheory.MorphismProperty.Over.mapCongr_hom_app_left, mapLeftIso_functor_map_right, isoMk_inv_left, mapRight_obj_left, mapLeftIso_inverse_map_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι, CategoryTheory.MorphismProperty.Over.forget_comp_forget_map, CategoryTheory.MorphismProperty.Over.changeProp_obj_hom, CategoryTheory.MorphismProperty.Over.pullbackComp_inv_app_left, Hom.prop_hom_left, CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong, lift_obj_toComma, comp_right_assoc, mapRightComp_hom_app_right, CategoryTheory.MorphismProperty.Under.homMk_hom, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_X, mapRightEq_inv_app_right, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_f, mapLeft_map_right, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι_assoc, mapRightId_inv_app_left, Hom.hom_right, ext_iff, AlgebraicGeometry.Scheme.ProEt.mk_hom, mapRightIso_unitIso_inv_app_left, mapLeft_obj_left, mapRightId_hom_app_right, CategoryTheory.MorphismProperty.Over.mapComp_hom_app_left, mapRightIso_counitIso_hom_app_left, CategoryTheory.MorphismProperty.Over.w_assoc, forget_obj, mapRightIso_inverse_obj_hom, CategoryTheory.MorphismProperty.underEquivOfIsTerminal_unitIso, CategoryTheory.MorphismProperty.CostructuredArrow.toOver_map, mapLeftId_inv_app_right, mapRight_obj_right, AlgebraicGeometry.instIsOpenImmersionLeftSchemeDiscretePUnitιOverTopMorphismProperty, Hom.comp_left, CategoryTheory.MorphismProperty.CostructuredArrow.toOver_obj, CategoryTheory.MorphismProperty.Under.w, prop, mapRightIso_inverse_map_left, mapRight_map_right, CategoryTheory.MorphismProperty.Over.mk_left, CategoryTheory.MorphismProperty.CostructuredArrow.mk_left, mapLeftIso_functor_obj_left, mapRightComp_inv_app_left, AlgebraicGeometry.Scheme.ProEt.instWeaklyEtaleHomDiscretePUnit, CategoryTheory.MorphismProperty.Under.Hom.ext_iff, CategoryTheory.MorphismProperty.Over.homMk_hom, comp_left, id_hom, isoFromComma_inv, CategoryTheory.MorphismProperty.Under.mk_left, isoMk_inv_right, mapLeftIso_counitIso_inv_app_right, instIsIsoCommaHom, mapRight_map_left, CategoryTheory.MorphismProperty.Under.forget_comp_forget_map, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_X, CategoryTheory.MorphismProperty.Over.w, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.trans_app_left, mapRightIso_inverse_map_right, mapRight_obj_hom, mapRightIso_unitIso_hom_app_left, mapLeftIso_functor_obj_right, mapRightIso_unitIso_hom_app_right, mapLeftId_hom_app_left, mapLeftId_hom_app_right, CategoryTheory.MorphismProperty.CostructuredArrow.Hom.ext_iff, CategoryTheory.MorphismProperty.Over.pullback_map_left, mapLeftIso_unitIso_inv_app_left, mapLeftIso_functor_obj_hom, mapLeft_obj_right, mapLeftIso_counitIso_hom_app_left, mapRightId_hom_app_left, mapRightIso_functor_obj_left, inv_hom, Hom.hom_left, CategoryTheory.MorphismProperty.Over.pullback_obj_hom, CategoryTheory.MorphismProperty.Over.mapComp_inv_app_left, CategoryTheory.MorphismProperty.Under.w_assoc, mapLeftId_inv_app_left, AlgebraicGeometry.Scheme.mem_smallGrothendieckTopology, CategoryTheory.MorphismProperty.instHasPullbackSndHomDiscretePUnitOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong, mapLeftIso_counitIso_inv_app_left, CategoryTheory.MorphismProperty.Over.isoMk_hom_left, eqToHom_right, comp_hom, mapLeftIso_inverse_map_right, Hom.prop_hom_right, CategoryTheory.MorphismProperty.overEquivOfIsInitial_unitIso, mapRightIso_inverse_obj_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_map, mapLeftEq_hom_app_right, mapLeftComp_hom_app_right, mapLeft_map_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst, AlgebraicGeometry.Scheme.ProEt.mk_right_as, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_obj, mapLeftEq_hom_app_left, mapRightIso_inverse_obj_right, mapRightIso_functor_obj_hom, AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology, CategoryTheory.MorphismProperty.Over.mapId_hom_app_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.relativeGluingData_natTrans_app, CategoryTheory.MorphismProperty.Over.pullbackComp_left_fst_fst, mapRightComp_inv_app_right, mapLeftComp_inv_app_right, Hom.comp_right, id_left, mapLeftIso_unitIso_hom_app_left, CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst_assoc, CategoryTheory.MorphismProperty.CostructuredArrow.mk_hom, mapRightEq_inv_app_left, AlgebraicGeometry.Scheme.ProEt.mk_left, CategoryTheory.MorphismProperty.Over.map_obj_hom, mapRightEq_hom_app_right, mapLeftIso_unitIso_hom_app_right, id_right

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_hom 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp CategoryTheory.MorphismProperty.Comma CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Comma CategoryTheory.commaCategory toComma	—	—
comp_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left toComma Hom.toCommaMorphism CategoryTheory.CategoryStruct.comp CategoryTheory.MorphismProperty.Comma CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Comma.left	—	—
comp_left_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left toComma CategoryTheory.CommaMorphism.left Hom.toCommaMorphism CategoryTheory.MorphismProperty.Comma instCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_left
comp_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right toComma Hom.toCommaMorphism CategoryTheory.CategoryStruct.comp CategoryTheory.MorphismProperty.Comma CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Comma.right	—	—
comp_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right toComma CategoryTheory.CommaMorphism.right Hom.toCommaMorphism CategoryTheory.MorphismProperty.Comma instCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_right
eqToHom_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left toComma Hom.toCommaMorphism CategoryTheory.eqToHom CategoryTheory.MorphismProperty.Comma CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Comma.left	—	—
eqToHom_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right toComma Hom.toCommaMorphism CategoryTheory.eqToHom CategoryTheory.MorphismProperty.Comma CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Comma.right	—	—
ext 📖	—	CategoryTheory.Comma.left toComma CategoryTheory.Comma.right Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.hom	—	—	—
ext_iff 📖	mathematical	—	CategoryTheory.Comma.left toComma CategoryTheory.Comma.right Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.hom	—	ext
forget_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Comma CategoryTheory.commaCategory forget Hom.hom	—	—
forget_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Comma CategoryTheory.commaCategory forget toComma	—	—
homFromCommaOfIsIso_hom 📖	mathematical	—	Hom.hom homFromCommaOfIsIso	—	—
hom_homFromCommaOfIsIso 📖	mathematical	—	homFromCommaOfIsIso Hom.hom	—	—
id_hom 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id CategoryTheory.MorphismProperty.Comma CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Comma CategoryTheory.commaCategory toComma	—	—
id_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left toComma Hom.toCommaMorphism id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	—
id_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right toComma Hom.toCommaMorphism id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	—
instFaithfulChangeProp 📖	mathematical	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	CategoryTheory.Functor.Faithful CategoryTheory.MorphismProperty.Comma instCategory changeProp	—	Hom.ext'
instFaithfulCommaForget 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Comma CategoryTheory.commaCategory forget	—	Hom.ext'
instFullChangeProp 📖	mathematical	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	CategoryTheory.Functor.Full CategoryTheory.MorphismProperty.Comma instCategory changeProp le_rfl CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	CategoryTheory.Functor.FullyFaithful.full le_rfl
instFullTopCommaForget 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.MorphismProperty.Comma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra instCategory CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.Comma CategoryTheory.commaCategory forget	—	CategoryTheory.Functor.FullyFaithful.full CategoryTheory.MorphismProperty.IsMultiplicative.instTop
instIsIsoCommaHom 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Comma CategoryTheory.commaCategory toComma Hom.hom	—	CategoryTheory.Functor.map_isIso
instIsIsoHomFromCommaOfIsIso 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.MorphismProperty.Comma instCategory homFromCommaOfIsIso	—	CategoryTheory.IsIso.inv_isIso Hom.ext' CategoryTheory.IsIso.hom_inv_id CategoryTheory.IsIso.inv_hom_id
instReflectsIsomorphismsCommaForgetOfRespectsIso 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Comma CategoryTheory.commaCategory forget	—	hom_homFromCommaOfIsIso instIsIsoHomFromCommaOfIsIso
inv_hom 📖	mathematical	—	Hom.hom CategoryTheory.inv CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Comma CategoryTheory.commaCategory toComma instIsIsoCommaHom	—	CategoryTheory.IsIso.eq_inv_of_hom_inv_id instIsIsoCommaHom comp_hom CategoryTheory.IsIso.hom_inv_id id_hom
isoFromComma_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.MorphismProperty.Comma instCategory isoFromComma homFromCommaOfIsIso CategoryTheory.Comma CategoryTheory.commaCategory toComma	—	—
isoFromComma_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.MorphismProperty.Comma instCategory isoFromComma homFromCommaOfIsIso CategoryTheory.Comma CategoryTheory.commaCategory toComma	—	—
isoMk_hom_left 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.left toComma Hom.toCommaMorphism CategoryTheory.Iso.hom CategoryTheory.MorphismProperty.Comma instCategory isoMk CategoryTheory.Comma.left	—	—
isoMk_hom_right 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.right toComma Hom.toCommaMorphism CategoryTheory.Iso.hom CategoryTheory.MorphismProperty.Comma instCategory isoMk CategoryTheory.Comma.right	—	—
isoMk_inv_left 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.left toComma Hom.toCommaMorphism CategoryTheory.Iso.inv CategoryTheory.MorphismProperty.Comma instCategory isoMk CategoryTheory.Comma.left	—	—
isoMk_inv_right 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.right toComma Hom.toCommaMorphism CategoryTheory.Iso.inv CategoryTheory.MorphismProperty.Comma instCategory isoMk CategoryTheory.Comma.right	—	—
lift_map_hom 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.left CategoryTheory.Functor.map CategoryTheory.CommaMorphism.right	Hom.hom CategoryTheory.Functor.map CategoryTheory.MorphismProperty.Comma instCategory lift CategoryTheory.Comma CategoryTheory.commaCategory	—	—
lift_obj_toComma 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.left CategoryTheory.Functor.map CategoryTheory.CommaMorphism.right	toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory lift CategoryTheory.Comma CategoryTheory.commaCategory	—	—
mapLeftComp_hom_app_left 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Comma.hom CategoryTheory.Functor CategoryTheory.Functor.category	CategoryTheory.CommaMorphism.left toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory mapLeft CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.hom mapLeftComp CategoryTheory.CategoryStruct.id CategoryTheory.Comma.left	—	—
mapLeftComp_hom_app_right 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Comma.hom CategoryTheory.Functor CategoryTheory.Functor.category	CategoryTheory.CommaMorphism.right toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory mapLeft CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.hom mapLeftComp CategoryTheory.CategoryStruct.id CategoryTheory.Comma.right	—	—
mapLeftComp_inv_app_left 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Comma.hom CategoryTheory.Functor CategoryTheory.Functor.category	CategoryTheory.CommaMorphism.left toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Functor.comp mapLeft CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.inv mapLeftComp CategoryTheory.CategoryStruct.id CategoryTheory.Comma.left	—	—
mapLeftComp_inv_app_right 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Comma.hom CategoryTheory.Functor CategoryTheory.Functor.category	CategoryTheory.CommaMorphism.right toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Functor.comp mapLeft CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.inv mapLeftComp CategoryTheory.CategoryStruct.id CategoryTheory.Comma.right	—	—
mapLeftEq_hom_app_left 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.left toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory mapLeft Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct mapLeftEq CategoryTheory.CategoryStruct.id CategoryTheory.Comma.left	—	—
mapLeftEq_hom_app_right 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.right toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory mapLeft Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct mapLeftEq CategoryTheory.CategoryStruct.id CategoryTheory.Comma.right	—	—
mapLeftEq_inv_app_left 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.left toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory mapLeft Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct mapLeftEq CategoryTheory.CategoryStruct.id CategoryTheory.Comma.left	—	—
mapLeftEq_inv_app_right 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.right toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory mapLeft Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct mapLeftEq CategoryTheory.CategoryStruct.id CategoryTheory.Comma.right	—	—
mapLeftId_hom_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory mapLeft CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.hom mapLeftId CategoryTheory.Comma.left	—	—
mapLeftId_hom_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory mapLeft CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.hom mapLeftId CategoryTheory.Comma.right	—	—
mapLeftId_inv_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Functor.id mapLeft CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.inv mapLeftId CategoryTheory.Comma.left	—	—
mapLeftId_inv_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Functor.id mapLeft CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.inv mapLeftId CategoryTheory.Comma.right	—	—
mapLeftIso_counitIso_hom_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Functor.comp mapLeft CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.inv CategoryTheory.Functor.id Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Equivalence.counitIso mapLeftIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	CategoryTheory.Category.comp_id
mapLeftIso_counitIso_hom_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Functor.comp mapLeft CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.inv CategoryTheory.Functor.id Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Equivalence.counitIso mapLeftIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	CategoryTheory.Category.comp_id
mapLeftIso_counitIso_inv_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp mapLeft CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.inv Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Equivalence.counitIso mapLeftIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	CategoryTheory.Category.comp_id
mapLeftIso_counitIso_inv_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp mapLeft CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.inv Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Equivalence.counitIso mapLeftIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	CategoryTheory.Category.comp_id
mapLeftIso_functor_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left toComma Hom.toCommaMorphism CategoryTheory.Functor.map CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Equivalence.functor mapLeftIso Hom.hom	—	—
mapLeftIso_functor_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right toComma Hom.toCommaMorphism CategoryTheory.Functor.map CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Equivalence.functor mapLeftIso Hom.hom	—	—
mapLeftIso_functor_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Equivalence.functor mapLeftIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category	—	—
mapLeftIso_functor_obj_left 📖	mathematical	—	CategoryTheory.Comma.left toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Equivalence.functor mapLeftIso	—	—
mapLeftIso_functor_obj_right 📖	mathematical	—	CategoryTheory.Comma.right toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Equivalence.functor mapLeftIso	—	—
mapLeftIso_inverse_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left toComma Hom.toCommaMorphism CategoryTheory.Functor.map CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Equivalence.inverse mapLeftIso Hom.hom	—	—
mapLeftIso_inverse_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right toComma Hom.toCommaMorphism CategoryTheory.Functor.map CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Equivalence.inverse mapLeftIso Hom.hom	—	—
mapLeftIso_inverse_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Equivalence.inverse mapLeftIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category	—	—
mapLeftIso_inverse_obj_left 📖	mathematical	—	CategoryTheory.Comma.left toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Equivalence.inverse mapLeftIso	—	—
mapLeftIso_inverse_obj_right 📖	mathematical	—	CategoryTheory.Comma.right toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Equivalence.inverse mapLeftIso	—	—
mapLeftIso_unitIso_hom_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp mapLeft CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.hom Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Equivalence.unitIso mapLeftIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	CategoryTheory.Category.comp_id
mapLeftIso_unitIso_hom_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp mapLeft CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.hom Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Equivalence.unitIso mapLeftIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	CategoryTheory.Category.comp_id
mapLeftIso_unitIso_inv_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Functor.comp mapLeft CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.hom CategoryTheory.Functor.id Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Equivalence.unitIso mapLeftIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	CategoryTheory.Category.comp_id
mapLeftIso_unitIso_inv_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Functor.comp mapLeft CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.hom CategoryTheory.Functor.id Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Equivalence.unitIso mapLeftIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	CategoryTheory.Category.comp_id
mapLeft_map_left 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.left toComma Hom.toCommaMorphism CategoryTheory.Functor.map CategoryTheory.MorphismProperty.Comma instCategory mapLeft Hom.hom	—	—
mapLeft_map_right 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.right toComma Hom.toCommaMorphism CategoryTheory.Functor.map CategoryTheory.MorphismProperty.Comma instCategory mapLeft Hom.hom	—	—
mapLeft_obj_hom 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Comma.hom	CategoryTheory.Comma.hom toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory mapLeft CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.NatTrans.app	—	—
mapLeft_obj_left 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Comma.hom	CategoryTheory.Comma.left toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory mapLeft	—	—
mapLeft_obj_right 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Comma.hom	CategoryTheory.Comma.right toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory mapLeft	—	—
mapRightComp_hom_app_left 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category	CategoryTheory.CommaMorphism.left toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory mapRight CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.hom mapRightComp CategoryTheory.CategoryStruct.id CategoryTheory.Comma.left	—	—
mapRightComp_hom_app_right 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category	CategoryTheory.CommaMorphism.right toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory mapRight CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.hom mapRightComp CategoryTheory.CategoryStruct.id CategoryTheory.Comma.right	—	—
mapRightComp_inv_app_left 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category	CategoryTheory.CommaMorphism.left toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Functor.comp mapRight CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.inv mapRightComp CategoryTheory.CategoryStruct.id CategoryTheory.Comma.left	—	—
mapRightComp_inv_app_right 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category	CategoryTheory.CommaMorphism.right toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Functor.comp mapRight CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.inv mapRightComp CategoryTheory.CategoryStruct.id CategoryTheory.Comma.right	—	—
mapRightEq_hom_app_left 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom CategoryTheory.NatTrans.app	CategoryTheory.CommaMorphism.left toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory mapRight Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct mapRightEq CategoryTheory.CategoryStruct.id CategoryTheory.Comma.left	—	—
mapRightEq_hom_app_right 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom CategoryTheory.NatTrans.app	CategoryTheory.CommaMorphism.right toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory mapRight Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct mapRightEq CategoryTheory.CategoryStruct.id CategoryTheory.Comma.right	—	—
mapRightEq_inv_app_left 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom CategoryTheory.NatTrans.app	CategoryTheory.CommaMorphism.left toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory mapRight Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct mapRightEq CategoryTheory.CategoryStruct.id CategoryTheory.Comma.left	—	—
mapRightEq_inv_app_right 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom CategoryTheory.NatTrans.app	CategoryTheory.CommaMorphism.right toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory mapRight Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct mapRightEq CategoryTheory.CategoryStruct.id CategoryTheory.Comma.right	—	—
mapRightId_hom_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory mapRight CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.hom mapRightId CategoryTheory.Comma.left	—	—
mapRightId_hom_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory mapRight CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.hom mapRightId CategoryTheory.Comma.right	—	—
mapRightId_inv_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Functor.id mapRight CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.inv mapRightId CategoryTheory.Comma.left	—	—
mapRightId_inv_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Functor.id mapRight CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Iso.inv mapRightId CategoryTheory.Comma.right	—	—
mapRightIso_counitIso_hom_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Functor.comp mapRight CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.hom CategoryTheory.Functor.id Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Equivalence.counitIso mapRightIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	CategoryTheory.Category.comp_id
mapRightIso_counitIso_hom_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Functor.comp mapRight CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.hom CategoryTheory.Functor.id Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Equivalence.counitIso mapRightIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	CategoryTheory.Category.comp_id
mapRightIso_counitIso_inv_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp mapRight CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.hom Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Equivalence.counitIso mapRightIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	CategoryTheory.Category.comp_id
mapRightIso_counitIso_inv_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp mapRight CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.hom Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Equivalence.counitIso mapRightIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	CategoryTheory.Category.comp_id
mapRightIso_functor_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left toComma Hom.toCommaMorphism CategoryTheory.Functor.map CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Equivalence.functor mapRightIso Hom.hom	—	—
mapRightIso_functor_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right toComma Hom.toCommaMorphism CategoryTheory.Functor.map CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Equivalence.functor mapRightIso Hom.hom	—	—
mapRightIso_functor_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Equivalence.functor mapRightIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category	—	—
mapRightIso_functor_obj_left 📖	mathematical	—	CategoryTheory.Comma.left toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Equivalence.functor mapRightIso	—	—
mapRightIso_functor_obj_right 📖	mathematical	—	CategoryTheory.Comma.right toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Equivalence.functor mapRightIso	—	—
mapRightIso_inverse_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left toComma Hom.toCommaMorphism CategoryTheory.Functor.map CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Equivalence.inverse mapRightIso Hom.hom	—	—
mapRightIso_inverse_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right toComma Hom.toCommaMorphism CategoryTheory.Functor.map CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Equivalence.inverse mapRightIso Hom.hom	—	—
mapRightIso_inverse_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Equivalence.inverse mapRightIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category	—	—
mapRightIso_inverse_obj_left 📖	mathematical	—	CategoryTheory.Comma.left toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Equivalence.inverse mapRightIso	—	—
mapRightIso_inverse_obj_right 📖	mathematical	—	CategoryTheory.Comma.right toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Equivalence.inverse mapRightIso	—	—
mapRightIso_unitIso_hom_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp mapRight CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.inv Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Equivalence.unitIso mapRightIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	CategoryTheory.Category.comp_id
mapRightIso_unitIso_hom_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp mapRight CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.inv Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Equivalence.unitIso mapRightIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	CategoryTheory.Category.comp_id
mapRightIso_unitIso_inv_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Functor.comp mapRight CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.inv CategoryTheory.Functor.id Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Equivalence.unitIso mapRightIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	CategoryTheory.Category.comp_id
mapRightIso_unitIso_inv_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory CategoryTheory.Functor.comp mapRight CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.inv CategoryTheory.Functor.id Hom.toCommaMorphism CategoryTheory.NatTrans.app CategoryTheory.Equivalence.unitIso mapRightIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	CategoryTheory.Category.comp_id
mapRight_map_left 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom CategoryTheory.NatTrans.app	CategoryTheory.CommaMorphism.left toComma Hom.toCommaMorphism CategoryTheory.Functor.map CategoryTheory.MorphismProperty.Comma instCategory mapRight Hom.hom	—	—
mapRight_map_right 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom CategoryTheory.NatTrans.app	CategoryTheory.CommaMorphism.right toComma Hom.toCommaMorphism CategoryTheory.Functor.map CategoryTheory.MorphismProperty.Comma instCategory mapRight Hom.hom	—	—
mapRight_obj_hom 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom CategoryTheory.NatTrans.app	CategoryTheory.Comma.hom toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory mapRight CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.NatTrans.app	—	—
mapRight_obj_left 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom CategoryTheory.NatTrans.app	CategoryTheory.Comma.left toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory mapRight	—	—
mapRight_obj_right 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom CategoryTheory.NatTrans.app	CategoryTheory.Comma.right toComma CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Comma instCategory mapRight	—	—
prop 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Comma.left toComma CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
toCommaMorphism_eq_hom 📖	mathematical	—	Hom.toCommaMorphism Hom.hom	—	—

CategoryTheory.MorphismProperty.Comma.Hom

Definitions

Name	Category	Theorems
comp 📖	CompOp	2 math math: comp_left, comp_right
hom 📖	CompOp	31 math math: CategoryTheory.MorphismProperty.Comma.mapRightIso_functor_map_right, CategoryTheory.MorphismProperty.Over.map_map_left, CategoryTheory.MorphismProperty.Comma.mapRightIso_functor_map_left, hom_mk, CategoryTheory.MorphismProperty.Comma.mapLeftIso_functor_map_left, CategoryTheory.MorphismProperty.Comma.homFromCommaOfIsIso_hom, CategoryTheory.MorphismProperty.Comma.mapLeftIso_functor_map_right, CategoryTheory.MorphismProperty.Comma.mapLeftIso_inverse_map_left, CategoryTheory.MorphismProperty.Comma.hom_homFromCommaOfIsIso, CategoryTheory.MorphismProperty.Under.homMk_hom, CategoryTheory.MorphismProperty.Comma.mapLeft_map_right, AlgebraicGeometry.Scheme.ProEt.forget_map, hom_right, CategoryTheory.MorphismProperty.Comma.toCommaMorphism_eq_hom, CategoryTheory.MorphismProperty.Under.Hom.mk_hom, ext'_iff, CategoryTheory.MorphismProperty.Comma.mapRightIso_inverse_map_left, CategoryTheory.MorphismProperty.Comma.mapRight_map_right, CategoryTheory.MorphismProperty.Comma.forget_map, CategoryTheory.MorphismProperty.Over.homMk_hom, CategoryTheory.MorphismProperty.Comma.id_hom, CategoryTheory.MorphismProperty.Comma.instIsIsoCommaHom, CategoryTheory.MorphismProperty.Comma.mapRight_map_left, CategoryTheory.MorphismProperty.Comma.mapRightIso_inverse_map_right, CategoryTheory.MorphismProperty.Comma.inv_hom, hom_left, CategoryTheory.MorphismProperty.Comma.comp_hom, CategoryTheory.MorphismProperty.Comma.mapLeftIso_inverse_map_right, CategoryTheory.MorphismProperty.Comma.lift_map_hom, CategoryTheory.MorphismProperty.Comma.mapLeft_map_left, CategoryTheory.MorphismProperty.Over.Hom.mk_hom
toCommaMorphism 📖	CompOp	114 math math: CategoryTheory.MorphismProperty.Comma.mapRightIso_functor_map_right, CategoryTheory.MorphismProperty.Comma.mapRightComp_hom_app_left, CategoryTheory.MorphismProperty.Comma.mapRightIso_counitIso_inv_app_left, ext_iff, CategoryTheory.MorphismProperty.Comma.mapRightIso_unitIso_inv_app_right, CategoryTheory.MorphismProperty.Comma.eqToHom_left, CategoryTheory.MorphismProperty.Comma.mapLeftEq_inv_app_right, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd_assoc, CategoryTheory.MorphismProperty.Over.pullbackComp_hom_app_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.isPullback, CategoryTheory.MorphismProperty.Comma.comp_right, AlgebraicGeometry.instIsOpenImmersionLeftSchemeDiscretePUnitMapWalkingSpanOverTopMorphismPropertySpan, CategoryTheory.MorphismProperty.CostructuredArrow.homMk_left, CategoryTheory.MorphismProperty.Comma.mapRightIso_counitIso_hom_app_right, CategoryTheory.MorphismProperty.Over.mapCongr_inv_app_left, CategoryTheory.MorphismProperty.Comma.mapLeftEq_inv_app_left, CategoryTheory.MorphismProperty.Comma.mapRightIso_counitIso_inv_app_right, CategoryTheory.MorphismProperty.Over.map_map_left, CategoryTheory.MorphismProperty.Comma.isoMk_hom_left, CategoryTheory.MorphismProperty.Comma.mapRightIso_functor_map_left, CategoryTheory.MorphismProperty.Over.Hom.ext_iff, CategoryTheory.MorphismProperty.Comma.comp_left_assoc, CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst, CategoryTheory.MorphismProperty.Comma.mapLeftIso_unitIso_inv_app_right, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst_assoc, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_f, CategoryTheory.MorphismProperty.Comma.mapRightId_inv_app_right, CategoryTheory.MorphismProperty.Comma.mapLeftIso_counitIso_hom_app_right, CategoryTheory.MorphismProperty.Over.isoMk_inv_left, CategoryTheory.MorphismProperty.Comma.mapLeftComp_hom_app_left, CategoryTheory.MorphismProperty.Comma.mapLeftIso_functor_map_left, CategoryTheory.MorphismProperty.Comma.mapRightEq_hom_app_left, CategoryTheory.MorphismProperty.Comma.mapLeftComp_inv_app_left, CategoryTheory.MorphismProperty.Under.isoMk_inv_right, CategoryTheory.MorphismProperty.Over.mapId_inv_app_left, CategoryTheory.MorphismProperty.Comma.isoMk_hom_right, CategoryTheory.MorphismProperty.Under.isoMk_hom_right, CategoryTheory.MorphismProperty.Over.mapCongr_hom_app_left, CategoryTheory.MorphismProperty.Comma.mapLeftIso_functor_map_right, CategoryTheory.MorphismProperty.Comma.isoMk_inv_left, CategoryTheory.MorphismProperty.Comma.mapLeftIso_inverse_map_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι, CategoryTheory.MorphismProperty.Over.forget_comp_forget_map, CategoryTheory.MorphismProperty.Over.pullbackComp_inv_app_left, prop_hom_left, CategoryTheory.MorphismProperty.Comma.comp_right_assoc, CategoryTheory.MorphismProperty.Comma.mapRightComp_hom_app_right, CategoryTheory.MorphismProperty.Comma.mapRightEq_inv_app_right, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_f, CategoryTheory.MorphismProperty.Comma.mapLeft_map_right, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι_assoc, CategoryTheory.MorphismProperty.Comma.mapRightId_inv_app_left, hom_right, CategoryTheory.MorphismProperty.Comma.mapRightIso_unitIso_inv_app_left, CategoryTheory.MorphismProperty.Comma.mapRightId_hom_app_right, CategoryTheory.MorphismProperty.Over.mapComp_hom_app_left, CategoryTheory.MorphismProperty.Comma.mapRightIso_counitIso_hom_app_left, CategoryTheory.MorphismProperty.Over.w_assoc, CategoryTheory.MorphismProperty.CostructuredArrow.toOver_map, CategoryTheory.MorphismProperty.Comma.mapLeftId_inv_app_right, AlgebraicGeometry.instIsOpenImmersionLeftSchemeDiscretePUnitιOverTopMorphismProperty, CategoryTheory.MorphismProperty.Comma.toCommaMorphism_eq_hom, comp_left, CategoryTheory.MorphismProperty.Under.w, CategoryTheory.MorphismProperty.Comma.mapRightIso_inverse_map_left, CategoryTheory.MorphismProperty.Comma.mapRight_map_right, CategoryTheory.MorphismProperty.Comma.mapRightComp_inv_app_left, CategoryTheory.MorphismProperty.Under.Hom.ext_iff, CategoryTheory.MorphismProperty.Comma.comp_left, CategoryTheory.MorphismProperty.Comma.isoMk_inv_right, CategoryTheory.MorphismProperty.Comma.mapLeftIso_counitIso_inv_app_right, CategoryTheory.MorphismProperty.Comma.mapRight_map_left, CategoryTheory.MorphismProperty.Under.forget_comp_forget_map, CategoryTheory.MorphismProperty.Over.w, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.trans_app_left, CategoryTheory.MorphismProperty.Comma.mapRightIso_inverse_map_right, CategoryTheory.MorphismProperty.Comma.mapRightIso_unitIso_hom_app_left, CategoryTheory.MorphismProperty.Comma.mapRightIso_unitIso_hom_app_right, CategoryTheory.MorphismProperty.Comma.mapLeftId_hom_app_left, CategoryTheory.MorphismProperty.Comma.mapLeftId_hom_app_right, CategoryTheory.MorphismProperty.CostructuredArrow.Hom.ext_iff, CategoryTheory.MorphismProperty.Over.pullback_map_left, CategoryTheory.MorphismProperty.Comma.mapLeftIso_unitIso_inv_app_left, CategoryTheory.MorphismProperty.Comma.mapLeftIso_counitIso_hom_app_left, CategoryTheory.MorphismProperty.Comma.mapRightId_hom_app_left, hom_left, CategoryTheory.MorphismProperty.Over.mapComp_inv_app_left, CategoryTheory.MorphismProperty.Under.w_assoc, CategoryTheory.MorphismProperty.Comma.mapLeftId_inv_app_left, CategoryTheory.MorphismProperty.Comma.mapLeftIso_counitIso_inv_app_left, CategoryTheory.MorphismProperty.Over.isoMk_hom_left, CategoryTheory.MorphismProperty.Comma.eqToHom_right, CategoryTheory.MorphismProperty.Comma.mapLeftIso_inverse_map_right, prop_hom_right, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_map, CategoryTheory.MorphismProperty.Comma.mapLeftEq_hom_app_right, CategoryTheory.MorphismProperty.Comma.mapLeftComp_hom_app_right, CategoryTheory.MorphismProperty.Comma.mapLeft_map_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst, CategoryTheory.MorphismProperty.Comma.mapLeftEq_hom_app_left, AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology, CategoryTheory.MorphismProperty.Over.mapId_hom_app_left, CategoryTheory.MorphismProperty.Over.pullbackComp_left_fst_fst, CategoryTheory.MorphismProperty.Comma.mapRightComp_inv_app_right, CategoryTheory.MorphismProperty.Comma.mapLeftComp_inv_app_right, comp_right, CategoryTheory.MorphismProperty.Comma.id_left, CategoryTheory.MorphismProperty.Comma.mapLeftIso_unitIso_hom_app_left, CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst_assoc, CategoryTheory.MorphismProperty.Comma.mapRightEq_inv_app_left, CategoryTheory.MorphismProperty.Comma.mapRightEq_hom_app_right, CategoryTheory.MorphismProperty.Comma.mapLeftIso_unitIso_hom_app_right, CategoryTheory.MorphismProperty.Comma.id_right

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.MorphismProperty.Comma.toComma toCommaMorphism comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	—
comp_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.MorphismProperty.Comma.toComma toCommaMorphism comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	—
ext 📖	—	CategoryTheory.CommaMorphism.left CategoryTheory.MorphismProperty.Comma.toComma toCommaMorphism CategoryTheory.CommaMorphism.right	—	—	—
ext' 📖	—	hom	—	—	ext
ext'_iff 📖	mathematical	—	hom	—	ext'
ext_iff 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.MorphismProperty.Comma.toComma toCommaMorphism CategoryTheory.CommaMorphism.right	—	ext
hom_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.MorphismProperty.Comma.toComma hom toCommaMorphism	—	—
hom_mk 📖	mathematical	CategoryTheory.Comma.left CategoryTheory.MorphismProperty.Comma.toComma CategoryTheory.CommaMorphism.left CategoryTheory.Comma.right CategoryTheory.CommaMorphism.right	hom	—	—
hom_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.MorphismProperty.Comma.toComma hom toCommaMorphism	—	—
prop_hom_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.MorphismProperty.Comma.toComma CategoryTheory.CommaMorphism.left toCommaMorphism	—	—
prop_hom_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.MorphismProperty.Comma.toComma CategoryTheory.CommaMorphism.right toCommaMorphism	—	—

CategoryTheory.MorphismProperty.Comma.Hom.Simps

Definitions

Name	Category	Theorems
hom 📖	CompOp	—

CategoryTheory.MorphismProperty.CostructuredArrow

Definitions

Name	Category	Theorems
forget 📖	CompOp	—
homMk 📖	CompOp	1 math math: homMk_left
mk 📖	CompOp	—
toOver 📖	CompOp	4 math math: CategoryTheory.MorphismProperty.instFaithfulCostructuredArrowTopOverToOver, toOver_map, toOver_obj, CategoryTheory.MorphismProperty.instFullCostructuredArrowTopOverToOver

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homMk_left 📖	mathematical	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism homMk	—	—
mk_hom 📖	mathematical	CategoryTheory.Functor.obj	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	—
mk_left 📖	mathematical	CategoryTheory.Functor.obj	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	—
toOver_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.MorphismProperty.CostructuredArrow Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.Over CategoryTheory.Functor.id toOver CategoryTheory.MorphismProperty.Over.homMk CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.MorphismProperty.Comma.toComma CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.left CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop
toOver_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.CostructuredArrow Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.Over CategoryTheory.Functor.id toOver CategoryTheory.Comma.left CategoryTheory.MorphismProperty.Comma.toComma CategoryTheory.Comma.hom	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop

CategoryTheory.MorphismProperty.CostructuredArrow.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism	—	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.Comma.Hom.ext' CategoryTheory.Comma.hom_ext
ext_iff 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop ext

CategoryTheory.MorphismProperty.HasFactorization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
over 📖	mathematical	—	CategoryTheory.MorphismProperty.HasFactorization CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.MorphismProperty.over	—	CategoryTheory.MorphismProperty.MapFactorizationData.fac_assoc CategoryTheory.Over.w CategoryTheory.Over.OverMorphism.ext CategoryTheory.MorphismProperty.MapFactorizationData.fac CategoryTheory.MorphismProperty.MapFactorizationData.hi CategoryTheory.MorphismProperty.MapFactorizationData.hp

CategoryTheory.MorphismProperty.Over

Definitions

Name	Category	Theorems
changeProp 📖	CompOp	2 math math: changeProp_obj_left, changeProp_obj_hom
forget 📖	CompOp	13 math math: CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_inducedTopology, AlgebraicGeometry.Scheme.locallyCoverDense_of_le, CategoryTheory.MorphismProperty.instFaithfulOverTopOverForget, forget_comp_forget_map, AlgebraicGeometry.instIsOpenImmersionMapSchemeCompOverOverTopMorphismPropertyForgetForget, instPreservesFiniteLimitsTopOverForget, CategoryTheory.MorphismProperty.instFullOverTopOverForget, CategoryTheory.MorphismProperty.exists_map_eq_of_presieve, AlgebraicGeometry.Scheme.instLocallyCoverDenseOverTopMorphismPropertyOverForgetOverGrothendieckTopology, CategoryTheory.MorphismProperty.locallyCoverDense_forget_of_le, AlgebraicGeometry.instIsLocallyDirectedCompSchemeOverOverTopMorphismPropertyForgetForgetForget, AlgebraicGeometry.instPreservesColimitOverSchemeTopMorphismPropertyOverForget, AlgebraicGeometry.instMonoObjWalkingSpanCompOverSchemeTopMorphismPropertySpanOverForgetForgetForgetNoneWalkingPairSomeMapInitOfIsOpenImmersionLeftDiscretePUnit
homMk 📖	CompOp	5 math math: pullbackMapHomPullback_app, mapPullbackAdj_counit_app, mapPullbackAdj_unit_app, CategoryTheory.MorphismProperty.CostructuredArrow.toOver_map, homMk_hom
isoMk 📖	CompOp	3 math math: isoMk_inv_left, isoMk_hom_left, CategoryTheory.MorphismProperty.overEquivOfIsInitial_unitIso
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
changeProp_obj_hom 📖	mathematical	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.MorphismProperty.IsMultiplicative.instTop changeProp	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop
changeProp_obj_left 📖	mathematical	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Functor.obj CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.MorphismProperty.IsMultiplicative.instTop changeProp	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop
forget_comp_forget_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.Functor.comp CategoryTheory.Over CategoryTheory.instCategoryOver forget CategoryTheory.Over.forget CategoryTheory.CommaMorphism.left CategoryTheory.MorphismProperty.Comma.toComma CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop
homMk_hom 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Comma.hom	CategoryTheory.MorphismProperty.Comma.Hom.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra homMk CategoryTheory.Over.homMk CategoryTheory.MorphismProperty.Comma.toComma	—	—
isoMk_hom_left 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Iso.hom CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.Iso.hom CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.MorphismProperty.IsMultiplicative.instTop isoMk CategoryTheory.Comma.left	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop
isoMk_inv_left 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Iso.hom CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.Iso.inv CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.MorphismProperty.IsMultiplicative.instTop isoMk CategoryTheory.Comma.left	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop
mk_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	—
mk_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	—
w 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.CommaMorphism.left CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.Comma.hom	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.Over.w
w_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.CommaMorphism.left CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' w

CategoryTheory.MorphismProperty.Over.Hom

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism	—	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.Comma.Hom.ext' CategoryTheory.Comma.hom_ext
ext_iff 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop ext
mk_hom 📖	mathematical	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.CommaMorphism.left	CategoryTheory.MorphismProperty.Comma.Hom.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	—

CategoryTheory.MorphismProperty.Under

Definitions

Name	Category	Theorems
forget 📖	CompOp	3 math math: CategoryTheory.MorphismProperty.instFullUnderTopUnderForget, forget_comp_forget_map, CategoryTheory.MorphismProperty.instFaithfulUnderTopUnderForget
homMk 📖	CompOp	1 math math: homMk_hom
isoMk 📖	CompOp	3 math math: isoMk_inv_right, isoMk_hom_right, CategoryTheory.MorphismProperty.underEquivOfIsTerminal_unitIso
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forget_comp_forget_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.MorphismProperty.Under CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.Functor.comp CategoryTheory.Under CategoryTheory.instCategoryUnder forget CategoryTheory.Under.forget CategoryTheory.CommaMorphism.right CategoryTheory.MorphismProperty.Comma.toComma CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop
homMk_hom 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Comma.hom	CategoryTheory.MorphismProperty.Comma.Hom.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra homMk CategoryTheory.Under.homMk CategoryTheory.MorphismProperty.Comma.toComma	—	—
isoMk_hom_right 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Comma.hom CategoryTheory.Iso.hom	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.Iso.hom CategoryTheory.MorphismProperty.Under CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.MorphismProperty.IsMultiplicative.instTop isoMk CategoryTheory.Comma.right	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop
isoMk_inv_right 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Comma.hom CategoryTheory.Iso.hom	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.Iso.inv CategoryTheory.MorphismProperty.Under CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.MorphismProperty.IsMultiplicative.instTop isoMk CategoryTheory.Comma.right	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop
mk_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	—
mk_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	—
w 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.right CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.Under.w
w_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.right CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' w

CategoryTheory.MorphismProperty.Under.Hom

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism	—	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.MorphismProperty.Comma.Hom.ext' CategoryTheory.Comma.hom_ext
ext_iff 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop ext
mk_hom 📖	mathematical	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.CommaMorphism.right	CategoryTheory.MorphismProperty.Comma.Hom.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	—

---

← Back to Index