Basic

📁 Source: Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean

Statistics

Metric	Count
Definitions HasLeftKanExtension, HasRightKanExtension, IsLeftKanExtension, IsRightKanExtension, LeftExtension, isUniversalEquivOfIso₂, isUniversalOfPrecomp₂, isUniversalPostcomp₁Equiv, isUniversalPrecompEquiv, isUniversalPrecomp₂, isUniversalPrecomp₂Equiv, mk, postcompose₂, postcompose₂ObjMkIso, postcomp₁, precomp, precomp₂, RightExtension, isUniversalEquivOfIso₂, isUniversalPostcomp₁Equiv, isUniversalPrecompEquiv, mk, postcompose₂, postcompose₂ObjMkIso, postcomp₁, precomp, coconeOfIsLeftKanExtension, colimitIsoOfIsLeftKanExtension, coneOfIsRightKanExtension, descOfIsLeftKanExtension, homEquivOfIsLeftKanExtension, homEquivOfIsRightKanExtension, isColimitCoconeOfIsLeftKanExtension, isLimitConeOfIsRightKanExtension, isUniversalOfIsLeftKanExtension, isUniversalOfIsRightKanExtension, leftExtensionEquivalenceOfIso₁, leftExtensionEquivalenceOfIso₂, leftKanExtension, leftKanExtensionUnique, leftKanExtensionUniqueOfIso, leftKanExtensionUnit, liftOfIsRightKanExtension, limitIsoOfIsRightKanExtension, rightExtensionEquivalenceOfIso₁, rightExtensionEquivalenceOfIso₂, rightKanExtension, rightKanExtensionCounit, rightKanExtensionUnique, rightKanExtensionUniqueOfIso	50
Theorems mk, mk, nonempty_isUniversal, nonempty_isUniversal, mk_hom, mk_left_as, mk_right, postcompose₂ObjMkIso_hom_right_app, postcompose₂ObjMkIso_inv_right_app, postcompose₂_map_left, postcompose₂_map_right_app, postcompose₂_obj_hom_app, postcompose₂_obj_left, postcompose₂_obj_right_map, postcompose₂_obj_right_obj, postcomp₁_map_left, postcomp₁_map_right_app, postcomp₁_obj_hom_app, postcomp₁_obj_left, postcomp₁_obj_right_map, postcomp₁_obj_right_obj, precomp_map_left, precomp_map_right, precomp_obj_hom_app, precomp_obj_left, precomp_obj_right, precomp₂_map_left, precomp₂_map_right, precomp₂_obj_hom_app, precomp₂_obj_left, precomp₂_obj_right, mk_hom, mk_left, mk_right_as, postcompose₂ObjMkIso_hom_left_app, postcompose₂ObjMkIso_inv_left_app, postcompose₂_map_left_app, postcompose₂_map_right, postcompose₂_obj_hom_app, postcompose₂_obj_left_map, postcompose₂_obj_left_obj, postcompose₂_obj_right, postcomp₁_map_left_app, postcomp₁_map_right, postcomp₁_obj_hom_app, postcomp₁_obj_left_map, postcomp₁_obj_left_obj, postcomp₁_obj_right, precomp_map_left, precomp_map_right, precomp_obj_hom_app, precomp_obj_left, precomp_obj_right, coconeOfIsLeftKanExtension_pt, coconeOfIsLeftKanExtension_ι, coneOfIsRightKanExtension_pt, coneOfIsRightKanExtension_π, descOfIsLeftKanExtension_fac, descOfIsLeftKanExtension_fac_app, descOfIsLeftKanExtension_fac_app_assoc, descOfIsLeftKanExtension_fac_assoc, hasLeftExtension_iff_of_iso₁, hasLeftExtension_iff_of_iso₂, hasLeftExtension_iff_postcomp₁, hasRightExtension_iff_of_iso₁, hasRightExtension_iff_of_iso₂, hasRightExtension_iff_postcomp₁, homEquivOfIsLeftKanExtension_apply_app, homEquivOfIsLeftKanExtension_symm_apply, homEquivOfIsRightKanExtension_apply_app, homEquivOfIsRightKanExtension_symm_apply, hom_ext_of_isLeftKanExtension, hom_ext_of_isRightKanExtension, instIsEquivalenceLeftExtensionCompPrecomp, instIsEquivalenceLeftExtensionPostcomp₁OfIsIso, instIsEquivalenceRightExtensionCompPrecomp, instIsEquivalenceRightExtensionPostcomp₁OfIsIso, instIsLeftKanExtensionLeftKanExtensionLeftKanExtensionUnit, instIsRightKanExtensionRightKanExtensionRightKanExtensionCounit, isColimitCoconeOfIsLeftKanExtension_desc, isLeftKanExtensionAlongEquivalence, isLeftKanExtensionAlongEquivalence', isLeftKanExtensionId, isLeftKanExtension_iff_isIso, isLeftKanExtension_iff_of_iso, isLeftKanExtension_iff_of_iso₂, isLeftKanExtension_iff_postcompose, isLeftKanExtension_iff_postcomp₁, isLeftKanExtension_iff_precomp, isLeftKanExtension_of_iso, isLimitConeOfIsRightKanExtension_lift, isRightKanExtensionAlongEquivalence, isRightKanExtensionAlongEquivalence', isRightKanExtensionId, isRightKanExtension_iff_isIso, isRightKanExtension_iff_of_iso, isRightKanExtension_iff_of_iso₂, isRightKanExtension_iff_postcomp₁, isRightKanExtension_iff_precomp, isRightKanExtension_of_iso, leftExtensionEquivalenceOfIso₁_counitIso_hom_app_right_app, leftExtensionEquivalenceOfIso₁_counitIso_inv_app_right_app, leftExtensionEquivalenceOfIso₁_functor_map_left, leftExtensionEquivalenceOfIso₁_functor_map_right, leftExtensionEquivalenceOfIso₁_functor_obj_hom_app, leftExtensionEquivalenceOfIso₁_functor_obj_left, leftExtensionEquivalenceOfIso₁_functor_obj_right, leftExtensionEquivalenceOfIso₁_inverse_map_left, leftExtensionEquivalenceOfIso₁_inverse_map_right, leftExtensionEquivalenceOfIso₁_inverse_obj_hom_app, leftExtensionEquivalenceOfIso₁_inverse_obj_left, leftExtensionEquivalenceOfIso₁_inverse_obj_right, leftExtensionEquivalenceOfIso₁_unitIso_hom_app_right_app, leftExtensionEquivalenceOfIso₁_unitIso_inv_app_right_app, leftKanExtensionUniqueOfIso_hom, leftKanExtensionUniqueOfIso_inv, leftKanExtensionUnique_hom, leftKanExtensionUnique_inv, leftKanExtension_hom_ext, leftKanExtension_hom_ext_iff, liftOfIsRightKanExtension_fac, liftOfIsRightKanExtension_fac_app, liftOfIsRightKanExtension_fac_app_assoc, liftOfIsRightKanExtension_fac_assoc, limitIsoOfIsRightKanExtension_hom_π, limitIsoOfIsRightKanExtension_hom_π_assoc, limitIsoOfIsRightKanExtension_inv_π, limitIsoOfIsRightKanExtension_inv_π_assoc, rightKanExtensionUniqueOfIso_hom, rightKanExtensionUniqueOfIso_inv, rightKanExtensionUnique_hom, rightKanExtensionUnique_inv, rightKanExtension_hom_ext, rightKanExtension_hom_ext_iff, ι_colimitIsoOfIsLeftKanExtension_hom, ι_colimitIsoOfIsLeftKanExtension_hom_assoc, ι_colimitIsoOfIsLeftKanExtension_inv, ι_colimitIsoOfIsLeftKanExtension_inv_assoc	138
Total	188

CategoryTheory.Functor

Definitions

Name	Category	Theorems
HasLeftKanExtension 📖	MathDef	11 math math: hasRightDerivedFunctor_iff, LeftExtension.IsPointwiseLeftKanExtension.hasLeftKanExtension, hasLeftExtension_iff_of_iso₁, HasRightDerivedFunctor.hasLeftKanExtension', hasLeftExtension_iff_of_iso₂, HasLeftKanExtension.mk, CategoryTheory.TwoSquare.hasLeftKanExtension, instHasLeftKanExtension, HasRightDerivedFunctor.hasLeftKanExtension, hasLeftKanExtension_of_preserves, hasLeftExtension_iff_postcomp₁
HasRightKanExtension 📖	MathDef	10 math math: HasRightKanExtension.mk, hasLeftDerivedFunctor_iff, HasLeftDerivedFunctor.hasRightKanExtension', hasRightExtension_iff_of_iso₁, HasLeftDerivedFunctor.hasRightKanExtension, instHasRightKanExtension, hasRightKanExtension_of_preserves, RightExtension.IsPointwiseRightKanExtension.hasRightKanExtension, hasRightExtension_iff_of_iso₂, hasRightExtension_iff_postcomp₁
IsLeftKanExtension 📖	CompData	36 math math: isLeftKanExtension_iff_isIso, IsRightDerivedFunctor.isLeftKanExtension, isRightDerivedFunctor_iff_isLeftKanExtension, CategoryTheory.MonoidalCategory.DayFunctor.instIsLeftKanExtensionDiscretePUnitFunctorTensorUnitνNatTrans, isLeftKanExtension_of_iso, CategoryTheory.Presheaf.instIsLeftKanExtensionFunctorOppositeTypeLanOpHomCompULiftYonedaIsoULiftYonedaCompLan, instIsLeftKanExtensionSimplexCategoryTopCatSSetToTopInvFunctorToTopSimplex, instIsLeftKanExtensionPointwiseLeftKanExtensionPointwiseLeftKanExtensionUnit, CategoryTheory.Presheaf.isLeftKanExtension_along_yoneda_iff, LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension, instIsLeftKanExtensionObjLanAppLanUnit, isLeftKanExtension_iff_postcompose, CategoryTheory.MonoidalCategory.DayConvolution.instIsLeftKanExtensionProdExternalProductConvolutionExtensionUnitRightUnit, CategoryTheory.Presheaf.isLeftKanExtension_along_uliftYoneda_iff, CategoryTheory.TwoSquare.isIso_lanBaseChange_app_iff, CategoryTheory.MonoidalCategory.DayConvolutionUnit.instIsLeftKanExtensionProdDiscretePUnitExternalProductExtensionUnitLeftφ, CategoryTheory.Presheaf.instIsLeftKanExtensionOppositeObjFunctorTypeYonedaYonedaMap, isIso_lanAdjunction_homEquiv_symm_iff, isLeftKanExtensionId, isLeftKanExtension_iff_postcomp₁, CategoryTheory.Presheaf.isLeftKanExtension_of_preservesColimits, isLeftKanExtensionAlongEquivalence, PreservesLeftKanExtension.preserves, CategoryTheory.MonoidalCategory.DayConvolution.instIsLeftKanExtensionProdExternalProductConvolutionExtensionUnitLeftUnit, CategoryTheory.SimplicialObject.instIsLeftKanExtensionOppositeTruncatedSimplexCategoryObjSkAppTruncatedUnitSkAdjTruncation, CategoryTheory.MonoidalCategory.DayFunctor.instIsLeftKanExtensionProdFunctorTensorObjη, isLeftKanExtension_iff_precomp, instIsLeftKanExtensionLeftKanExtensionLeftKanExtensionUnit, CategoryTheory.Presheaf.instIsLeftKanExtensionFunctorOppositeTypeIdCompUliftYonedaOfPreservesColimitsOfSizeOfHasPointwiseLeftKanExtension, isLeftKanExtension_iff_of_iso, isIso_lanAdjunction_counit_app_iff, isLeftKanExtensionAlongEquivalence', isLeftKanExtension_iff_of_iso₂, CategoryTheory.MonoidalCategory.DayConvolutionUnit.instIsLeftKanExtensionProdDiscretePUnitExternalProductExtensionUnitRightφ, CategoryTheory.Presheaf.instIsLeftKanExtensionOppositeObjFunctorTypeUliftYonedaUliftYonedaMap, CategoryTheory.MonoidalCategory.DayConvolution.leftKanExtension
IsRightKanExtension 📖	CompData	23 math math: CategoryTheory.SimplicialObject.instIsRightKanExtensionOppositeTruncatedSimplexCategoryObjCoskAppTruncatedCounitCoskAdjTruncation, PreservesRightKanExtension.preserves, isRightKanExtension_iff_of_iso, isLeftDerivedFunctor_iff_isRightKanExtension, instIsRightKanExtensionRightKanExtensionRightKanExtensionCounit, isIso_ranAdjunction_unit_app_iff, Condensed.instIsRightKanExtensionFintypeCatCondensedModProfiniteProfiniteSolidProfiniteSolidCounit, CategoryTheory.SimplicialObject.isCoskeletal_iff, IsLeftDerivedFunctor.isRightKanExtension, isIso_ranAdjunction_homEquiv_iff, instIsRightKanExtensionObjRanAppRanCounit, RightExtension.IsPointwiseRightKanExtension.isRightKanExtension, CategoryTheory.SimplicialObject.IsCoskeletal.isRightKanExtension, isRightKanExtensionId, isRightKanExtension_iff_precomp, isRightKanExtension_iff_isIso, isRightKanExtensionAlongEquivalence', instIsRightKanExtensionPointwiseRightKanExtensionPointwiseRightKanExtensionCounit, isRightKanExtension_iff_postcomp₁, SSet.StrictSegal.isRightKanExtension, isRightKanExtension_of_iso, isRightKanExtension_iff_of_iso₂, isRightKanExtensionAlongEquivalence
LeftExtension 📖	CompOp	45 math math: LeftExtension.coconeAtFunctor_map_hom, leftExtensionEquivalenceOfIso₁_functor_map_left, LeftExtension.precomp₂_obj_hom_app, LeftExtension.precomp₂_map_right, LeftExtension.postcomp₁_map_right_app, leftExtensionEquivalenceOfIso₁_functor_obj_left, LeftExtension.postcomp₁_obj_left, LeftExtension.precomp_map_right, LeftExtension.precomp₂_obj_left, LeftExtension.precomp_obj_hom_app, LeftExtension.coconeAtWhiskerRightIso_inv_hom, LeftExtension.postcompose₂_obj_right_map, leftExtensionEquivalenceOfIso₁_inverse_map_left, leftExtensionEquivalenceOfIso₁_inverse_obj_left, LeftExtension.postcompose₂ObjMkIso_inv_right_app, LeftExtension.postcompose₂_map_right_app, instIsEquivalenceLeftExtensionPostcomp₁OfIsIso, LeftExtension.postcompose₂_obj_hom_app, LeftExtension.postcomp₁_obj_hom_app, leftExtensionEquivalenceOfIso₁_inverse_map_right, LeftExtension.postcompose₂_obj_right_obj, leftExtensionEquivalenceOfIso₁_inverse_obj_right, leftExtensionEquivalenceOfIso₁_counitIso_inv_app_right_app, LeftExtension.postcompose₂ObjMkIso_hom_right_app, LeftExtension.postcomp₁_obj_right_map, PreservesPointwiseLeftKanExtensionAt.preserves, LeftExtension.coconeAtFunctor_obj, LeftExtension.coconeAtWhiskerRightIso_hom_hom, instIsEquivalenceLeftExtensionCompPrecomp, leftExtensionEquivalenceOfIso₁_inverse_obj_hom_app, LeftExtension.precomp_obj_right, LeftExtension.postcompose₂_obj_left, LeftExtension.precomp_obj_left, leftExtensionEquivalenceOfIso₁_functor_obj_hom_app, LeftExtension.postcompose₂_map_left, LeftExtension.postcomp₁_obj_right_obj, LeftExtension.precomp_map_left, LeftExtension.precomp₂_obj_right, LeftExtension.postcomp₁_map_left, leftExtensionEquivalenceOfIso₁_unitIso_hom_app_right_app, LeftExtension.precomp₂_map_left, leftExtensionEquivalenceOfIso₁_counitIso_hom_app_right_app, leftExtensionEquivalenceOfIso₁_functor_map_right, leftExtensionEquivalenceOfIso₁_unitIso_inv_app_right_app, leftExtensionEquivalenceOfIso₁_functor_obj_right
RightExtension 📖	CompOp	26 math math: RightExtension.postcompose₂_obj_left_map, RightExtension.postcompose₂_obj_right, RightExtension.postcomp₁_obj_left_map, RightExtension.postcomp₁_map_right, RightExtension.precomp_map_left, instIsEquivalenceRightExtensionPostcomp₁OfIsIso, RightExtension.coneAtFunctor_obj, RightExtension.postcomp₁_obj_left_obj, RightExtension.coneAtWhiskerRightIso_inv_hom, RightExtension.precomp_obj_right, RightExtension.postcomp₁_map_left_app, PreservesPointwiseRightKanExtensionAt.preserves, RightExtension.postcomp₁_obj_right, RightExtension.postcompose₂_obj_hom_app, RightExtension.precomp_obj_hom_app, RightExtension.precomp_map_right, RightExtension.postcompose₂ObjMkIso_inv_left_app, RightExtension.postcompose₂_map_left_app, RightExtension.postcompose₂_obj_left_obj, RightExtension.postcompose₂_map_right, RightExtension.coneAtFunctor_map_hom, RightExtension.coneAtWhiskerRightIso_hom_hom, RightExtension.postcomp₁_obj_hom_app, RightExtension.postcompose₂ObjMkIso_hom_left_app, RightExtension.precomp_obj_left, instIsEquivalenceRightExtensionCompPrecomp
coconeOfIsLeftKanExtension 📖	CompOp	3 math math: isColimitCoconeOfIsLeftKanExtension_desc, coconeOfIsLeftKanExtension_ι, coconeOfIsLeftKanExtension_pt
colimitIsoOfIsLeftKanExtension 📖	CompOp	6 math math: ι_colimitIsoOfIsLeftKanExtension_inv_assoc, ι_colimitIsoOfIsLeftKanExtension_inv, lanCompColimIso_inv_app, ι_colimitIsoOfIsLeftKanExtension_hom, ι_colimitIsoOfIsLeftKanExtension_hom_assoc, lanCompColimIso_hom_app
coneOfIsRightKanExtension 📖	CompOp	3 math math: coneOfIsRightKanExtension_pt, isLimitConeOfIsRightKanExtension_lift, coneOfIsRightKanExtension_π
descOfIsLeftKanExtension 📖	CompOp	13 math math: descOfIsLeftKanExtension_fac_assoc, homEquivOfIsLeftKanExtension_symm_apply, coconeOfIsLeftKanExtension_ι, CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy_homEquiv_symm_apply, leftKanExtensionUniqueOfIso_inv, descOfIsLeftKanExtension_fac_app_assoc, descOfIsLeftKanExtension_fac, leftKanExtensionUniqueOfIso_hom, descOfIsLeftKanExtension_fac_app, lanAdjunction_counit_app, pointwiseLeftKanExtension_desc_app, leftKanExtensionUnique_inv, leftKanExtensionUnique_hom
homEquivOfIsLeftKanExtension 📖	CompOp	6 math math: CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy₂_homEquiv, homEquivOfIsLeftKanExtension_symm_apply, CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy₂'_homEquiv, CategoryTheory.MonoidalCategory.DayConvolutionUnit.corepresentableByLeft_homEquiv, CategoryTheory.MonoidalCategory.DayConvolutionUnit.corepresentableByRight_homEquiv, homEquivOfIsLeftKanExtension_apply_app
homEquivOfIsRightKanExtension 📖	CompOp	2 math math: homEquivOfIsRightKanExtension_symm_apply, homEquivOfIsRightKanExtension_apply_app
isColimitCoconeOfIsLeftKanExtension 📖	CompOp	1 math math: isColimitCoconeOfIsLeftKanExtension_desc
isLimitConeOfIsRightKanExtension 📖	CompOp	1 math math: isLimitConeOfIsRightKanExtension_lift
isUniversalOfIsLeftKanExtension 📖	CompOp	—
isUniversalOfIsRightKanExtension 📖	CompOp	—
leftExtensionEquivalenceOfIso₁ 📖	CompOp	14 math math: leftExtensionEquivalenceOfIso₁_functor_map_left, leftExtensionEquivalenceOfIso₁_functor_obj_left, leftExtensionEquivalenceOfIso₁_inverse_map_left, leftExtensionEquivalenceOfIso₁_inverse_obj_left, leftExtensionEquivalenceOfIso₁_inverse_map_right, leftExtensionEquivalenceOfIso₁_inverse_obj_right, leftExtensionEquivalenceOfIso₁_counitIso_inv_app_right_app, leftExtensionEquivalenceOfIso₁_inverse_obj_hom_app, leftExtensionEquivalenceOfIso₁_functor_obj_hom_app, leftExtensionEquivalenceOfIso₁_unitIso_hom_app_right_app, leftExtensionEquivalenceOfIso₁_counitIso_hom_app_right_app, leftExtensionEquivalenceOfIso₁_functor_map_right, leftExtensionEquivalenceOfIso₁_unitIso_inv_app_right_app, leftExtensionEquivalenceOfIso₁_functor_obj_right
leftExtensionEquivalenceOfIso₂ 📖	CompOp	—
leftKanExtension 📖	CompOp	21 math math: leftKanExtensionUnit_leftKanExtension_map_leftKanExtensionObjIsoColimit_hom, ι_leftKanExtensionObjIsoColimit_inv, leftKanExtensionCompIsoOfPreserves_hom_fac_app, ι_leftKanExtensionObjIsoColimit_inv_assoc, leftKanExtensionCompIsoOfPreserves_hom_fac_assoc, leftKanExtensionCompIsoOfPreserves_inv_fac_assoc, leftKanExtensionCompIsoOfPreserves_hom_fac_app_assoc, leftKanExtension_hom_ext_iff, leftKanExtensionCompIsoOfPreserves_inv_fac_app_assoc, leftKanExtensionCompIsoOfPreserves_hom_fac, leftKanExtensionUnit_leftKanExtensionObjIsoColimit_hom, leftKanExtensionIsoFiberwiseColimit_hom_app, leftKanExtensionCompIsoOfPreserves_inv_fac, instIsLeftKanExtensionLeftKanExtensionLeftKanExtensionUnit, ι_leftKanExtensionObjIsoColimit_hom, CategoryTheory.Presheaf.preservesColimitsOfSize_leftKanExtension, leftKanExtensionUnit_leftKanExtensionObjIsoColimit_hom_assoc, leftKanExtensionCompIsoOfPreserves_inv_fac_app, ι_leftKanExtensionObjIsoColimit_hom_assoc, CategoryTheory.Presheaf.instIsIsoFunctorLeftKanExtensionUnitOppositeTypeUliftYoneda, leftKanExtensionIsoFiberwiseColimit_inv_app
leftKanExtensionUnique 📖	CompOp	2 math math: leftKanExtensionUnique_inv, leftKanExtensionUnique_hom
leftKanExtensionUniqueOfIso 📖	CompOp	2 math math: leftKanExtensionUniqueOfIso_inv, leftKanExtensionUniqueOfIso_hom
leftKanExtensionUnit 📖	CompOp	18 math math: leftKanExtensionUnit_leftKanExtension_map_leftKanExtensionObjIsoColimit_hom, ι_leftKanExtensionObjIsoColimit_inv, leftKanExtensionCompIsoOfPreserves_hom_fac_app, ι_leftKanExtensionObjIsoColimit_inv_assoc, leftKanExtensionCompIsoOfPreserves_hom_fac_assoc, leftKanExtensionCompIsoOfPreserves_inv_fac_assoc, leftKanExtensionCompIsoOfPreserves_hom_fac_app_assoc, leftKanExtension_hom_ext_iff, leftKanExtensionCompIsoOfPreserves_inv_fac_app_assoc, leftKanExtensionCompIsoOfPreserves_hom_fac, leftKanExtensionUnit_leftKanExtensionObjIsoColimit_hom, leftKanExtensionCompIsoOfPreserves_inv_fac, instIsLeftKanExtensionLeftKanExtensionLeftKanExtensionUnit, ι_leftKanExtensionObjIsoColimit_hom, leftKanExtensionUnit_leftKanExtensionObjIsoColimit_hom_assoc, leftKanExtensionCompIsoOfPreserves_inv_fac_app, ι_leftKanExtensionObjIsoColimit_hom_assoc, CategoryTheory.Presheaf.instIsIsoFunctorLeftKanExtensionUnitOppositeTypeUliftYoneda
liftOfIsRightKanExtension 📖	CompOp	12 math math: liftOfIsRightKanExtension_fac, rightKanExtensionUniqueOfIso_hom, pointwiseRightKanExtension_lift_app, liftOfIsRightKanExtension_fac_app, liftOfIsRightKanExtension_fac_app_assoc, coneOfIsRightKanExtension_π, homEquivOfIsRightKanExtension_symm_apply, rightKanExtensionUniqueOfIso_inv, ranAdjunction_unit_app, rightKanExtensionUnique_hom, rightKanExtensionUnique_inv, liftOfIsRightKanExtension_fac_assoc
limitIsoOfIsRightKanExtension 📖	CompOp	6 math math: ranCompLimIso_inv_app, limitIsoOfIsRightKanExtension_hom_π_assoc, limitIsoOfIsRightKanExtension_inv_π_assoc, limitIsoOfIsRightKanExtension_hom_π, ranCompLimIso_hom_app, limitIsoOfIsRightKanExtension_inv_π
rightExtensionEquivalenceOfIso₁ 📖	CompOp	—
rightExtensionEquivalenceOfIso₂ 📖	CompOp	—
rightKanExtension 📖	CompOp	10 math math: rightKanExtensionCompIsoOfPreserves_inv_fac_app, rightKanExtensionCompIsoOfPreserves_hom_fac_app, rightKanExtensionCompIsoOfPreserves_hom_fac_app_assoc, instIsRightKanExtensionRightKanExtensionRightKanExtensionCounit, rightKanExtension_hom_ext_iff, rightKanExtensionCompIsoOfPreserves_hom_fac, rightKanExtensionCompIsoOfPreserves_inv_fac, rightKanExtensionCompIsoOfPreserves_hom_fac_assoc, rightKanExtensionCompIsoOfPreserves_inv_fac_app_assoc, rightKanExtensionCompIsoOfPreserves_inv_fac_assoc
rightKanExtensionCounit 📖	CompOp	10 math math: rightKanExtensionCompIsoOfPreserves_inv_fac_app, rightKanExtensionCompIsoOfPreserves_hom_fac_app, rightKanExtensionCompIsoOfPreserves_hom_fac_app_assoc, instIsRightKanExtensionRightKanExtensionRightKanExtensionCounit, rightKanExtension_hom_ext_iff, rightKanExtensionCompIsoOfPreserves_hom_fac, rightKanExtensionCompIsoOfPreserves_inv_fac, rightKanExtensionCompIsoOfPreserves_hom_fac_assoc, rightKanExtensionCompIsoOfPreserves_inv_fac_app_assoc, rightKanExtensionCompIsoOfPreserves_inv_fac_assoc
rightKanExtensionUnique 📖	CompOp	2 math math: rightKanExtensionUnique_hom, rightKanExtensionUnique_inv
rightKanExtensionUniqueOfIso 📖	CompOp	2 math math: rightKanExtensionUniqueOfIso_hom, rightKanExtensionUniqueOfIso_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coconeOfIsLeftKanExtension_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt coconeOfIsLeftKanExtension	—	—
coconeOfIsLeftKanExtension_ι 📖	mathematical	—	CategoryTheory.Limits.Cocone.ι coconeOfIsLeftKanExtension descOfIsLeftKanExtension obj CategoryTheory.Functor category const CategoryTheory.Limits.Cocone.pt	—	—
coneOfIsRightKanExtension_pt 📖	mathematical	—	CategoryTheory.Limits.Cone.pt coneOfIsRightKanExtension	—	—
coneOfIsRightKanExtension_π 📖	mathematical	—	CategoryTheory.Limits.Cone.π coneOfIsRightKanExtension liftOfIsRightKanExtension obj CategoryTheory.Functor category const CategoryTheory.Limits.Cone.pt	—	—
descOfIsLeftKanExtension_fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp whiskerLeft descOfIsLeftKanExtension	—	CategoryTheory.StructuredArrow.IsUniversal.fac
descOfIsLeftKanExtension_fac_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj comp CategoryTheory.NatTrans.app descOfIsLeftKanExtension	—	CategoryTheory.NatTrans.congr_app descOfIsLeftKanExtension_fac
descOfIsLeftKanExtension_fac_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.NatTrans.app comp descOfIsLeftKanExtension	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' descOfIsLeftKanExtension_fac_app
descOfIsLeftKanExtension_fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp whiskerLeft descOfIsLeftKanExtension	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' descOfIsLeftKanExtension_fac
hasLeftExtension_iff_of_iso₁ 📖	mathematical	—	HasLeftKanExtension	—	CategoryTheory.Equivalence.hasInitial_iff
hasLeftExtension_iff_of_iso₂ 📖	mathematical	—	HasLeftKanExtension	—	CategoryTheory.Equivalence.hasInitial_iff
hasLeftExtension_iff_postcomp₁ 📖	mathematical	—	HasLeftKanExtension	—	CategoryTheory.Equivalence.hasInitial_iff instIsEquivalenceLeftExtensionPostcomp₁OfIsIso CategoryTheory.Iso.isIso_inv
hasRightExtension_iff_of_iso₁ 📖	mathematical	—	HasRightKanExtension	—	CategoryTheory.Equivalence.hasTerminal_iff
hasRightExtension_iff_of_iso₂ 📖	mathematical	—	HasRightKanExtension	—	CategoryTheory.Equivalence.hasTerminal_iff
hasRightExtension_iff_postcomp₁ 📖	mathematical	—	HasRightKanExtension	—	CategoryTheory.Equivalence.hasTerminal_iff instIsEquivalenceRightExtensionPostcomp₁OfIsIso CategoryTheory.Iso.isIso_hom
homEquivOfIsLeftKanExtension_apply_app 📖	mathematical	—	CategoryTheory.NatTrans.app comp DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct category EquivLike.toFunLike Equiv.instEquivLike homEquivOfIsLeftKanExtension CategoryTheory.CategoryStruct.comp obj	—	—
homEquivOfIsLeftKanExtension_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct category comp EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquivOfIsLeftKanExtension descOfIsLeftKanExtension	—	—
homEquivOfIsRightKanExtension_apply_app 📖	mathematical	—	CategoryTheory.NatTrans.app comp DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct category EquivLike.toFunLike Equiv.instEquivLike homEquivOfIsRightKanExtension CategoryTheory.CategoryStruct.comp obj	—	—
homEquivOfIsRightKanExtension_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct category comp EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquivOfIsRightKanExtension liftOfIsRightKanExtension	—	—
hom_ext_of_isLeftKanExtension 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp whiskerLeft	—	—	CategoryTheory.StructuredArrow.IsUniversal.hom_ext
hom_ext_of_isRightKanExtension 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp whiskerLeft	—	—	CategoryTheory.CostructuredArrow.IsUniversal.hom_ext
instIsEquivalenceLeftExtensionCompPrecomp 📖	mathematical	—	IsEquivalence LeftExtension CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor category obj whiskeringLeft comp LeftExtension.precomp	—	CategoryTheory.StructuredArrow.isEquivalenceMap₂ isEquivalence_refl IsEquivalence.faithful instIsEquivalenceObjWhiskeringLeft IsEquivalence.full CategoryTheory.IsIso.id
instIsEquivalenceLeftExtensionPostcomp₁OfIsIso 📖	mathematical	—	IsEquivalence LeftExtension CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor category obj whiskeringLeft LeftExtension.postcomp₁	—	CategoryTheory.StructuredArrow.isEquivalenceMap₂ instIsEquivalenceObjWhiskeringLeft Faithful.id Full.id CategoryTheory.IsIso.id map_isIso
instIsEquivalenceRightExtensionCompPrecomp 📖	mathematical	—	IsEquivalence RightExtension CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor category obj whiskeringLeft comp RightExtension.precomp	—	CategoryTheory.CostructuredArrow.isEquivalenceMap₂ isEquivalence_refl IsEquivalence.faithful instIsEquivalenceObjWhiskeringLeft IsEquivalence.full CategoryTheory.IsIso.id
instIsEquivalenceRightExtensionPostcomp₁OfIsIso 📖	mathematical	—	IsEquivalence RightExtension CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor category obj whiskeringLeft RightExtension.postcomp₁	—	CategoryTheory.CostructuredArrow.isEquivalenceMap₂ instIsEquivalenceObjWhiskeringLeft Faithful.id Full.id map_isIso CategoryTheory.IsIso.id
instIsLeftKanExtensionLeftKanExtensionLeftKanExtensionUnit 📖	mathematical	—	IsLeftKanExtension leftKanExtension leftKanExtensionUnit	—	—
instIsRightKanExtensionRightKanExtensionRightKanExtensionCounit 📖	mathematical	—	IsRightKanExtension rightKanExtension rightKanExtensionCounit	—	—
isColimitCoconeOfIsLeftKanExtension_desc 📖	mathematical	—	CategoryTheory.Limits.IsColimit.desc coconeOfIsLeftKanExtension isColimitCoconeOfIsLeftKanExtension CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp obj const whiskerLeft CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι	—	—
isLeftKanExtensionAlongEquivalence 📖	mathematical	—	IsLeftKanExtension CategoryTheory.Equivalence.functor CategoryTheory.Iso.hom CategoryTheory.Functor category comp	—	CategoryTheory.Equivalence.isEquivalence_functor CategoryTheory.NatTrans.ext' LeftExtension.postcomp₁_obj_hom_app map_id CategoryTheory.Category.comp_id CategoryTheory.Iso.hom_inv_id_app_assoc CategoryTheory.StructuredArrow.hom_ext CategoryTheory.Iso.inv_hom_id_app_assoc CategoryTheory.Discrete.functor_map_id CategoryTheory.Category.id_comp CategoryTheory.whisker_eq CategoryTheory.congr_app CategoryTheory.CommaMorphism.w
isLeftKanExtensionAlongEquivalence' 📖	mathematical	—	IsLeftKanExtension	—	isLeftKanExtensionAlongEquivalence
isLeftKanExtensionId 📖	mathematical	—	IsLeftKanExtension id CategoryTheory.Iso.inv CategoryTheory.Functor category comp leftUnitor	—	IsEquivalence.full instIsEquivalenceObjWhiskeringLeft isEquivalence_refl IsEquivalence.faithful
isLeftKanExtension_iff_isIso 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp whiskerLeft	IsLeftKanExtension CategoryTheory.IsIso	—	hom_ext_of_isLeftKanExtension leftKanExtensionUnique_hom descOfIsLeftKanExtension_fac CategoryTheory.Iso.isIso_hom isLeftKanExtension_of_iso
isLeftKanExtension_iff_of_iso 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp whiskerLeft CategoryTheory.Iso.hom	IsLeftKanExtension	—	isLeftKanExtension_of_iso CategoryTheory.Category.assoc whiskerLeft_comp CategoryTheory.Iso.symm_hom CategoryTheory.Iso.hom_inv_id whiskerLeft_id' CategoryTheory.Category.comp_id
isLeftKanExtension_iff_of_iso₂ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp whiskerLeft CategoryTheory.Iso.hom	IsLeftKanExtension	—	—
isLeftKanExtension_iff_postcompose 📖	mathematical	Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct category comp CategoryTheory.CategoryStruct.comp whiskerLeft CategoryTheory.Iso.inv associator whiskerRight CategoryTheory.Iso.hom	IsLeftKanExtension	—	CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit instPreservesColimitsOfShapeOfIsLeftAdjoint isLeftAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.CreatesColimit.toReflectsColimit CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.NatTrans.ext' LeftExtension.precomp₂_obj_hom_app CategoryTheory.congr_app CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_app map_id CategoryTheory.Equivalence.isEquivalence_functor
isLeftKanExtension_iff_postcomp₁ 📖	mathematical	—	IsLeftKanExtension comp CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category whiskerRight CategoryTheory.Iso.inv CategoryTheory.Iso.hom associator	—	CategoryTheory.Category.comp_id CategoryTheory.NatTrans.ext' LeftExtension.postcomp₁_obj_hom_app
isLeftKanExtension_iff_precomp 📖	mathematical	—	IsLeftKanExtension comp CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category whiskerLeft CategoryTheory.Iso.inv associator	—	CategoryTheory.Category.comp_id CategoryTheory.NatTrans.ext' LeftExtension.precomp_obj_hom_app
isLeftKanExtension_of_iso 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp whiskerLeft CategoryTheory.Iso.hom	IsLeftKanExtension	—	—
isLimitConeOfIsRightKanExtension_lift 📖	mathematical	—	CategoryTheory.Limits.IsLimit.lift coneOfIsRightKanExtension isLimitConeOfIsRightKanExtension CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category obj const comp whiskerLeft CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.Cone.π	—	—
isRightKanExtensionAlongEquivalence 📖	mathematical	—	IsRightKanExtension CategoryTheory.Equivalence.functor CategoryTheory.Iso.hom CategoryTheory.Functor category comp	—	CategoryTheory.Equivalence.isEquivalence_functor CategoryTheory.Category.assoc CategoryTheory.NatTrans.ext' RightExtension.postcomp₁_obj_hom_app map_id CategoryTheory.Category.id_comp CategoryTheory.Iso.inv_hom_id_app CategoryTheory.Category.comp_id CategoryTheory.CostructuredArrow.hom_ext CategoryTheory.Iso.hom_inv_id_app CategoryTheory.Discrete.functor_map_id CategoryTheory.eq_whisker CategoryTheory.congr_app CategoryTheory.CommaMorphism.w
isRightKanExtensionAlongEquivalence' 📖	mathematical	—	IsRightKanExtension	—	isRightKanExtensionAlongEquivalence
isRightKanExtensionId 📖	mathematical	—	IsRightKanExtension id CategoryTheory.Iso.hom CategoryTheory.Functor category comp leftUnitor	—	IsEquivalence.full instIsEquivalenceObjWhiskeringLeft isEquivalence_refl IsEquivalence.faithful
isRightKanExtension_iff_isIso 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp whiskerLeft	IsRightKanExtension CategoryTheory.IsIso	—	hom_ext_of_isRightKanExtension rightKanExtensionUnique_hom liftOfIsRightKanExtension_fac CategoryTheory.Iso.isIso_hom isRightKanExtension_iff_of_iso
isRightKanExtension_iff_of_iso 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp whiskerLeft CategoryTheory.Iso.hom	IsRightKanExtension	—	isRightKanExtension_of_iso whiskerLeft_comp_assoc CategoryTheory.Iso.symm_hom CategoryTheory.Iso.inv_hom_id whiskerLeft_id' CategoryTheory.Category.id_comp
isRightKanExtension_iff_of_iso₂ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp whiskerLeft CategoryTheory.Iso.hom	IsRightKanExtension	—	—
isRightKanExtension_iff_postcomp₁ 📖	mathematical	—	IsRightKanExtension comp CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category CategoryTheory.Iso.inv associator whiskerRight CategoryTheory.Iso.hom	—	CategoryTheory.Category.id_comp CategoryTheory.NatTrans.ext' RightExtension.postcomp₁_obj_hom_app
isRightKanExtension_iff_precomp 📖	mathematical	—	IsRightKanExtension comp CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category CategoryTheory.Iso.hom associator whiskerLeft	—	CategoryTheory.Category.id_comp CategoryTheory.NatTrans.ext' RightExtension.precomp_obj_hom_app
isRightKanExtension_of_iso 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp whiskerLeft CategoryTheory.Iso.hom	IsRightKanExtension	—	—
leftExtensionEquivalenceOfIso₁_counitIso_hom_app_right_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor category fromPUnit obj whiskeringLeft CategoryTheory.Comma CategoryTheory.commaCategory comp CategoryTheory.Comma.mapRight CategoryTheory.Iso.inv mapIso CategoryTheory.Iso.hom id CategoryTheory.CommaMorphism.right CategoryTheory.Equivalence.counitIso LeftExtension CategoryTheory.instCategoryStructuredArrow leftExtensionEquivalenceOfIso₁ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Category.comp_id
leftExtensionEquivalenceOfIso₁_counitIso_inv_app_right_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor category fromPUnit obj whiskeringLeft CategoryTheory.Comma CategoryTheory.commaCategory id comp CategoryTheory.Comma.mapRight CategoryTheory.Iso.inv mapIso CategoryTheory.Iso.hom CategoryTheory.CommaMorphism.right CategoryTheory.Equivalence.counitIso LeftExtension CategoryTheory.instCategoryStructuredArrow leftExtensionEquivalenceOfIso₁ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Category.comp_id
leftExtensionEquivalenceOfIso₁_functor_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor category fromPUnit obj whiskeringLeft CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom CategoryTheory.NatTrans.app CategoryTheory.Iso.hom mapIso map CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor LeftExtension CategoryTheory.instCategoryStructuredArrow leftExtensionEquivalenceOfIso₁ CategoryTheory.CategoryStruct.id	—	—
leftExtensionEquivalenceOfIso₁_functor_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor category fromPUnit obj whiskeringLeft CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom CategoryTheory.NatTrans.app CategoryTheory.Iso.hom mapIso map CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor LeftExtension CategoryTheory.instCategoryStructuredArrow leftExtensionEquivalenceOfIso₁	—	—
leftExtensionEquivalenceOfIso₁_functor_obj_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor category fromPUnit CategoryTheory.Comma.left whiskeringLeft CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor LeftExtension CategoryTheory.instCategoryStructuredArrow leftExtensionEquivalenceOfIso₁ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct comp map CategoryTheory.Iso.hom	—	—
leftExtensionEquivalenceOfIso₁_functor_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor category fromPUnit obj whiskeringLeft CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor LeftExtension CategoryTheory.instCategoryStructuredArrow leftExtensionEquivalenceOfIso₁	—	—
leftExtensionEquivalenceOfIso₁_functor_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor category fromPUnit obj whiskeringLeft CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.functor LeftExtension CategoryTheory.instCategoryStructuredArrow leftExtensionEquivalenceOfIso₁	—	—
leftExtensionEquivalenceOfIso₁_inverse_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor category fromPUnit obj whiskeringLeft CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom CategoryTheory.NatTrans.app CategoryTheory.Iso.inv mapIso map CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse LeftExtension CategoryTheory.instCategoryStructuredArrow leftExtensionEquivalenceOfIso₁ CategoryTheory.CategoryStruct.id	—	—
leftExtensionEquivalenceOfIso₁_inverse_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor category fromPUnit obj whiskeringLeft CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom CategoryTheory.NatTrans.app CategoryTheory.Iso.inv mapIso map CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse LeftExtension CategoryTheory.instCategoryStructuredArrow leftExtensionEquivalenceOfIso₁	—	—
leftExtensionEquivalenceOfIso₁_inverse_obj_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor category fromPUnit CategoryTheory.Comma.left whiskeringLeft CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse LeftExtension CategoryTheory.instCategoryStructuredArrow leftExtensionEquivalenceOfIso₁ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct comp map CategoryTheory.Iso.inv	—	—
leftExtensionEquivalenceOfIso₁_inverse_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor category fromPUnit obj whiskeringLeft CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse LeftExtension CategoryTheory.instCategoryStructuredArrow leftExtensionEquivalenceOfIso₁	—	—
leftExtensionEquivalenceOfIso₁_inverse_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor category fromPUnit obj whiskeringLeft CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Equivalence.inverse LeftExtension CategoryTheory.instCategoryStructuredArrow leftExtensionEquivalenceOfIso₁	—	—
leftExtensionEquivalenceOfIso₁_unitIso_hom_app_right_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor category fromPUnit obj whiskeringLeft CategoryTheory.Comma CategoryTheory.commaCategory id comp CategoryTheory.Comma.mapRight CategoryTheory.Iso.hom mapIso CategoryTheory.Iso.inv CategoryTheory.CommaMorphism.right CategoryTheory.Equivalence.unitIso LeftExtension CategoryTheory.instCategoryStructuredArrow leftExtensionEquivalenceOfIso₁ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Category.comp_id
leftExtensionEquivalenceOfIso₁_unitIso_inv_app_right_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor category fromPUnit obj whiskeringLeft CategoryTheory.Comma CategoryTheory.commaCategory comp CategoryTheory.Comma.mapRight CategoryTheory.Iso.hom mapIso CategoryTheory.Iso.inv id CategoryTheory.CommaMorphism.right CategoryTheory.Equivalence.unitIso LeftExtension CategoryTheory.instCategoryStructuredArrow leftExtensionEquivalenceOfIso₁ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Category.comp_id
leftKanExtensionUniqueOfIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor category leftKanExtensionUniqueOfIso descOfIsLeftKanExtension CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct comp	—	—
leftKanExtensionUniqueOfIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor category leftKanExtensionUniqueOfIso descOfIsLeftKanExtension CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct comp	—	—
leftKanExtensionUnique_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor category leftKanExtensionUnique descOfIsLeftKanExtension	—	descOfIsLeftKanExtension.congr_simp CategoryTheory.Category.id_comp
leftKanExtensionUnique_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor category leftKanExtensionUnique descOfIsLeftKanExtension	—	descOfIsLeftKanExtension.congr_simp CategoryTheory.Category.id_comp
leftKanExtension_hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp leftKanExtension leftKanExtensionUnit whiskerLeft	—	—	hom_ext_of_isLeftKanExtension instIsLeftKanExtensionLeftKanExtensionLeftKanExtensionUnit
leftKanExtension_hom_ext_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp leftKanExtension leftKanExtensionUnit whiskerLeft	—	leftKanExtension_hom_ext
liftOfIsRightKanExtension_fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp whiskerLeft liftOfIsRightKanExtension	—	CategoryTheory.CostructuredArrow.IsUniversal.fac
liftOfIsRightKanExtension_fac_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.NatTrans.app liftOfIsRightKanExtension comp	—	CategoryTheory.NatTrans.congr_app liftOfIsRightKanExtension_fac
liftOfIsRightKanExtension_fac_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.NatTrans.app liftOfIsRightKanExtension comp	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' liftOfIsRightKanExtension_fac_app
liftOfIsRightKanExtension_fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp whiskerLeft liftOfIsRightKanExtension	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' liftOfIsRightKanExtension_fac
limitIsoOfIsRightKanExtension_hom_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.limit obj CategoryTheory.Iso.hom limitIsoOfIsRightKanExtension CategoryTheory.Limits.limit.π CategoryTheory.NatTrans.app comp	—	CategoryTheory.Iso.eq_inv_comp limitIsoOfIsRightKanExtension_inv_π
limitIsoOfIsRightKanExtension_hom_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.limit CategoryTheory.Iso.hom limitIsoOfIsRightKanExtension obj CategoryTheory.Limits.limit.π CategoryTheory.NatTrans.app comp	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' limitIsoOfIsRightKanExtension_hom_π
limitIsoOfIsRightKanExtension_inv_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.limit obj CategoryTheory.Iso.inv limitIsoOfIsRightKanExtension CategoryTheory.Limits.limit.π CategoryTheory.NatTrans.app comp	—	CategoryTheory.Limits.limit.conePointUniqueUpToIso_inv_comp_assoc liftOfIsRightKanExtension_fac_app
limitIsoOfIsRightKanExtension_inv_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.limit CategoryTheory.Iso.inv limitIsoOfIsRightKanExtension obj CategoryTheory.Limits.limit.π CategoryTheory.NatTrans.app comp	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' limitIsoOfIsRightKanExtension_inv_π
rightKanExtensionUniqueOfIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor category rightKanExtensionUniqueOfIso liftOfIsRightKanExtension CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct comp	—	—
rightKanExtensionUniqueOfIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor category rightKanExtensionUniqueOfIso liftOfIsRightKanExtension CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct comp	—	—
rightKanExtensionUnique_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor category rightKanExtensionUnique liftOfIsRightKanExtension	—	liftOfIsRightKanExtension.congr_simp CategoryTheory.Category.comp_id
rightKanExtensionUnique_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor category rightKanExtensionUnique liftOfIsRightKanExtension	—	liftOfIsRightKanExtension.congr_simp CategoryTheory.Category.comp_id
rightKanExtension_hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp rightKanExtension whiskerLeft rightKanExtensionCounit	—	—	hom_ext_of_isRightKanExtension instIsRightKanExtensionRightKanExtensionRightKanExtensionCounit
rightKanExtension_hom_ext_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp rightKanExtension whiskerLeft rightKanExtensionCounit	—	rightKanExtension_hom_ext
ι_colimitIsoOfIsLeftKanExtension_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj comp CategoryTheory.Limits.colimit CategoryTheory.NatTrans.app CategoryTheory.Limits.colimit.ι CategoryTheory.Iso.hom colimitIsoOfIsLeftKanExtension	—	CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom descOfIsLeftKanExtension_fac_app
ι_colimitIsoOfIsLeftKanExtension_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.NatTrans.app comp CategoryTheory.Limits.colimit CategoryTheory.Limits.colimit.ι CategoryTheory.Iso.hom colimitIsoOfIsLeftKanExtension	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_colimitIsoOfIsLeftKanExtension_hom
ι_colimitIsoOfIsLeftKanExtension_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Limits.colimit CategoryTheory.Limits.colimit.ι CategoryTheory.Iso.inv colimitIsoOfIsLeftKanExtension comp CategoryTheory.NatTrans.app	—	CategoryTheory.Iso.comp_inv_eq CategoryTheory.Category.assoc ι_colimitIsoOfIsLeftKanExtension_hom
ι_colimitIsoOfIsLeftKanExtension_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Limits.colimit CategoryTheory.Limits.colimit.ι CategoryTheory.Iso.inv colimitIsoOfIsLeftKanExtension CategoryTheory.NatTrans.app comp	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_colimitIsoOfIsLeftKanExtension_inv

CategoryTheory.Functor.HasLeftKanExtension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk 📖	mathematical	—	CategoryTheory.Functor.HasLeftKanExtension	—	CategoryTheory.Limits.IsInitial.hasInitial

CategoryTheory.Functor.HasRightKanExtension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk 📖	mathematical	—	CategoryTheory.Functor.HasRightKanExtension	—	CategoryTheory.Limits.IsTerminal.hasTerminal

CategoryTheory.Functor.IsLeftKanExtension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonempty_isUniversal 📖	mathematical	—	CategoryTheory.StructuredArrow.IsUniversal CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft	—	—

CategoryTheory.Functor.IsRightKanExtension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonempty_isUniversal 📖	mathematical	—	CategoryTheory.CostructuredArrow.IsUniversal CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft	—	—

CategoryTheory.Functor.LeftExtension

Definitions

Name	Category	Theorems
isUniversalEquivOfIso₂ 📖	CompOp	—
isUniversalOfPrecomp₂ 📖	CompOp	—
isUniversalPostcomp₁Equiv 📖	CompOp	—
isUniversalPrecompEquiv 📖	CompOp	—
isUniversalPrecomp₂ 📖	CompOp	—
isUniversalPrecomp₂Equiv 📖	CompOp	—
mk 📖	CompOp	—
postcompose₂ 📖	CompOp	11 math math: coconeAtWhiskerRightIso_inv_hom, postcompose₂_obj_right_map, postcompose₂ObjMkIso_inv_right_app, postcompose₂_map_right_app, postcompose₂_obj_hom_app, postcompose₂_obj_right_obj, postcompose₂ObjMkIso_hom_right_app, CategoryTheory.Functor.PreservesPointwiseLeftKanExtensionAt.preserves, coconeAtWhiskerRightIso_hom_hom, postcompose₂_obj_left, postcompose₂_map_left
postcompose₂ObjMkIso 📖	CompOp	2 math math: postcompose₂ObjMkIso_inv_right_app, postcompose₂ObjMkIso_hom_right_app
postcomp₁ 📖	CompOp	7 math math: postcomp₁_map_right_app, postcomp₁_obj_left, CategoryTheory.Functor.instIsEquivalenceLeftExtensionPostcomp₁OfIsIso, postcomp₁_obj_hom_app, postcomp₁_obj_right_map, postcomp₁_obj_right_obj, postcomp₁_map_left
precomp 📖	CompOp	9 math math: precomp₂_obj_hom_app, precomp₂_map_right, precomp_map_right, precomp_obj_hom_app, CategoryTheory.Functor.instIsEquivalenceLeftExtensionCompPrecomp, precomp_obj_right, precomp_obj_left, precomp_map_left, precomp₂_map_left
precomp₂ 📖	CompOp	5 math math: precomp₂_obj_hom_app, precomp₂_map_right, precomp₂_obj_left, precomp₂_obj_right, precomp₂_map_left

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft	—	—
mk_left_as 📖	mathematical	—	CategoryTheory.Discrete.as CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft	—	—
mk_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft	—	—
postcompose₂ObjMkIso_hom_right_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow postcompose₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.hom CategoryTheory.Functor.associator CategoryTheory.CommaMorphism.right postcompose₂ObjMkIso CategoryTheory.CategoryStruct.id	—	—
postcompose₂ObjMkIso_inv_right_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.hom CategoryTheory.Functor.associator CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow postcompose₂ CategoryTheory.CommaMorphism.right CategoryTheory.Iso.inv postcompose₂ObjMkIso CategoryTheory.CategoryStruct.id	—	—
postcompose₂_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Functor.whiskeringRight CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Discrete.natTrans CategoryTheory.CategoryStruct.id CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.Iso.hom CategoryTheory.Functor.associator CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow postcompose₂	—	—
postcompose₂_map_right_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringRight CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.whiskeringLeft CategoryTheory.CommaMorphism.right CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Discrete.natTrans CategoryTheory.CategoryStruct.id CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.Iso.hom CategoryTheory.Functor.associator CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow postcompose₂	—	—
postcompose₂_obj_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.whiskeringRight CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow postcompose₂ CategoryTheory.Functor.map	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
postcompose₂_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow postcompose₂	—	—
postcompose₂_obj_right_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow postcompose₂	—	—
postcompose₂_obj_right_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow postcompose₂	—	—
postcomp₁_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Discrete.natTrans CategoryTheory.CategoryStruct.id CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow postcomp₁	—	—
postcomp₁_map_right_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.Discrete.natTrans CategoryTheory.CategoryStruct.id CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow postcomp₁	—	—
postcomp₁_obj_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Functor.whiskeringLeft CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow postcomp₁ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.Functor.map	—	CategoryTheory.Category.id_comp
postcomp₁_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow postcomp₁	—	—
postcomp₁_obj_right_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow postcomp₁	—	—
postcomp₁_obj_right_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow postcomp₁	—	—
precomp_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Discrete.natTrans CategoryTheory.CategoryStruct.id CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow precomp	—	—
precomp_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Discrete.natTrans CategoryTheory.CategoryStruct.id CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow precomp	—	—
precomp_obj_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Functor.whiskeringLeft CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow precomp	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
precomp_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow precomp	—	—
precomp_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow precomp	—	—
precomp₂_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.comp CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow CategoryTheory.StructuredArrow.map precomp CategoryTheory.Functor.map precomp₂ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	—
precomp₂_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.comp CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow CategoryTheory.StructuredArrow.map precomp CategoryTheory.Functor.map precomp₂	—	—
precomp₂_obj_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.comp CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow precomp CategoryTheory.Comma.right CategoryTheory.Comma.hom precomp₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	precomp_obj_hom_app
precomp₂_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.comp CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow precomp₂	—	—
precomp₂_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.comp CategoryTheory.Functor.LeftExtension CategoryTheory.instCategoryStructuredArrow precomp₂	—	—

CategoryTheory.Functor.RightExtension

Definitions

Name	Category	Theorems
isUniversalEquivOfIso₂ 📖	CompOp	—
isUniversalPostcomp₁Equiv 📖	CompOp	—
isUniversalPrecompEquiv 📖	CompOp	—
mk 📖	CompOp	—
postcompose₂ 📖	CompOp	11 math math: postcompose₂_obj_left_map, postcompose₂_obj_right, coneAtWhiskerRightIso_inv_hom, CategoryTheory.Functor.PreservesPointwiseRightKanExtensionAt.preserves, postcompose₂_obj_hom_app, postcompose₂ObjMkIso_inv_left_app, postcompose₂_map_left_app, postcompose₂_obj_left_obj, postcompose₂_map_right, coneAtWhiskerRightIso_hom_hom, postcompose₂ObjMkIso_hom_left_app
postcompose₂ObjMkIso 📖	CompOp	2 math math: postcompose₂ObjMkIso_inv_left_app, postcompose₂ObjMkIso_hom_left_app
postcomp₁ 📖	CompOp	7 math math: postcomp₁_obj_left_map, postcomp₁_map_right, CategoryTheory.Functor.instIsEquivalenceRightExtensionPostcomp₁OfIsIso, postcomp₁_obj_left_obj, postcomp₁_map_left_app, postcomp₁_obj_right, postcomp₁_obj_hom_app
precomp 📖	CompOp	6 math math: precomp_map_left, precomp_obj_right, precomp_obj_hom_app, precomp_map_right, precomp_obj_left, CategoryTheory.Functor.instIsEquivalenceRightExtensionCompPrecomp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.fromPUnit	—	—
mk_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.fromPUnit	—	—
mk_right_as 📖	mathematical	—	CategoryTheory.Discrete.as CategoryTheory.Comma.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.fromPUnit	—	—
postcompose₂ObjMkIso_hom_left_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.Functor.RightExtension CategoryTheory.instCategoryCostructuredArrow postcompose₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv CategoryTheory.Functor.associator CategoryTheory.Functor.whiskerRight CategoryTheory.CommaMorphism.left CategoryTheory.Iso.hom postcompose₂ObjMkIso CategoryTheory.CategoryStruct.id	—	—
postcompose₂ObjMkIso_inv_left_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv CategoryTheory.Functor.associator CategoryTheory.Functor.whiskerRight CategoryTheory.Functor.RightExtension CategoryTheory.instCategoryCostructuredArrow postcompose₂ CategoryTheory.CommaMorphism.left postcompose₂ObjMkIso CategoryTheory.CategoryStruct.id	—	—
postcompose₂_map_left_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringRight CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.fromPUnit CategoryTheory.CommaMorphism.left CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv CategoryTheory.Functor.associator CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.Discrete.natTrans CategoryTheory.CategoryStruct.id CategoryTheory.Functor.RightExtension CategoryTheory.instCategoryCostructuredArrow postcompose₂	—	—
postcompose₂_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.Functor.whiskeringRight CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor.associator CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.Discrete.natTrans CategoryTheory.CategoryStruct.id CategoryTheory.Functor.RightExtension CategoryTheory.instCategoryCostructuredArrow postcompose₂	—	—
postcompose₂_obj_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.whiskeringRight CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.RightExtension CategoryTheory.instCategoryCostructuredArrow postcompose₂ CategoryTheory.Functor.map	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
postcompose₂_obj_left_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.Functor.RightExtension CategoryTheory.instCategoryCostructuredArrow postcompose₂	—	—
postcompose₂_obj_left_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.Functor.RightExtension CategoryTheory.instCategoryCostructuredArrow postcompose₂	—	—
postcompose₂_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.comp CategoryTheory.Functor.RightExtension CategoryTheory.instCategoryCostructuredArrow postcompose₂	—	—
postcomp₁_map_left_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.Discrete.natTrans CategoryTheory.CategoryStruct.id CategoryTheory.Functor.RightExtension CategoryTheory.instCategoryCostructuredArrow postcomp₁	—	—
postcomp₁_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.Discrete.natTrans CategoryTheory.CategoryStruct.id CategoryTheory.Functor.RightExtension CategoryTheory.instCategoryCostructuredArrow postcomp₁	—	—
postcomp₁_obj_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.RightExtension CategoryTheory.instCategoryCostructuredArrow postcomp₁ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map CategoryTheory.Functor.comp	—	CategoryTheory.Category.comp_id
postcomp₁_obj_left_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.RightExtension CategoryTheory.instCategoryCostructuredArrow postcomp₁	—	—
postcomp₁_obj_left_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.RightExtension CategoryTheory.instCategoryCostructuredArrow postcomp₁	—	—
postcomp₁_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.RightExtension CategoryTheory.instCategoryCostructuredArrow postcomp₁	—	—
precomp_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.comp CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.CategoryStruct.id CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.Discrete.natTrans CategoryTheory.Functor.RightExtension CategoryTheory.instCategoryCostructuredArrow precomp	—	—
precomp_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.comp CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.CategoryStruct.id CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.Discrete.natTrans CategoryTheory.Functor.RightExtension CategoryTheory.instCategoryCostructuredArrow precomp	—	—
precomp_obj_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.RightExtension CategoryTheory.instCategoryCostructuredArrow precomp	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
precomp_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.comp CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.RightExtension CategoryTheory.instCategoryCostructuredArrow precomp	—	—
precomp_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.comp CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.RightExtension CategoryTheory.instCategoryCostructuredArrow precomp	—	—

---

← Back to Index