Equivalence

📁 Source: Mathlib/CategoryTheory/Equivalence.lean

Statistics

Metric	Count
Definitions adjointifyη, asNatTrans, changeFunctor, changeInverse, congrLeft, congrRight, congrRightFunctor, counit, counitInv, counitIso, fullyFaithfulFunctor, fullyFaithfulInverse, funInvIdAssoc, functor, functorFunctor, instCategory, instInhabited, instPowInt, invFunIdAssoc, inverse, mk, mkHom, mkIso, pow, powNat, refl, trans, unit, unitInv, unitIso, IsEquivalence, asEquivalence, inv, compInverseIso, inverseCompIso, isoCompInverse, isoFunctorOfIsoInverse, isoInverseComp, isoInverseOfIsoFunctor, fullSubcategoryCongr, «term_≌_»	41
Theorems Equivalence_mk'_counit, Equivalence_mk'_counitInv, Equivalence_mk'_unit, Equivalence_mk'_unitInv, adjointify_η_ε, adjointify_η_ε_assoc, asNatTrans_mkHom, cancel_counitInv_right, cancel_counitInv_right_assoc, cancel_counitInv_right_assoc', cancel_counit_right, cancel_unitInv_right, cancel_unit_right, cancel_unit_right_assoc, cancel_unit_right_assoc', changeFunctor_counitIso_hom_app, changeFunctor_counitIso_inv_app, changeFunctor_functor, changeFunctor_inverse, changeFunctor_refl, changeFunctor_trans, changeFunctor_unitIso_hom_app, changeFunctor_unitIso_inv_app, changeInverse_counitIso_hom_app, changeInverse_counitIso_inv_app, changeInverse_functor, changeInverse_inverse, changeInverse_unitIso_hom_app, changeInverse_unitIso_inv_app, comp_asNatTrans, comp_asNatTrans_assoc, congrLeft_counitIso_hom_app, congrLeft_counitIso_inv_app, congrLeft_functor, congrLeft_inverse, congrLeft_unitIso_hom_app, congrLeft_unitIso_inv_app, congrRightFunctor_map, congrRightFunctor_obj, congrRight_counitIso_hom_app, congrRight_counitIso_inv_app, congrRight_functor, congrRight_inverse, congrRight_unitIso_hom_app, congrRight_unitIso_inv_app, counitInv_app_functor, counitInv_functor_comp, counitInv_functor_comp_assoc, counitInv_naturality, counitInv_naturality_assoc, counit_app_functor, counit_naturality, counit_naturality_assoc, essSurjInducedFunctor, essSurj_functor, essSurj_inverse, ext, ext_iff, faithful_functor, faithful_inverse, full_functor, full_inverse, fullyFaithfulToEssImage, funInvIdAssoc_hom_app, funInvIdAssoc_inv_app, fun_inv_map, fun_inv_map_assoc, functorFunctor_map, functorFunctor_obj, functor_unitIso_comp, functor_unit_comp, functor_unit_comp_assoc, hom_ext, hom_ext_iff, id_asNatTrans, inducedFunctorOfEquiv, invFunIdAssoc_hom_app, invFunIdAssoc_inv_app, inv_fun_map, inv_fun_map_assoc, inverse_counitInv_comp, inverse_counitInv_comp_assoc, isEquivalence_functor, isEquivalence_inverse, mkHom_asNatTrans, mkHom_comp, mkHom_comp_assoc, mkHom_id_functor, mkHom_id_inverse, mkIso_hom, mkIso_inv, pow_neg_one, pow_one, pow_zero, refl_counitIso, refl_functor, refl_inverse, refl_unitIso, symm_counit, symm_counitIso, symm_functor, symm_inverse, symm_unit, symm_unitIso, trans_counitIso, trans_functor, trans_inverse, trans_unitIso, unitInv_app_inverse, unitInv_naturality, unitInv_naturality_assoc, unit_app_inverse, unit_inverse_comp, unit_inverse_comp_assoc, unit_naturality, unit_naturality_assoc, essSurj, faithful, full, mk', asEquivalence_functor, fun_inv_map, instIsEquivalenceObjWhiskeringLeft, instIsEquivalenceObjWhiskeringRight, inv_fun_map, isEquivalence_iff_of_iso, isEquivalence_inv, isEquivalence_of_comp_left, isEquivalence_of_comp_right, isEquivalence_of_iso, isEquivalence_refl, isEquivalence_trans, compInverseIso_hom_app, compInverseIso_inv_app, inverseCompIso_hom_app, inverseCompIso_inv_app, isoCompInverse_hom_app, isoCompInverse_inv_app, isoFunctorOfIsoInverse_hom_app, isoFunctorOfIsoInverse_inv_app, isoFunctorOfIsoInverse_isoInverseOfIsoFunctor, isoInverseComp_hom_app, isoInverseComp_inv_app, isoInverseOfIsoFunctor_hom_app, isoInverseOfIsoFunctor_inv_app, isoInverseOfIsoFunctor_isoFunctorOfIsoInverse, fullSubcategoryCongr_counitIso, fullSubcategoryCongr_functor, fullSubcategoryCongr_inverse, fullSubcategoryCongr_unitIso	150
Total	191

CategoryTheory

Definitions

Name	Category	Theorems
«term_≌_» 📖	CompOp	—

CategoryTheory.Equivalence

Definitions

Name	Category	Theorems
adjointifyη 📖	CompOp	2 math math: adjointify_η_ε_assoc, adjointify_η_ε
asNatTrans 📖	CompOp	12 math math: comp_asNatTrans, inverseFunctor_map, symmEquivFunctor_map, congrLeftFunctor_map, comp_asNatTrans_assoc, mkHom_asNatTrans, id_asNatTrans, functorFunctor_map, hom_ext_iff, asNatTrans_mkHom, congrRightFunctor_map, symmEquivInverse_map_app
changeFunctor 📖	CompOp	8 math math: changeFunctor_unitIso_hom_app, changeFunctor_trans, changeFunctor_counitIso_hom_app, changeFunctor_refl, changeFunctor_unitIso_inv_app, changeFunctor_functor, changeFunctor_inverse, changeFunctor_counitIso_inv_app
changeInverse 📖	CompOp	6 math math: changeInverse_functor, changeInverse_inverse, changeInverse_counitIso_inv_app, changeInverse_unitIso_inv_app, changeInverse_counitIso_hom_app, changeInverse_unitIso_hom_app
congrLeft 📖	CompOp	37 math math: CategoryTheory.ComposableArrows.opEquivalence_counitIso_inv_app_app, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_snd_fst, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_map_app, CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_inv_app_fst, congrLeft_counitIso_inv_app, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_snd_snd, CategoryTheory.ComposableArrows.opEquivalence_unitIso_inv_app, CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_hom_app_snd, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_snd_snd, congrLeft_functor, CategoryTheory.instIsMonoidalFunctorCongrLeft, CategoryTheory.ComposableArrows.opEquivalence_functor_map_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_left_app, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_fst, CategoryTheory.ComposableArrows.opEquivalence_unitIso_hom_app, congrLeftFunctor_obj, CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitorCorepresentingIso_hom_app_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_left_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_right, congrLeft_unitIso_inv_app, congrLeft_unitIso_hom_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_left_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_hom_app, congrLeftFunctor_map, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_hom_app_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_inv_app_app, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_snd_fst, CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_hom_app_fst, CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitorCorepresentingIso_hom_app_app, CategoryTheory.MonoidalCategory.DayConvolution.associatorCorepresentingIso_hom_app_app, CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_inv_app_snd, congrLeft_counitIso_hom_app, congrLeft_inverse, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_fst, CategoryTheory.ComposableArrows.opEquivalence_counitIso_hom_app_app
congrRight 📖	CompOp	12 math math: congrRight_functor, CategoryTheory.prod.prodFunctorToFunctorProdAssociator_inv_app_app, congrRightFunctor_obj, congrRight_inverse, congrRight_unitIso_hom_app, CategoryTheory.prod.functorProdToProdFunctorAssociator_inv_app, CategoryTheory.prod.prodFunctorToFunctorProdAssociator_hom_app_app, congrRightFunctor_map, congrRight_counitIso_inv_app, CategoryTheory.prod.functorProdToProdFunctorAssociator_hom_app, congrRight_counitIso_hom_app, congrRight_unitIso_inv_app
congrRightFunctor 📖	CompOp	2 math math: congrRightFunctor_obj, congrRightFunctor_map
counit 📖	CompOp	29 math math: cancel_counit_right, functor_unit_comp, CategoryTheory.toOverIsoToOverUnit_inv_app_left, CategoryTheory.Monoidal.instIsMonoidalTransportedCounitEquivalenceTransported, map_η_comp_η, counit_naturality_assoc, CategoryTheory.Limits.IsColimit.ofCoconeEquiv_symm_apply_desc, CategoryTheory.Adjunction.Equivalence.instIsMonoidalCounit, CategoryTheory.Limits.HasLimit.isoOfEquivalence_hom_π, invFunIdAssoc_hom_app, functor_map_ε_inverse_comp_counit_app_assoc, CategoryTheory.Sieve.functorPushforward_inverse, unitInv_app_inverse, CategoryTheory.Sieve.mem_functorPushforward_inverse, toAdjunction_counit, fun_inv_map, CategoryTheory.Functor.fun_inv_map, symm_counit, map_η_comp_η_assoc, functor_map_ε_inverse_comp_counit_app, fun_inv_map_assoc, functor_map_μ_inverse_comp_counit_app_tensor_assoc, unit_inverse_comp, functor_map_μ_inverse_comp_counit_app_tensor, Equivalence_mk'_counit, counit_app_functor, unit_inverse_comp_assoc, counit_naturality, functor_unit_comp_assoc
counitInv 📖	CompOp	25 math math: symm_unit, counitInv_app_tensor_comp_functor_map_δ_inverse, CategoryTheory.Limits.HasColimit.isoOfEquivalence_inv_π, cancel_counitInv_right, counitInv_functor_comp, counitInv_app_comp_functor_map_η_inverse_assoc, cancel_counitInv_right_assoc, invFunIdAssoc_inv_app, counitInv_app_comp_functor_map_η_inverse, fun_inv_map, CategoryTheory.Functor.fun_inv_map, inverse_counitInv_comp_assoc, counitInv_app_functor, counitInv_functor_comp_assoc, fun_inv_map_assoc, cancel_counitInv_right_assoc', unit_app_inverse, counitInv_naturality, CategoryTheory.toOverIteratedSliceForwardIsoPullback_inv_app_left, Equivalence_mk'_counitInv, CategoryTheory.ComposableArrows.opEquivalence_counitIso_hom_app_app, counitInv_app_tensor_comp_functor_map_δ_inverse_assoc, counitInv_naturality_assoc, inverse_counitInv_comp, symmEquivInverse_map_app
counitIso 📖	CompOp	368 math math: sheafCongrPrecoherent_counitIso_hom_app_val_app, CategoryTheory.ComposableArrows.opEquivalence_counitIso_inv_app_app, CategoryTheory.Discrete.sumEquiv_counitIso_inv_app, CategoryTheory.Limits.IsLimit.ofConeEquiv_symm_apply_desc, CategoryTheory.Adjunction.toEquivalence_counitIso_hom_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_left, CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalence_counitIso_inv_app, sheafCongr.counitIso_hom_app_val_app, mapGrp_counitIso, CategoryTheory.eq_counitIso, sheafCongrPreregular_counitIso_inv_app_val_app, CategoryTheory.Pretriangulated.triangleRotation_counitIso, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_counitIso_hom_app_hom, AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso_inv_app, CategoryTheory.WithTerminal.equivComma_counitIso_hom_app_left_app, CategoryTheory.Idempotents.KaroubiKaroubi.equivalence_counitIso, CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence_counitIso, AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso_eq, counitIso_inv_app_comp_functor_map_η_inverse, partialFunEquivPointed_counitIso_inv_app_toFun, CategoryTheory.equivOfTensorIsoUnit_counitIso, CategoryTheory.WithTerminal.equivComma_counitIso_inv_app_left_app, CategoryTheory.Join.mapPairEquiv_counitIso, CategoryTheory.CostructuredArrow.prodEquivalence_counitIso, rightOp_counitIso_inv_app, CategoryTheory.Under.equivalenceOfIsInitial_counitIso, CategoryTheory.CatCommSq.hInv_iso_inv_app, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_counitIso, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_counitIso_inv_app_hom, CategoryTheory.cosimplicialSimplicialEquiv_counitIso_hom_app_app, CategoryTheory.Functor.leftOpRightOpEquiv_counitIso_inv_app_app, CategoryTheory.Over.equivalenceOfIsTerminal_counitIso, CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_hom_app_op_one, AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso_hom_app, CategoryTheory.simplicialCosimplicialEquiv_counitIso_inv_app_app, AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso_inv_app, CategoryTheory.ObjectProperty.topEquivalence_counitIso, CategoryTheory.Comon.Comon_EquivMon_OpOp_counitIso, CategoryTheory.Iso.isoInverseComp_inv_app, prod_counitIso, CategoryTheory.Grothendieck.grothendieckTypeToCat_counitIso_inv_app_coe, leftOp_counitIso_inv_app, CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_inv_app_op_zero, CategoryTheory.Comma.mapRightIso_counitIso_inv_app_left, CategoryTheory.Comma.mapRightIso_counitIso_inv_app_right, AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso_hom_app, CategoryTheory.Comma.opEquiv_counitIso, CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv_counitIso, CategoryTheory.Monad.monadMonEquiv_counitIso_hom_app_hom, congrFullSubcategory_counitIso, commGroupAddCommGroupEquivalence_counitIso, CategoryTheory.GradedObject.comapEquiv_counitIso, CategoryTheory.Comma.mapLeftIso_counitIso_inv_app_right, CategoryTheory.WithTerminal.equivComma_counitIso_hom_app_right, CategoryTheory.ShortComplex.functorEquivalence_counitIso, CategoryTheory.WithInitial.opEquiv_counitIso_hom_app, CategoryTheory.Pi.equivalenceOfEquiv_counitIso, CategoryTheory.Functor.currying_counitIso_hom_app_app, CategoryTheory.Iso.isoInverseComp_hom_app, CategoryTheory.Limits.Cocones.whiskeringEquivalence_unitIso, AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso_inv_app, CategoryTheory.MonoOver.mapIso_counitIso, CategoryTheory.Limits.Cocones.whiskeringEquivalence_inverse, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₂, CategoryTheory.Comma.toPUnitIdEquiv_counitIso_hom_app, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_counitIso_hom_app_hom, CategoryTheory.Limits.CategoricalPullback.functorEquiv_counitIso_inv_app_snd_app, CategoryTheory.WithTerminal.opEquiv_counitIso_inv_app, CategoryTheory.Functor.flipping_counitIso_inv_app_app_app, congrLeft_counitIso_inv_app, symm_unitIso, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_naturality_assoc, CategoryTheory.Preadditive.DoldKan.equivalence_counitIso, CategoryTheory.WithInitial.equivComma_counitIso_hom_app_right_app, CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_zero, CategoryTheory.Cat.opEquivalence_counitIso, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_naturality, AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso_inv_app, CoalgCat.comonEquivalence_counitIso, CategoryTheory.CategoryOfElements.structuredArrowEquivalence_counitIso, CategoryTheory.Limits.walkingCospanOpEquiv_counitIso_hom_app, OrderHom.equivalenceFunctor_counitIso_inv_app_app, CategoryTheory.Functor.Initial.conesEquiv_counitIso, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_naturality, Bipointed.swapEquiv_counitIso_hom_app_toFun, AddMonCat.equivalence_counitIso, CategoryTheory.Functor.opUnopEquiv_counitIso, CategoryTheory.Localization.equivalence_counitIso_app, CategoryTheory.Presheaf.coherentExtensiveEquivalence_counitIso, CategoryTheory.StructuredArrow.ofCommaSndEquivalence_counitIso, CategoryTheory.WithTerminal.coneEquiv_counitIso_inv_app_hom, CategoryTheory.prod.associativity_counitIso, CategoryTheory.Comma.equivProd_counitIso_hom_app, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_counitIso, CategoryTheory.WithTerminal.opEquiv_counitIso_hom_app, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₃, CategoryTheory.MonoidalCategory.DayFunctor.equiv_counitIso_inv_app, SimplicialObject.opEquivalence_counitIso, CategoryTheory.Limits.walkingCospanOpEquiv_counitIso_inv_app, CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_hom_app, symmEquivInverse_obj_counitIso_hom, CategoryTheory.Limits.pullbackConeEquivBinaryFan_counitIso, functor_map_μ_inverse_comp_counitIso_hom_app_tensor_assoc, CategoryTheory.WithInitial.equivComma_counitIso_inv_app_right_app, CategoryTheory.Functor.currying_counitIso_inv_app_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_naturality_assoc, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app_shift, CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence_counitIso, CategoryTheory.AsSmall.equiv_counitIso, CategoryTheory.WithInitial.coconeEquiv_counitIso_inv_app_hom, CategoryTheory.Idempotents.DoldKan.equivalence_counitIso, CategoryTheory.TwoSquare.equivalenceJ_counitIso, CategoryTheory.simplicialCosimplicialEquiv_counitIso_hom_app_app, CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_counitIso_hom_app, CategoryTheory.MonoidalCategory.DayFunctor.equiv_counitIso_hom_app, CategoryTheory.Limits.Cones.equivalenceOfReindexing_counitIso, CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso_counitIso, CategoryTheory.Discrete.productEquiv_counitIso_hom_app, CommShift.instCommShiftHomFunctorCounitIso, CategoryTheory.ULift.equivalence_counitIso_hom_app, CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalence_counitIso_inv_app_assoc, FinPartOrd.dualEquiv_counitIso, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_counitIso, CategoryTheory.CatCommSq.vInv_iso_hom_app, CategoryTheory.Functor.flipping_counitIso_hom_app_app_app, CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_counitIso_inv_app, changeFunctor_counitIso_hom_app, refl_counitIso, CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_counitIso, MulEquiv.toSingleObjEquiv_counitIso_hom, CategoryTheory.Under.postEquiv_counitIso, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_left_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app, unop_counitIso, CategoryTheory.typeEquiv_counitIso_inv_app_val_app, CategoryTheory.CostructuredArrow.mapNatIso_counitIso_inv_app_left, CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_counitIso, CategoryTheory.CostructuredArrow.mapIso_counitIso_hom_app_left, CategoryTheory.Adjunction.toEquivalence_counitIso_inv_app, CategoryTheory.Limits.Cones.postcomposeEquivalence_counitIso, CategoryTheory.Limits.CategoricalPullback.functorEquiv_counitIso_hom_app_fst_app, CategoryTheory.Limits.walkingSpanOpEquiv_counitIso_hom_app, changeInverse_counitIso_inv_app, HomologicalComplex.opEquivalence_counitIso, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_counitIso_inv_app_hom, TwoP.swapEquiv_counitIso_inv_app_hom_toFun, CategoryTheory.prod.rightUnitorEquivalence_counitIso, CategoryTheory.Grothendieck.grothendieckTypeToCat_counitIso_hom_app_coe, CategoryTheory.Comma.equivProd_counitIso_inv_app, CategoryTheory.WithInitial.equivComma_counitIso_hom_app_left, functor_map_ε_inverse_comp_counitIso_hom_app, CategoryTheory.cosimplicialSimplicialEquiv_counitIso_inv_app_app, CategoryTheory.Comma.mapLeftIso_counitIso_hom_app_left, HomologicalComplex.dgoEquivHomologicalComplex_counitIso, CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_counitIso_inv_app_f, CategoryTheory.Discrete.sumEquiv_counitIso_hom_app, CategoryTheory.ShortComplex.opEquiv_counitIso, CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_apply, CategoryTheory.Over.postEquiv_counitIso, CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_counitIso, CategoryTheory.equivToOverUnit_counitIso, MonObj.mopEquiv_counitIso_hom_app_hom_unmop, CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_counitIso_inv_app_right_app, CategoryTheory.Pretriangulated.triangleOpEquivalence_counitIso, CategoryTheory.ObjectProperty.fullSubcategoryCongr_counitIso, CategoryTheory.Over.ConstructProducts.conesEquiv_counitIso, CategoryTheory.Limits.Cones.whiskeringEquivalence_counitIso, MulEquiv.toSingleObjEquiv_counitIso_inv, CategoryTheory.skeletonEquivalence_counitIso, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_right, CategoryTheory.MonoidalOpposite.unmopEquiv_counitIso_hom_app, AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso_eq, CategoryTheory.Iso.isoFunctorOfIsoInverse_inv_app, OrderIso.equivalence_counitIso, sheafCongrPreregular_counitIso_hom_app_val_app, CategoryTheory.Comma.toIdPUnitEquiv_counitIso_hom_app, commAlgCatEquivUnder_counitIso, sheafCongrPrecoherent_counitIso_inv_app_val_app, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_counitIso_hom, HomologicalComplex₂.flipEquivalence_counitIso, TopologicalSpace.Opens.overEquivalence_counitIso_inv_app, ext_iff, symmEquivInverse_obj_counitIso_inv, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_counitIso, CategoryTheory.Monoidal.transportStruct_leftUnitor, CategoryTheory.Monoidal.transportStruct_rightUnitor, CategoryTheory.Over.opEquivOpUnder_counitIso, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_left_app, CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_inv_app, CategoryTheory.forgetEnrichmentOppositeEquivalence_counitIso, changeInverse_counitIso_hom_app, TopCat.Presheaf.generateEquivalenceOpensLe_counitIso, CategoryTheory.Endofunctor.Algebra.equivOfNatIso_counitIso, CategoryTheory.coalgebraEquivOver_counitIso, CategoryTheory.WithInitial.opEquiv_counitIso_inv_app, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_obj, CategoryTheory.Limits.widePushoutShapeOpEquiv_counitIso, Bipointed.swapEquiv_counitIso_inv_app_toFun, CategoryTheory.Monad.algebraEquivOfIsoMonads_counitIso, CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_hom_app_unop, mapCommMon_counitIso, sheafCongr_counitIso, CategoryTheory.MonoidalOpposite.mopMopEquivalence_counitIso_inv_app, symmEquiv_counitIso, CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_inv_app_unop_assoc, CategoryTheory.Comma.mapRightIso_counitIso_hom_app_right, CategoryTheory.Limits.Cocones.functorialityEquivalence_counitIso, mapMon_counitIso, CategoryTheory.Iso.isoInverseOfIsoFunctor_inv_app, CategoryTheory.prod.leftUnitorEquivalence_counitIso, core_counitIso_hom_app_iso_hom, trans_counitIso, CategoryTheory.CatCommSq.vInv_iso_inv_app, counitIso_inv_app_tensor_comp_functor_map_δ_inverse_assoc, functor_map_ε_inverse_comp_counitIso_hom_app_assoc, CategoryTheory.RelCat.opEquivalence_counitIso, CategoryTheory.ShrinkHoms.equivalence_counitIso, CategoryTheory.Functor.leftOpRightOpEquiv_counitIso_hom_app_app, CategoryTheory.Discrete.equivalence_counitIso, ModuleCat.matrixEquivalence_counitIso, CategoryTheory.orderDualEquivalence_counitIso, CategoryTheory.Discrete.productEquiv_counitIso_inv_app, counitIso_inv_app_comp_functor_map_η_inverse_assoc, CategoryTheory.Subobject.lowerEquivalence_counitIso, CategoryTheory.Idempotents.karoubiUniversal₁_counitIso, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app_assoc, mapHomologicalComplex_counitIso, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app, Action.functorCategoryEquivalence_counitIso, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_inv_app_hom_hom_hom, OrderHom.equivalenceFunctor_counitIso_hom_app_app, rightOp_counitIso_hom_app, CategoryTheory.Limits.Cones.functorialityEquivalence_counitIso, CategoryTheory.CostructuredArrow.ofCommaFstEquivalence_counitIso, CategoryTheory.StructuredArrow.mapNatIso_counitIso_hom_app_right, CategoryTheory.typeEquiv_counitIso_hom_app_val_app, CategoryTheory.functorProdFunctorEquiv_counitIso, CategoryTheory.Comma.mapLeftIso_counitIso_inv_app_left, CategoryTheory.Limits.Cone.equivCostructuredArrow_counitIso, CategoryTheory.Comma.mapRightIso_counitIso_hom_app_left, CategoryTheory.ShiftedHom.opEquiv'_symm_op_opShiftFunctorEquivalence_counitIso_inv_app_op_shift, CategoryTheory.algebraEquivUnder_counitIso, CategoryTheory.Comma.mapLeftIso_counitIso_hom_app_right, CategoryTheory.Pi.optionEquivalence_counitIso, CategoryTheory.opOpEquivalence_counitIso, functor_unitIso_comp, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_right, groupAddGroupEquivalence_counitIso, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_counitIso, core_counitIso_hom_app_iso_inv, CategoryTheory.Over.iteratedSliceEquiv_counitIso, CategoryTheory.Groupoid.invEquivalence_counitIso, symm_counitIso, CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_counitIso_hom_app_f, CategoryTheory.Monoidal.comonFunctorCategoryEquivalence_counitIso, TopCat.Presheaf.presheafEquivOfIso_counitIso_inv_app_app, CategoryTheory.CostructuredArrow.mapNatIso_counitIso_hom_app_left, CategoryTheory.ULift.equivalence_counitIso_inv_app, CategoryTheory.WithInitial.equivComma_counitIso_inv_app_left, CategoryTheory.Iso.isoInverseOfIsoFunctor_hom_app, CategoryTheory.Monoidal.monFunctorCategoryEquivalence_counitIso, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_hom_app_hom_hom_hom, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_counitIso_inv, CategoryTheory.Functor.Final.coconesEquiv_counitIso, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app_assoc, CategoryTheory.Pretriangulated.shift_unop_opShiftFunctorEquivalence_counitIso_hom_app, CategoryTheory.subterminalsEquivMonoOverTerminal_counitIso, CategoryTheory.Monad.monadMonEquiv_counitIso_inv_app_hom, MonObj.mopEquiv_counitIso_inv_app_hom_unmop, CategoryTheory.ForgetEnrichment.equiv_counitIso, CategoryTheory.WithInitial.coconeEquiv_counitIso_hom_app_hom, functor_map_μ_inverse_comp_counitIso_hom_app_tensor, CategoryTheory.Iso.inverseCompIso_inv_app, TopCat.Presheaf.presheafEquivOfIso_counitIso_hom_app_app, CategoryTheory.Iso.isoFunctorOfIsoInverse_hom_app, CategoryTheory.prodOpEquiv_counitIso_hom_app, CategoryTheory.Limits.coconeEquivalenceOpConeOp_counitIso, AddCommMonCat.equivalence_counitIso, leftOp_counitIso_hom_app, CategoryTheory.shiftEquiv'_counitIso, CategoryTheory.Comma.toPUnitIdEquiv_counitIso_inv_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_right_app, mapCommGrp_counitIso, core_counitIso_inv_app_iso_hom, CategoryTheory.Iso.inverseCompIso_hom_app, congrLeft_counitIso_hom_app, AlgebraicTopology.DoldKan.Compatibility.τ₀_hom_app, partialFunEquivPointed_counitIso_hom_app_toFun, CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence_counitIso, TwoP.swapEquiv_counitIso_hom_app_hom_toFun, CategoryTheory.Prod.braiding_counitIso, CategoryTheory.MonoidalOpposite.unmopEquiv_counitIso_inv_app, CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_counitIso, CategoryTheory.Under.opEquivOpOver_counitIso, CategoryTheory.Comma.toIdPUnitEquiv_counitIso_inv_app, AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso_eq, CategoryTheory.StructuredArrow.preEquivalence_counitIso, CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_inv_app_unop, FundamentalGroupoid.punitEquivDiscretePUnit_counitIso, symmEquivInverse_obj_unitIso_inv, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₁, alexDiscEquivPreord_counitIso, counitIso_inv_app_tensor_comp_functor_map_δ_inverse, TopologicalSpace.Opens.mapMapIso_counitIso, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_counitIso, CategoryTheory.Square.arrowArrowEquivalence'_counitIso, SimplexCategory.revEquivalence_counitIso, CategoryTheory.Pseudofunctor.DescentData.pullFunctorEquivalence_counitIso, CategoryTheory.MonoOver.congr_counitIso, CategoryTheory.CatCommSq.hInv_iso_hom_app, CategoryTheory.StructuredArrow.prodEquivalence_counitIso, CategoryTheory.sheafBotEquivalence_counitIso, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_counitIso_inv, CategoryTheory.Limits.walkingSpanOpEquiv_counitIso_inv_app, CategoryTheory.equivEssImageOfReflective_counitIso, TopologicalSpace.Opens.overEquivalence_counitIso_hom_app, CategoryTheory.ComposableArrows.opEquivalence_counitIso_hom_app_app, SSet.opEquivalence_counitIso, CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_one, CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_hom_app_unop_assoc, Types.monoOverEquivalenceSet_counitIso, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_counitIso_hom_app_right_app, CategoryTheory.WithTerminal.equivComma_counitIso_inv_app_right, op_counitIso, CategoryTheory.Limits.Cocone.equivStructuredArrow_counitIso, CategoryTheory.prodOpEquiv_counitIso_inv_app, CategoryTheory.MonoidalOpposite.mopMopEquivalence_counitIso_hom_app, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence_counitIso, CategoryTheory.Pretriangulated.shift_unop_opShiftFunctorEquivalence_counitIso_inv_app, HomologicalComplex.unopEquivalence_counitIso, CategoryTheory.Limits.CategoricalPullback.functorEquiv_counitIso_hom_app_snd_app, CategoryTheory.piEquivalenceFunctorDiscrete_counitIso, CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_inv_app_op_one, sheafCongr.counitIso_inv_app_val_app, CategoryTheory.StructuredArrow.mapNatIso_counitIso_inv_app_right, CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_hom_app_op_zero, pi_counitIso, CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_counitIso, symmEquivInverse_obj_unitIso_hom, CategoryTheory.Limits.widePullbackShapeOpEquiv_counitIso, core_counitIso_inv_app_iso_inv, CategoryTheory.Functor.equiv_counitIso, CategoryTheory.Limits.Cocones.whiskeringEquivalence_counitIso, AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso_hom_app, commBialgCatEquivComonCommAlgCat_counitIso_inv_app, CategoryTheory.Subfunctor.equivalenceMonoOver_counitIso, CategoryTheory.WithTerminal.coneEquiv_counitIso_hom_app_hom, congrRight_counitIso_inv_app, CategoryTheory.Limits.Cocones.precomposeEquivalence_counitIso, CategoryTheory.CostructuredArrow.mapIso_counitIso_inv_app_left, CategoryTheory.StructuredArrow.mapIso_counitIso_hom_app_right, congrRight_counitIso_hom_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_right_app, CategoryTheory.Square.arrowArrowEquivalence_counitIso, CategoryTheory.Sum.functorEquiv_counitIso, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_left, CategoryTheory.StructuredArrow.mapIso_counitIso_inv_app_right, changeFunctor_counitIso_inv_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_apply_assoc, CategoryTheory.MonoidalOpposite.mopEquiv_counitIso, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_counitIso_hom, CategoryTheory.Limits.CategoricalPullback.functorEquiv_counitIso_inv_app_fst_app, AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso_hom_app, induced_counitIso, CategoryTheory.comonEquiv_counitIso, CategoryTheory.Square.flipEquivalence_counitIso, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app_shift
fullyFaithfulFunctor 📖	CompOp	5 math math: CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitorCorepresentingIso_hom_app_app, CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitorCorepresentingIso_hom_app_app, CategoryTheory.MonoidalCategory.DayConvolution.associatorCorepresentingIso_hom_app_app, CategoryTheory.Limits.CategoricalPullback.mkNatIso_eq, additive_inverse_of_FullyFaithful
fullyFaithfulInverse 📖	CompOp	—
funInvIdAssoc 📖	CompOp	6 math math: funInvIdAssoc_hom_app, CategoryTheory.ComposableArrows.opEquivalence_unitIso_inv_app, CategoryTheory.ComposableArrows.opEquivalence_unitIso_hom_app, congrLeft_unitIso_inv_app, congrLeft_unitIso_hom_app, funInvIdAssoc_inv_app
functor 📖	CompOp	978 math math: CategoryTheory.MorphismProperty.LeftFraction.map_compatibility, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_app_eq, CochainComplex.acyclic_op, CategoryTheory.MorphismProperty.inverseImage_equivalence_inverse_eq_map_functor, CategoryTheory.sheafBotEquivalence_functor, prod_unitIso, CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_hom_app_zero, CategoryTheory.Sum.natTransOfWhiskerLeftInlInr_app, leftOp_unitIso_hom_app, sheafCongrPrecoherent_counitIso_hom_app_val_app, CategoryTheory.ComposableArrows.opEquivalence_counitIso_inv_app_app, CategoryTheory.Limits.IsLimit.ofConeEquiv_symm_apply_desc, CategoryTheory.Pi.eqToEquivalenceFunctorIso_hom, AlgebraicTopology.DoldKan.Compatibility.equivalence₀_unitIso_hom_app, CategoryTheory.WithInitial.equivComma_functor_obj_right_obj, CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalence_counitIso_inv_app, sheafCongr.counitIso_hom_app_val_app, CategoryTheory.Functor.leftOpRightOpEquiv_functor_obj_map, mapGrp_counitIso, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_add_unitIso_hom_app_eq, Bipointed.swapEquiv_functor_obj_toProd, CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_functor_map_left, comp_asNatTrans, CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_one, sheafCongrPreregular_counitIso_inv_app_val_app, MoritaEquivalence.linear, CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_map_val, CategoryTheory.WithTerminal.equivComma_functor_obj_left_obj, CategoryTheory.StructuredArrow.mapIso_functor_obj_left, AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso_inv_app, sheafCongr_functor, CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_functor, unitIso_hom_app_comp_inverse_map_η_functor_assoc, CategoryTheory.MonoOver.congr_unitIso, commGroupAddCommGroupEquivalence_functor, counitInv_app_tensor_comp_functor_map_δ_inverse, CategoryTheory.Sum.functorEquivFunctorCompFstIso_inv_app_app, CategoryTheory.Limits.Cones.equivalenceOfReindexing_inverse, CategoryTheory.Limits.Cones.whiskeringEquivalence_functor, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₁, CategoryTheory.MonoOver.mapIso_functor, CategoryTheory.Limits.widePushoutShapeOpEquiv_functor, CategoryTheory.Comma.toPUnitIdEquiv_functor_map, CategoryTheory.MonoidalOpposite.mopMopEquivalence_functor_obj, CategoryTheory.Square.arrowArrowEquivalence_functor, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_X, counitIso_inv_app_comp_functor_map_η_inverse, CategoryTheory.Endofunctor.Algebra.equivOfNatIso_functor, CategoryTheory.Limits.parallelPairOpIso_inv_app_zero, CategoryTheory.Limits.HasColimit.isoOfEquivalence_inv_π, CategoryTheory.Monoidal.transportStruct_associator, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_map_f_f, CategoryTheory.StructuredArrow.ofCommaSndEquivalence_functor, CategoryTheory.Under.forgetMapInitial_inv_app, CategoryTheory.CategoryOfElements.structuredArrowEquivalence_functor, AddMonCat.equivalence_functor_obj_coe, CategoryTheory.WithInitial.isColimitEquiv_apply_desc_right, CategoryTheory.Join.mapPairEquiv_unitIso, CategoryTheory.Join.mapPairEquiv_counitIso, rightOp_counitIso_inv_app, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_snd_fst, CategoryTheory.typeEquiv_functor_obj_val_obj, CategoryTheory.WithInitial.coconeEquiv_functor_obj_pt, CategoryTheory.MonoidalClosed.ofEquiv_uncurry_def, CategoryTheory.Sum.functorEquiv_functor_map, CategoryTheory.CatCommSq.hInv_iso_inv_app, CategoryTheory.Discrete.opposite_functor_obj_as, leftOp_unitIso_inv_app, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_functor_obj_ι_app, leftOp_functor_obj, prod_functor, CategoryTheory.Pretriangulated.Opposite.mem_distinguishedTriangles_iff', CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_map_hom, CochainComplex.exactAt_op, CategoryTheory.Over.forgetMapTerminal_hom_app, rightOp_functor_map, CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_hom_app_op_one, CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor_inv_hom, AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso_hom_app, CategoryTheory.Limits.PushoutCocone.unop_π_app, AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso_inv_app, CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_functor, IsTriangulated.instIsTriangulatedFunctor, isRightAdjoint_functor, CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_left_inv, CategoryTheory.Under.mapIso_functor, CategoryTheory.CostructuredArrow.mapIso_functor_obj_hom, CategoryTheory.Iso.isoInverseComp_inv_app, CompleteLat.dualEquiv_functor, CategoryTheory.Comma.mapLeftIso_functor_map_left, prod_counitIso, Action.leftUnitor_inv_hom, CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_functor_obj_left, MonObj.mopEquivCompForgetIso_hom_app_unmop, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_left, AlgebraicTopology.DoldKan.Compatibility.equivalence_functor, leftOp_counitIso_inv_app, CategoryTheory.shiftEquiv'_functor, CategoryTheory.Monoidal.instIsMonoidalUnitTransportedEquivalenceTransported, CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_inv_app_op_zero, CategoryTheory.Limits.CategoricalPullback.functorEquiv_functor_obj_fst_map, AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso_hom_app, OrderIso.equivalence_functor, cancel_unit_right, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_functor_obj, CategoryTheory.Limits.Cocones.precomposeEquivalence_functor, CategoryTheory.Limits.Cones.functorialityEquivalence_functor, CategoryTheory.comonEquiv_functor, AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso_hom_app, CategoryTheory.Comon.monoidal_rightUnitor_inv_hom, cancel_counit_right, CategoryTheory.forgetEnrichmentOppositeEquivalence_functor, map_injective_iff, CategoryTheory.WithInitial.opEquiv_functor_map, CategoryTheory.Functor.flipping_functor_map_app_app, CategoryTheory.Functor.currying₃_unitIso_hom_app_app_app_app, CategoryTheory.Monoidal.transportStruct_tensorHom, BoolAlg.dualEquiv_functor, CategoryTheory.Preadditive.DoldKan.equivalence_functor, FinPartOrd.dualEquiv_functor, CategoryTheory.Idempotents.karoubiUniversal_functor_eq, unitInv_naturality, functor_unit_comp, Action.whiskerRight_hom, CategoryTheory.Comma.mapRightIso_functor_map_left, inv_fun_map, full_functor, AlgebraicTopology.AlternatingCofaceMapComplex.d_eq_unop_d, CategoryTheory.coalgebraEquivOver_functor, CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv_functor, CategoryTheory.Pi.equivalenceOfEquiv_unitIso, CategoryTheory.Under.equivalenceOfIsInitial_functor, CategoryTheory.WithInitial.isColimitEquiv_symm_apply_desc, sheafCongrPreregular_unitIso_hom_app_val_app, CategoryTheory.Pi.equivalenceOfEquiv_counitIso, HomologicalComplex.unopEquivalence_functor, CategoryTheory.Sieve.pullback_functorPushforward_equivalence_eq, CategoryTheory.CostructuredArrow.overEquivPresheafCostructuredArrow_inverse_map_toOverCompCoyoneda, CategoryTheory.Iso.isoInverseComp_hom_app, CategoryTheory.StructuredArrow.mapNatIso_functor_obj_right, CategoryTheory.Functor.IsDenseSubsite.sheafEquiv_functor, core_unitIso_hom_app_iso_inv, CategoryTheory.Limits.Cocones.whiskeringEquivalence_unitIso, CategoryTheory.Sum.functorEquiv_unit_app_app_inr, CategoryTheory.Monoidal.transportStruct_tensorObj, CategoryTheory.WithTerminal.equivComma_functor_obj_left_map, toOrderIso_apply, CategoryTheory.Functor.curry₃_obj_obj_map_app, CategoryTheory.Limits.hasColimit_equivalence_comp, AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso_inv_app, CategoryTheory.Sum.functorEquiv_unitIso_inv_app_app_inl, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompPointIso_hom_app, CochainComplex.homotopyUnop_hom_eq, FinBddDistLat.dualEquiv_functor, CategoryTheory.Limits.Cocones.whiskeringEquivalence_inverse, CategoryTheory.WithTerminal.equivComma_functor_obj_right, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₂, CategoryTheory.Join.opEquiv_functor_obj_op_right, BddOrd.dualEquiv_functor, CategoryTheory.Limits.parallelPairOpIso_inv_app_one, changeInverse_functor, CategoryTheory.Comma.toPUnitIdEquiv_counitIso_hom_app, CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso_incl, CategoryTheory.Idempotents.karoubiUniversal₁_functor, CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_inv_app_fst, sheafCongrPreregular_inverse_obj_val_map, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_functor, congrLeft_counitIso_inv_app, CategoryTheory.Comma.mapRightIso_functor_obj_right, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_snd_snd, CategoryTheory.TwoSquare.GuitartExact.vComp_iff_of_equivalences, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_p, CategoryTheory.Limits.HasColimit.isoOfEquivalence_hom_π, TwoP.swapEquiv_functor_map_hom_toFun, CategoryTheory.Monoidal.instIsMonoidalTransportedCounitEquivalenceTransported, symm_unitIso, CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_mul, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_naturality_assoc, CategoryTheory.WithInitial.equivComma_functor_obj_right_map, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₃, CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_hom_hom₂, mapHomologicalComplex_unitIso, CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_zero, boolRingCatEquivBoolAlg_functor, CategoryTheory.Functor.asEquivalence_functor, CategoryTheory.ShrinkHoms.equivalence_functor, funInvIdAssoc_hom_app, CategoryTheory.Functor.Final.coconesEquiv_functor, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_naturality, pi_functor, AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso_inv_app, CategoryTheory.Idempotents.toKaroubiEquivalence_functor_additive, CategoryTheory.MonoidalOpposite.mopMopEquivalence_unitIso_hom_app_unmop_unmop, CategoryTheory.Comon.Comon_EquivMon_OpOp_functor, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_naturality, CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_hom_hom₁, sheafCongrPrecoherent_functor_obj_val_obj, CategoryTheory.Limits.CategoricalPullback.functorEquiv_functor_obj_iso_inv_app, CategoryTheory.Localization.equivalence_counitIso_app, CategoryTheory.Limits.Fork.equivOfIsos_functor_obj_ι, CategoryTheory.WithTerminal.coneEquiv_functor_obj_π_app_star, AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso_inv_app, CategoryTheory.ShortComplex.functorEquivalence_functor, CategoryTheory.eq_functor_obj, CategoryTheory.CostructuredArrow.mapIso_functor_map_left, CategoryTheory.Limits.CategoricalPullback.functorEquiv_functor_obj_fst_obj, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_left, CategoryTheory.Monoidal.transportStruct_tensorUnit, CategoryTheory.piEquivalenceFunctorDiscrete_functor_obj, CategoryTheory.Limits.Cocones.equivalenceOfReindexing_functor_obj, ModuleCat.matrixEquivalence_functor, PartOrd.dualEquiv_functor, MonObj.mopEquiv_functor_obj_mon_one_unmop, CategoryTheory.StructuredArrow.prodEquivalence_functor, cancel_counitInv_right, AddCommMonCat.equivalence_functor_map, SemilatSupCatEquivSemilatInfCat_functor, CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_inv_app_unop, faithful_functor, changeFunctor_unitIso_hom_app, CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_inv, CategoryTheory.ComposableArrows.opEquivalence_unitIso_inv_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso_inv_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso_hom_app, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₃, map_η_comp_η, CategoryTheory.Limits.pullbackConeEquivBinaryFan_functor_map_hom, counit_naturality_assoc, CategoryTheory.StructuredArrow.mapNatIso_functor_obj_hom, mapCommGrp_functor, Lat.dualEquiv_functor, CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_hom_app_snd, CategoryTheory.Limits.parallelPairOpIso_hom_app_one, commAlgCatEquivUnder_functor_obj, CategoryTheory.Limits.IsColimit.ofCoconeEquiv_symm_apply_desc, symmEquivInverse_obj_counitIso_hom, CategoryTheory.Idempotents.DoldKan.N₂_map_isoΓ₀_hom_app_f, inverseFunctor_map, CategoryTheory.StructuredArrow.mapNatIso_functor_map_right, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_functor, functor_map_μ_inverse_comp_counitIso_hom_app_tensor_assoc, CategoryTheory.CostructuredArrow.mapIso_functor_obj_left, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_snd_snd, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_functor_map_hom, sheafCongrPreregular_functor_obj_val_obj, CategoryTheory.MonoidalCategory.DayFunctor.equiv_functor_map, changeFunctor_trans, CategoryTheory.Limits.Cones.whiskeringEquivalence_inverse, CategoryTheory.Limits.IsLimit.pullbackConeEquivBinaryFanFunctor_lift_left, sheafCongrPreregular_functor_map_val_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_naturality_assoc, CategoryTheory.functorProdFunctorEquiv_functor, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_map_f_f, CategoryTheory.Functor.curry₃_obj_map_app_app, CategoryTheory.Adjunction.Equivalence.instIsMonoidalCounit, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app_shift, CategoryTheory.IsSeparating.of_equivalence, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_map_left, HomologicalComplex.dgoEquivHomologicalComplex_functor, CategoryTheory.WithTerminal.equivComma_functor_map_right, CategoryTheory.Comon.monoidal_whiskerLeft_hom, mapMon_unitIso, CategoryTheory.Monoidal.monFunctorCategoryEquivalence_functor, CategoryTheory.Comma.toPUnitIdEquiv_functor_obj, CategoryTheory.StructuredArrow.preEquivalence_functor, mapAction_functor, CategoryTheory.cosimplicialSimplicialEquiv_functor_obj_obj, pi_unitIso, CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_functor, counitInv_functor_comp, sheafCongrPreregular_inverse_map_val_app, sheafCongrPrecoherent_functor_obj_val_map, CategoryTheory.IsSeparator.of_equivalence, CategoryTheory.decomposedEquiv_functor, CategoryTheory.Adjunction.Equivalence.instIsMonoidalUnit, CategoryTheory.WithInitial.coconeEquiv_functor_obj_ι_app_star, CategoryTheory.Limits.CategoricalPullback.functorEquiv_functor_map_fst_app, CategoryTheory.Subfunctor.equivalenceMonoOver_functor_map, CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_obj_fst, commBialgCatEquivComonCommAlgCat_functor_obj_unop_X, CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_inv_hom₃, symmEquivFunctor_map, sheafCongrPreregular_functor_obj_val_map, CategoryTheory.Comma.mapLeftIso_functor_obj_left, CategoryTheory.Over.postEquiv_inverse, CategoryTheory.Pi.evalCompEqToEquivalenceFunctor_hom, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₁, CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_hom_hom₃, AlgebraicTopology.DoldKan.Compatibility.equivalence₁_functor, CategoryTheory.WithTerminal.coneEquiv_functor_obj_π_app_of, refl_functor, CategoryTheory.Over.forgetMapTerminal_inv_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_app, CategoryTheory.ComposableArrows.opEquivalence_functor_obj_map, unitIso_hom_app_tensor_comp_inverse_map_δ_functor, partialFunEquivPointed_functor_map_toFun, CategoryTheory.TwoSquare.GuitartExact.vComp'_iff_of_equivalences, CategoryTheory.Comon.monoidal_leftUnitor_hom_hom, FinBoolAlg.dualEquiv_functor, CategoryTheory.Over.equivalenceOfIsTerminal_functor, sheafCongrPrecoherent_inverse_map_val_app, isDenseSubsite_functor_of_isCocontinuous, Action.functorCategoryEquivalence_functor, rightOp_unitIso_hom_app, CategoryTheory.Limits.colimitLimitToLimitColimitCone_hom, unitIso_hom_app_tensor_comp_inverse_map_δ_functor_assoc, CategoryTheory.MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_μ, CategoryTheory.prod.rightUnitorEquivalence_functor, CategoryTheory.Limits.Cones.equivalenceOfReindexing_counitIso, CategoryTheory.Join.opEquiv_functor_map_op_edge, CategoryTheory.Limits.walkingParallelPairOpEquiv_functor, TopologicalSpace.Opens.mapMapIso_functor, CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_X, CommShift.instCommShiftHomFunctorCounitIso, CategoryTheory.MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_ε, congrLeft_functor, CategoryTheory.Join.opEquiv_functor_map_op_inclRight, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_zero_unitIso_inv_app, CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalence_counitIso_inv_app_assoc, CategoryTheory.Limits.opSpan_hom_app, CategoryTheory.Iso.compInverseIso_inv_app, CategoryTheory.Limits.coconeEquivalenceOpConeOp_functor_obj, TopCat.Presheaf.presheafEquivOfIso_unitIso_hom_app_app, unitInv_naturality_assoc, CategoryTheory.ShortComplex.opEquiv_functor, TopologicalSpace.Opens.coe_overEquivalence_functor_obj, CategoryTheory.CatCommSq.vInv_iso_hom_app, DistLat.dualEquiv_functor, CategoryTheory.Sum.natIsoOfWhiskerLeftInlInr_eq, CategoryTheory.CostructuredArrow.mapNatIso_functor_obj_hom, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_obj_pt, CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_functor_map, CategoryTheory.Comma.mapRightIso_functor_obj_hom, essSurj_functor, CategoryTheory.Limits.CategoricalPullback.functorEquiv_functor_map_snd_app, CategoryTheory.Comma.toIdPUnitEquiv_unitIso_inv_app_right, CategoryTheory.Limits.Cones.whiskeringEquivalence_unitIso, CategoryTheory.Functor.leftOpRightOpEquiv_functor_obj_obj, map_projective_iff, CategoryTheory.Comma.toPUnitIdEquiv_unitIso_inv_app_left, congrRight_functor, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_right, CategoryTheory.MonoidalOpposite.unmopEquiv_unitIso_inv_app_unmop, changeFunctor_counitIso_hom_app, Preord.dualEquiv_functor, CategoryTheory.equivEssImageOfReflective_functor, CategoryTheory.Limits.IsLimit.ofConeEquiv_apply_desc, CategoryTheory.Limits.HasLimit.isoOfEquivalence_hom_π, MulEquiv.toSingleObjEquiv_functor_obj, TopCat.Presheaf.whiskerIsoMapGenerateCocone_inv_hom, CategoryTheory.Pretriangulated.preadditiveYoneda_homologySequenceδ_apply, CategoryTheory.Discrete.equivalence_functor, CategoryTheory.Under.postEquiv_counitIso, CategoryTheory.Groupoid.invEquivalence_functor_map, counitInv_app_comp_functor_map_η_inverse_assoc, CategoryTheory.ComposableArrows.opEquivalence_functor_map_app, sheafCongrPrecoherent_inverse_obj_val_obj, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_left_app, CategoryTheory.Functor.curry₃_obj_obj_obj_map, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app, CategoryTheory.WithInitial.coconeEquiv_functor_map_hom, unop_counitIso, CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_inv_hom₁, CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence_hom, CategoryTheory.ComposableArrows.opEquivalence_inverse_obj, mapCommGrp_unitIso, cancel_unitInv_right, invFunIdAssoc_hom_app, unitIso_hom_app_comp_inverse_map_η_functor, CategoryTheory.Limits.pullbackConeEquivBinaryFan_functor_obj, CategoryTheory.Functor.opUnopEquiv_functor, CategoryTheory.sum.associativity_functor, CategoryTheory.Iso.compInverseIso_hom_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_hom_app_app, CategoryTheory.WithInitial.equivComma_functor_map_left, changeFunctor_refl, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_functor_obj, CategoryTheory.Limits.Cones.functorialityEquivalence_unitIso, CategoryTheory.WithTerminal.opEquiv_functor_obj, functor_map_ε_inverse_comp_counit_app_assoc, CategoryTheory.cosimplicialSimplicialEquiv_functor_map_app, CategoryTheory.Sieve.functorPushforward_inverse, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_right, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_d_f, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_fst, changeInverse_counitIso_inv_app, CategoryTheory.Limits.opCospan_hom_app, CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv_functor_map_term, CategoryTheory.IsCoseparating.of_equivalence, CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_map_f, CategoryTheory.RelCat.opEquivalence_functor, CategoryTheory.Functor.equiv_functor_obj, AlgebraicTopology.DoldKan.compatibility_N₂_N₁_karoubi, CategoryTheory.IsUniversalColimit.whiskerEquivalence, CategoryTheory.Monad.algebraEquivOfIsoMonads_functor, sheafCongr.inverse_obj_val_obj, mapCommMon_unitIso, instIsDenseSubsiteInducedTopologyInverseFunctor, CategoryTheory.CostructuredArrow.mapIso_functor_map_right, mkIso_hom, changeInverse_unitIso_inv_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_zero_unitIso_hom_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompPointIso_inv_app, CategoryTheory.WithTerminal.equivComma_functor_obj_hom_app, CategoryTheory.Pretriangulated.op_distinguished, CategoryTheory.CostructuredArrow.overEquivPresheafCostructuredArrow_functor_map_toOverCompYoneda, CategoryTheory.Comon.monoidal_whiskerRight_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_map_hom_hom, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_functor_map, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence_functor, CategoryTheory.WithTerminal.isLimitEquiv_symm_apply_lift, CategoryTheory.Comma.toIdPUnitEquiv_unitIso_hom_app_right, CoalgCat.comonEquivalence_functor, functor_map_ε_inverse_comp_counitIso_hom_app, CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_inverseImage_iff, CategoryTheory.Prod.braiding_functor, CategoryTheory.ComposableArrows.opEquivalence_unitIso_hom_app, CategoryTheory.Subfunctor.equivalenceMonoOver_functor_obj, CategoryTheory.Limits.Cones.postcomposeEquivalence_functor, CategoryTheory.AsSmall.equiv_functor, symmEquiv_functor, CategoryTheory.Under.forgetMapInitial_hom_app, symmEquivInverse_obj_functor, CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv_functor_obj_some, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_functor_map_hom, CategoryTheory.Pseudofunctor.DescentData.pullFunctorEquivalence_functor, CategoryTheory.Comma.mapRightIso_functor_map_right, cancel_counitInv_right_assoc, TwoP.swapEquiv_functor_obj_X, CategoryTheory.WithInitial.equivComma_functor_map_right_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_apply, CategoryTheory.Over.postEquiv_counitIso, CategoryTheory.Comma.toIdPUnitEquiv_functor_map, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_right, CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor_hom_hom, TwoP.swapEquiv_functor_obj_toTwoPointing_toProd, sheafCongr.unitIso_hom_app_val_app, CategoryTheory.Comon.monoidal_associator_hom_hom, CategoryTheory.MonoidalCategory.DayFunctor.equiv_functor_obj, Bipointed.swapEquiv_functor_map_toFun, CategoryTheory.prod.prodFunctorToFunctorProdAssociator_inv_app_app, CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence_inv, CategoryTheory.typeEquiv_functor_obj_val_map, CategoryTheory.Over.iteratedSliceEquiv_functor, CategoryTheory.WithInitial.coconeEquiv_functor_obj_ι_app_of, CategoryTheory.Limits.CategoricalPullback.functorEquiv_functor_obj_iso_hom_app, invFunIdAssoc_inv_app, CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_inv_app_zero, CategoryTheory.Monoidal.transportStruct_whiskerRight, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_functor_obj_pt, CategoryTheory.Limits.reflexiveCoforkEquivCofork_functor_obj_pt, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_left_app, CategoryTheory.Under.opEquivOpOver_functor_obj, CategoryTheory.WithInitial.equivComma_functor_obj_hom_app, CategoryTheory.Pretriangulated.triangleOpEquivalence_functor, CategoryTheory.Comma.toIdPUnitEquiv_functor_obj, CategoryTheory.Limits.Cones.whiskeringEquivalence_counitIso, BddDistLat.dualEquiv_functor, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_right, congrLeft_unitIso_inv_app, CategoryTheory.MonoidalOpposite.unmopEquiv_counitIso_hom_app, CategoryTheory.Cat.opEquivalence_functor, CategoryTheory.Adjunction.rightOp_eq, cancel_unit_right_assoc, mapGrp_unitIso, functorFunctor_obj, CategoryTheory.Join.InclLeftCompRightOpOpEquivFunctor_hom_app, CategoryTheory.Iso.isoFunctorOfIsoInverse_inv_app, counitInv_app_comp_functor_map_η_inverse, sheafCongrPreregular_counitIso_hom_app_val_app, CochainComplex.homotopyOp_hom_eq, CategoryTheory.Comma.toIdPUnitEquiv_counitIso_hom_app, CategoryTheory.Limits.opCospan_inv_app, congrLeft_unitIso_hom_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_left, sheafCongrPrecoherent_counitIso_inv_app_val_app, mapHomologicalComplex_functor, unitInv_app_inverse, CategoryTheory.CostructuredArrow.ofCommaFstEquivalence_functor, ext_iff, CategoryTheory.Monoidal.comonFunctorCategoryEquivalence_functor, symmEquivInverse_obj_counitIso_inv, CategoryTheory.Limits.PullbackCone.unop_ι_app, TopCat.Presheaf.generateEquivalenceOpensLe_functor, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality_assoc, CategoryTheory.Pretriangulated.mem_distTriang_op_iff', CategoryTheory.Comma.mapRightIso_functor_obj_left, OrderHom.equivalenceFunctor_functor_obj_obj, CategoryTheory.ForgetEnrichment.equiv_functor, Types.monoOverEquivalenceSet_functor_map, CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproducts_functor, changeFunctor_unitIso_inv_app, CategoryTheory.Monoidal.transportStruct_leftUnitor, CategoryTheory.ULift.equivalence_functor, CategoryTheory.Limits.reflexiveCoforkEquivCofork_functor_obj_π, CategoryTheory.Sieve.mem_functorPushforward_inverse, CategoryTheory.Monoidal.transportStruct_rightUnitor, CategoryTheory.Idempotents.DoldKan.η_inv_app_f, ContAction.resEquiv_functor, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_left_app, CategoryTheory.Discrete.equivOfEquivalence_apply, CategoryTheory.Functor.flipping_functor_obj_map_app, CategoryTheory.Comma.toPUnitIdEquiv_functor_iso, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_hom_app_app, IsTriangulated.instIsTriangulatedFunctorSymmOfInverse, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_hom_app, changeInverse_counitIso_hom_app, CategoryTheory.Join.opEquiv_functor_obj_op_left, groupAddGroupEquivalence_functor, CategoryTheory.StructuredArrow.mapIso_functor_obj_right, toAdjunction_counit, MonObj.mopEquiv_functor_map_hom_unmop, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_X_p, fun_inv_map, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_obj_π_app, CategoryTheory.MonoidalOpposite.mopMopEquivalence_functor_map, Bipointed.swapEquiv_functor_obj_X, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_naturality_assoc, MonObj.mopEquivCompForgetIso_inv_app_unmop, CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor, CategoryTheory.IsVanKampenColimit.whiskerEquivalence, CategoryTheory.prod.associativity_functor, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_obj, CategoryTheory.Limits.Cones.functorialityEquivalence_inverse, Types.monoOverEquivalenceSet_functor_obj, CategoryTheory.StructuredArrow.mapIso_functor_map_left, congrLeftFunctor_map, core_functor_obj_of, CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_inv_app_one, CategoryTheory.MonoOver.congr_functor, isEquivalence_functor, CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_functor_obj_hom_app, CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_hom_app_unop, CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor_inv_hom, CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso_isoBot, CategoryTheory.ComposableArrows.opEquivalence_functor_obj_obj, mapCommMon_counitIso, CategoryTheory.ObjectProperty.IsSeparating.of_equivalence, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₃, TopCat.Presheaf.presheafEquivOfIso_unitIso_inv_app_app, CategoryTheory.MonoidalOpposite.mopMopEquivalence_counitIso_inv_app, core_functor_map_iso_inv, CategoryTheory.Limits.walkingCospanOpEquiv_functor_map, CategoryTheory.eq_functor_map, CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_inv_app_unop_assoc, partialFunEquivPointed_functor_obj_X, CategoryTheory.MonoOver.congr_inverse, cancel_unit_right_assoc', CategoryTheory.Functor.fun_inv_map, CategoryTheory.Iso.isoCompInverse_inv_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_naturality, instIsCommMonObjOppositeCommAlgCatXUnopMonObjCommBialgCatFunctorCommBialgCatEquivComonCommAlgCatOfIsCocommCarrier, CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor_hom_hom, op_functor, CategoryTheory.Limits.Cocones.functorialityEquivalence_counitIso, HomologicalComplex₂.flipEquivalence_functor, mapMon_counitIso, CategoryTheory.Limits.Cone.equivCostructuredArrow_functor, CategoryTheory.Iso.isoInverseOfIsoFunctor_inv_app, core_counitIso_hom_app_iso_hom, inv_fun_map_assoc, TopCat.Presheaf.whiskerIsoMapGenerateCocone_hom_hom, inverse_counitInv_comp_assoc, sheafCongrPrecoherent_unitIso_inv_app_val_app, TopCat.Presheaf.presheafEquivOfIso_functor_obj_obj, symm_functor, trans_counitIso, CategoryTheory.Comma.toPUnitIdEquiv_unitIso_hom_app_left, CategoryTheory.CatCommSq.vInv_iso_inv_app, counitIso_inv_app_tensor_comp_functor_map_δ_inverse_assoc, changeFunctor_functor, CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_obj_V, CategoryTheory.Limits.Fork.op_ι_app, functor_map_ε_inverse_comp_counitIso_hom_app_assoc, CategoryTheory.IsVanKampenColimit.whiskerEquivalence_iff, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₂, CategoryTheory.WithInitial.equivComma_functor_obj_left, rightOp_functor_obj, map_η_comp_η_assoc, CategoryTheory.Functor.instIsWellOrderContinuousCompFunctorEquivalence, CategoryTheory.Limits.walkingCospanOpEquiv_functor_obj, CategoryTheory.Limits.IsColimit.ofCoconeEquiv_apply_desc, CategoryTheory.simplicialCosimplicialEquiv_functor_map_app, MonObj.mopEquiv_functor_obj_X_unmop, CategoryTheory.Limits.walkingSpanOpEquiv_functor_map, CategoryTheory.Adjunction.leftOp_eq, CategoryTheory.Discrete.sumEquiv_functor_obj, counitIso_inv_app_comp_functor_map_η_inverse_assoc, CategoryTheory.Subobject.lowerEquivalence_counitIso, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app_assoc, mapHomologicalComplex_counitIso, CategoryTheory.subterminalsEquivMonoOverTerminal_functor_map, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app, isLeftAdjoint_functor, CategoryTheory.CostructuredArrow.mapNatIso_functor_obj_left, CategoryTheory.orderDualEquivalence_functor_obj, CategoryTheory.Comma.opEquiv_functor, counitInv_app_functor, rightOp_counitIso_hom_app, CategoryTheory.Limits.Cones.functorialityEquivalence_counitIso, CategoryTheory.MonoidalOpposite.unmopEquiv_unitIso_hom_app_unmop, CategoryTheory.Sum.functorEquivFunctorCompSndIso_inv_app_app, CategoryTheory.Functor.flipping_functor_obj_obj_obj, CategoryTheory.Under.postEquiv_inverse, CategoryTheory.equivOfTensorIsoUnit_functor, CategoryTheory.Sum.functorEquiv_unitIso_inv_app_app_inr, counitInv_functor_comp_assoc, CategoryTheory.Over.ConstructProducts.conesEquiv_functor, functor_map_ε_inverse_comp_counit_app, CategoryTheory.Functor.currying₃_unitIso_inv_app_app_app_app, fun_inv_map_assoc, CategoryTheory.Functor.closedIhom_map_app, ε_comp_map_ε, CategoryTheory.CostructuredArrow.mapNatIso_functor_obj_right, CategoryTheory.ShiftedHom.opEquiv'_symm_op_opShiftFunctorEquivalence_counitIso_inv_app_op_shift, comp_asNatTrans_assoc, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_right, CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_hom_app_unop_assoc, SimplexCategory.revEquivalence_functor, CategoryTheory.Limits.Cocones.whiskeringEquivalence_functor, CategoryTheory.Functor.currying_functor_obj_obj, CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj_hom_app, CategoryTheory.Pi.optionEquivalence_functor, CategoryTheory.Functor.isLeftKanExtensionAlongEquivalence, unit_naturality_assoc, CategoryTheory.Limits.CategoricalPullback.functorEquiv_functor_obj_snd_obj, unit_app_tensor_comp_inverse_map_δ_functor_assoc, Action.tensorHom_hom, AlgebraicTopology.DoldKan.Compatibility.υ_hom_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_add_unitIso_inv_app_eq, Action.associator_hom_hom, CategoryTheory.MonoidalOpposite.mopMopEquivalence_unitIso_inv_app_unmop_unmop, CategoryTheory.Subobject.lowerEquivalence_unitIso, unit_naturality, CategoryTheory.Sieve.mem_functorPushforward_functor, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_hom_app_app, functor_unitIso_comp, CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_obj, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_right, ModuleCat.restrictScalarsEquivalenceOfRingEquiv_additive, CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_obj_val, MoritaEquivalence.instAdditiveModuleCatFunctorEqv, CategoryTheory.Pi.evalCompEqToEquivalenceFunctor_inv, CategoryTheory.orderDualEquivalence_functor_map, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_inv_app_app, CategoryTheory.Sieve.functorPushforward_functor, CategoryTheory.Limits.widePullbackShapeOpEquiv_functor, CategoryTheory.Limits.IsColimit.pushoutCoconeEquivBinaryCofanFunctor_desc_right, CategoryTheory.Groupoid.invEquivalence_functor_obj, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_mul, CategoryTheory.Pi.eqToEquivalenceFunctorIso_inv, sheafCongrPrecoherent_inverse_obj_val_map, core_counitIso_hom_app_iso_inv, sheafCongrPrecoherent_unitIso_hom_app_val_app, cancel_counitInv_right_assoc', CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_snd_fst, CategoryTheory.MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_δ, symm_counitIso, CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence_functor, CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso_F, mapMon_functor, AlgebraicTopology.DoldKan.Compatibility.τ₁_hom_app, CategoryTheory.Comma.mapLeftIso_functor_obj_hom, unit_app_comp_inverse_map_η_functor, TopCat.Presheaf.presheafEquivOfIso_counitIso_inv_app_app, CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_one, MonObj.mopEquiv_functor_obj_mon_mul_unmop, CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso_functor, functor_map_μ_inverse_comp_counit_app_tensor_assoc, Action.whiskerLeft_hom, core_unitIso_hom_app_iso_hom, CategoryTheory.Idempotents.DoldKan.isoN₁_hom_app_f, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_left, CategoryTheory.StructuredArrow.mapIso_functor_obj_hom, CategoryTheory.ObjectProperty.IsCoseparating.of_equivalence, CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_hom_app_fst, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_d_f, sheafCongrPreregular_inverse_obj_val_obj, CategoryTheory.WithTerminal.isLimitEquiv_apply_lift_left, rightOp_unitIso_inv_app, id_asNatTrans, CategoryTheory.Join.InclLeftCompRightOpOpEquivFunctor_inv_app, CategoryTheory.Over.postEquiv_unitIso, unit_app_inverse, CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence_hom, CategoryTheory.Iso.isoCompInverse_hom_app, CategoryTheory.Iso.isoInverseOfIsoFunctor_hom_app, CategoryTheory.ComposableArrows.opEquivalence_inverse_map, CategoryTheory.MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_η, CategoryTheory.typeEquiv_functor_map_val_app, CategoryTheory.Comon.monoidal_leftUnitor_inv_hom, CategoryTheory.Idempotents.karoubiUniversal₂_functor_eq, CategoryTheory.Functor.equiv_functor_map, HomologicalComplex.opEquivalence_functor, CategoryTheory.Functor.inv_fun_map, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_app_assoc, CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence_inv, sheafCongr.inverse_obj_val_map, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app_assoc, CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_zero, CategoryTheory.ObjectProperty.fullSubcategoryCongr_functor, CategoryTheory.Idempotents.DoldKan.equivalence_functor, NonemptyFinLinOrd.dualEquiv_functor, CategoryTheory.Pretriangulated.shift_unop_opShiftFunctorEquivalence_counitIso_hom_app, CategoryTheory.CostructuredArrow.prodEquivalence_functor, CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_functor, CategoryTheory.Comon.monoidal_rightUnitor_hom_hom, CategoryTheory.Join.InclRightCompRightOpOpEquivFunctor_inv_app, CategoryTheory.Square.arrowArrowEquivalence'_functor, CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_inv_hom₂, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_left, CategoryTheory.WithTerminal.equivComma_functor_map_left_app, CategoryTheory.Functor.flipping_functor_obj_obj_map, CategoryTheory.Abelian.DoldKan.equivalence_functor, mkHom_id_functor, counitInv_naturality, SSet.Truncated.HomotopyCategory.BinaryProduct.associativity, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_right, CategoryTheory.Pseudofunctor.DescentData.exists_equivalence_of_sieve_eq, unit_inverse_comp, CategoryTheory.prodOpEquiv_functor_map, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_inv_app_app, functor_map_μ_inverse_comp_counitIso_hom_app_tensor, CategoryTheory.Limits.Cones.equivalenceOfReindexing_unitIso, AddCommMonCat.equivalence_functor_obj_coe, CategoryTheory.CostructuredArrow.mapNatIso_functor_map_left, PartOrdEmb.dualEquiv_functor, CategoryTheory.Iso.inverseCompIso_inv_app, CategoryTheory.simplicialCosimplicialEquiv_functor_obj_obj, TopCat.Presheaf.presheafEquivOfIso_counitIso_hom_app_app, LinOrd.dualEquiv_functor, CategoryTheory.Iso.isoFunctorOfIsoInverse_hom_app, commAlgCatEquivUnder_functor_map, CategoryTheory.WithInitial.opEquiv_functor_obj, CategoryTheory.ShiftedHom.opEquiv_symm_apply, CategoryTheory.Idempotents.KaroubiKaroubi.equivalence_functor, CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_obj_str, CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_inv_app_snd, CategoryTheory.prodOpEquiv_functor_obj, AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso_hom_app, unit_app_comp_inverse_map_η_functor_assoc, CategoryTheory.StructuredArrow.mapNatIso_functor_obj_left, leftOp_counitIso_hom_app, CategoryTheory.Comma.toPUnitIdEquiv_counitIso_inv_app, CategoryTheory.Limits.walkingSpanOpEquiv_functor_obj, functor_map_μ_inverse_comp_counit_app_tensor, mapCommGrp_counitIso, CategoryTheory.MorphismProperty.inverseImage_equivalence_functor_eq_map_inverse, CategoryTheory.CostructuredArrow.overEquivPresheafCostructuredArrow_functor_map_toOverCompCoyoneda, Action.rightUnitor_hom_hom, core_counitIso_inv_app_iso_hom, CategoryTheory.Iso.inverseCompIso_hom_app, congrLeft_counitIso_hom_app, CategoryTheory.simplicialCosimplicialAugmentedEquiv_functor, AlgebraicTopology.DoldKan.Compatibility.τ₀_hom_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_right_map, CategoryTheory.Monad.monadMonEquiv_functor, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_right, CategoryTheory.StructuredArrow.mapIso_functor_map_right, CategoryTheory.Limits.Cocones.functorialityEquivalence_inverse, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_map, CategoryTheory.Sum.functorEquiv_unit_app_app_inl, CategoryTheory.CostructuredArrow.mapIso_functor_obj_right, CategoryTheory.MonoidalOpposite.unmopEquiv_counitIso_inv_app, sheafCongr.inverse_map_val_app, CategoryTheory.Discrete.sumEquiv_functor_map, CategoryTheory.MonoidalOpposite.unmopEquiv_functor_map, CategoryTheory.Abelian.DoldKan.comparisonN_hom_app_f, CategoryTheory.TwoSquare.equivalenceJ_functor, SSet.Truncated.HomotopyCategory.BinaryProduct.associativityIso_hom_app, CategoryTheory.equivToOverUnit_functor, CategoryTheory.Comon.monoidal_associator_inv_hom, CategoryTheory.Comma.toIdPUnitEquiv_counitIso_inv_app, Action.associator_inv_hom, CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_inv_app_unop, core_functor_map_iso_hom, AddMonCat.equivalence_functor_map, Action.resEquiv_functor, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_map_right_app, CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_inv_app_unop_assoc, unop_unitIso, trans_functor, CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_inverseImage_iff, CategoryTheory.isCardinalPresentable_of_equivalence, congrLeft_inverse, TopCat.Presheaf.presheafEquivOfIso_functor_map_app, symmEquivInverse_obj_unitIso_inv, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₁, CategoryTheory.Idempotents.KaroubiKaroubi.equivalence.additive_functor, CategoryTheory.Limits.Cones.equivalenceOfReindexing_functor, CategoryTheory.Comma.equivProd_functor_map, Action.functorCategoryEquivalence_linear, counitIso_inv_app_tensor_comp_functor_map_δ_inverse, CategoryTheory.piEquivalenceFunctorDiscrete_functor_map, unop_functor, CategoryTheory.MonoOver.congr_counitIso, AlgebraicTopology.DoldKan.Compatibility.equivalence₀_functor, op_unitIso, mkHom_comp, CategoryTheory.Over.opEquivOpUnder_functor_map, induced_functor, CategoryTheory.CatCommSq.hInv_iso_hom_app, CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_functor_obj, CategoryTheory.IsCoseparator.of_equivalence, mkIso_inv, Action.functorCategoryEquivalence_preservesZeroMorphisms, CategoryTheory.Under.postEquiv_functor, CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_left_inv_assoc, CategoryTheory.Subobject.lowerEquivalence_functor, CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv_functor_obj_none, CategoryTheory.Over.mapIso_functor, CategoryTheory.MonoidalClosed.ofEquiv_curry_def, changeInverse_unitIso_hom_app, CategoryTheory.Comma.mapLeftIso_functor_obj_right, Action.rightUnitor_inv_hom, CategoryTheory.CostructuredArrow.overEquivPresheafCostructuredArrow_inverse_map_toOverCompYoneda, congrRight_unitIso_hom_app, CategoryTheory.IsUniversalColimit.whiskerEquivalence_iff, partialFunEquivPointed_functor_obj_point, CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_hom_app_one, sheafCongrPrecoherent_functor_map_val_app, CategoryTheory.Functor.currying_functor_obj_map, CategoryTheory.Functor.leftOpRightOpEquiv_functor_map_app, CategoryTheory.skeletonEquivalence_functor, CategoryTheory.Monoidal.transportStruct_whiskerLeft, CategoryTheory.Discrete.productEquiv_functor_obj, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_fst, ε_comp_map_ε_assoc, SimplicialObject.opEquivalence_functor, core_unitIso_inv_app_iso_hom, CategoryTheory.Join.opEquiv_functor_map_op_inclLeft, MulEquiv.toSingleObjEquiv_functor_map, CategoryTheory.CostructuredArrow.mapNatIso_functor_map_right, CategoryTheory.WithTerminal.coneEquiv_functor_obj_pt, CategoryTheory.Under.opEquivOpOver_functor_map, sheafCongrPreregular_unitIso_inv_app_val_app, CategoryTheory.Limits.coconeEquivalenceOpConeOp_functor_map, trans_unitIso, CategoryTheory.Under.postEquiv_unitIso, CategoryTheory.Pretriangulated.triangleRotation_functor, sheafCongr.unitIso_inv_app_val_app, CategoryTheory.Sum.functorEquivFunctorCompSndIso_hom_app_app, CategoryTheory.ComposableArrows.opEquivalence_counitIso_hom_app_app, CategoryTheory.Sum.functorEquivFunctorCompFstIso_hom_app_app, CategoryTheory.ObjectProperty.topEquivalence_functor, CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_one, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_functor, CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_hom_app_unop_assoc, leftOp_functor_map, CategoryTheory.Limits.HasLimit.isoOfEquivalence_inv_π, AlgebraicTopology.DoldKan.Compatibility.equivalence₂_functor, funInvIdAssoc_inv_app, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_X_X, CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_map_coe, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_functor, CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork_functor_obj_ι, mkHom_comp_assoc, CategoryTheory.prod.functorProdToProdFunctorAssociator_inv_app, symmEquivInverse_obj_inverse, Action.functorCategoryEquivalence_additive, CategoryTheory.Limits.hasLimit_equivalence_comp, CategoryTheory.Comma.toIdPUnitEquiv_functor_iso, mapGrp_functor, CategoryTheory.Limits.opSpan_inv_app, CategoryTheory.subterminalsEquivMonoOverTerminal_functor_obj_obj, AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso_inv_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_inv_app_app, AlgebraicTopology.DoldKan.Compatibility.equivalence₂_inverse, op_counitIso, CategoryTheory.Functor.Initial.conesEquiv_functor, CategoryTheory.Comon.monoidal_tensorHom_hom, commBialgCatEquivComonCommAlgCat_functor_map_unop_hom, CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence_functor, CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_map, CategoryTheory.Limits.Cocone.equivStructuredArrow_functor, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_app_eq, toAdjunction_unit, CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_obj_snd, CategoryTheory.MonoidalOpposite.mopMopEquivalence_counitIso_hom_app, core_unitIso_inv_app_iso_inv, CategoryTheory.Discrete.productEquiv_functor_map, CategoryTheory.subterminals_to_monoOver_terminal_comp_forget, ModuleCat.Algebra.restrictScalarsEquivalenceOfRingEquiv_linear, mapCommMon_functor, CategoryTheory.algebraEquivUnder_functor, CategoryTheory.cosimplicialSimplicialEquiv_functor_obj_map, CategoryTheory.prod.prodFunctorToFunctorProdAssociator_hom_app_app, counitInv_app_tensor_comp_functor_map_δ_inverse_assoc, CategoryTheory.Preadditive.commGrpEquivalence_functor_map_hom_hom_hom, counitInv_naturality_assoc, instIsDenseSubsiteFunctor, CategoryTheory.Pretriangulated.shift_unop_opShiftFunctorEquivalence_counitIso_inv_app, CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalenceSymmHomEquiv_unop, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_app, CategoryTheory.Join.mapPairEquiv_functor, counit_app_functor, CommShift.instCommShiftHomFunctorUnitIso, CategoryTheory.Limits.Cocones.functorialityEquivalence_functor, CategoryTheory.MonoidalOpposite.mopEquiv_functor, alexDiscEquivPreord_functor, CategoryTheory.Pi.equivalenceOfEquiv_functor, CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_inv_app_op_one, sheafCongr.counitIso_inv_app_val_app, CategoryTheory.Sieve.functorPushforward_equivalence_eq_pullback, CategoryTheory.StructuredArrow.mapNatIso_functor_map_left, TopCat.Presheaf.presheafEquivOfIso_functor_obj_map, CategoryTheory.Limits.CategoricalPullback.mkNatIso_eq, CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_hom_app_unop, CategoryTheory.GradedObject.comapEquiv_functor, CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_hom_app_op_zero, pi_counitIso, symmEquivInverse_obj_unitIso_hom, CategoryTheory.Sum.Swap.equivalence_functor, CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_functor_map_right, CategoryTheory.Abelian.DoldKan.comparisonN_inv_app_f, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_hom_app, TopCat.Presheaf.presheafEquivOfIso_inverse_map_app, inverse_counitInv_comp, CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence_functor, CategoryTheory.Adjunction.toEquivalence_functor, CategoryTheory.Over.postEquiv_functor, core_counitIso_inv_app_iso_inv, FundamentalGroupoidFunctor.coneDiscreteComp_obj_mapCone, CategoryTheory.WithTerminal.opEquiv_functor_map, CategoryTheory.Join.InclRightCompRightOpOpEquivFunctor_hom_app, unit_app_tensor_comp_inverse_map_δ_functor, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_functor, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₂, CategoryTheory.Limits.Cocones.whiskeringEquivalence_counitIso, AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso_hom_app, CategoryTheory.Limits.Cocones.functorialityEquivalence_unitIso, BddLat.dualEquiv_functor, AlgebraicTopology.DoldKan.Compatibility.υ_inv_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_right_obj, congrRightFunctor_map, unit_inverse_comp_assoc, symm_inverse, congrRight_counitIso_inv_app, counit_naturality, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_one, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_obj, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_map_app_hom_hom, CategoryTheory.Comma.mapLeftIso_functor_map_right, CategoryTheory.Functor.currying_functor_map_app, CategoryTheory.Square.flipEquivalence_functor, Action.leftUnitor_hom_hom, CategoryTheory.Over.opEquivOpUnder_functor_obj, CategoryTheory.opOpEquivalence_functor, CategoryTheory.WithTerminal.widePullbackShapeEquiv_functor_obj, CategoryTheory.prod.functorProdToProdFunctorAssociator_hom_app, CategoryTheory.Comma.equivProd_functor_obj, congrRight_counitIso_hom_app, CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj_inv_app, CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalenceSymmHomEquiv_unop_assoc, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality, CategoryTheory.Idempotents.DoldKan.η_hom_app_f, CategoryTheory.simplicialCosimplicialEquiv_functor_obj_map, trans_toAdjunction, changeFunctor_counitIso_inv_app, CategoryTheory.MonoidalOpposite.unmopEquiv_functor_obj, CategoryTheory.Sum.functorEquiv_functor_obj, CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_apply_assoc, SSet.opEquivalence_functor, congrRight_unitIso_inv_app, functor_unit_comp_assoc, additive_inverse_of_FullyFaithful, symmEquivInverse_map_app, AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso_hom_app, CategoryTheory.Limits.CategoricalPullback.functorEquiv_functor_obj_snd_map, CategoryTheory.WithTerminal.coneEquiv_functor_map_hom, CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_functor_obj_right, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app_shift, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_app_assoc, CategoryTheory.prod.leftUnitorEquivalence_functor, CategoryTheory.Functor.isRightKanExtensionAlongEquivalence, CategoryTheory.Limits.parallelPairOpIso_hom_app_zero, FundamentalGroupoid.punitEquivDiscretePUnit_functor
functorFunctor 📖	CompOp	3 math math: functorFunctor_obj, inverseFunctorMapIso_symm_eq_isoInverseOfIsoFunctor, functorFunctor_map
instCategory 📖	CompOp	35 math math: symmEquivFunctor_obj, comp_asNatTrans, mkHom_id_inverse, inverseFunctor_obj, symmEquivInverse_obj_counitIso_hom, inverseFunctor_map, symmEquivFunctor_map, inverseFunctorObjIso_inv, mkIso_hom, congrLeftFunctor_obj, symmEquiv_functor, symmEquivInverse_obj_functor, functorFunctor_obj, symmEquivInverse_obj_counitIso_inv, inverseFunctorObj'_hom_app, inverseFunctorMapIso_symm_eq_isoInverseOfIsoFunctor, congrLeftFunctor_map, symmEquiv_counitIso, symmEquiv_unitIso, comp_asNatTrans_assoc, symmEquiv_inverse, id_asNatTrans, congrRightFunctor_obj, mkHom_id_functor, functorFunctor_map, inverseFunctorObjIso_hom, inverseFunctorObj'_inv_app, symmEquivInverse_obj_unitIso_inv, mkHom_comp, mkIso_inv, mkHom_comp_assoc, symmEquivInverse_obj_inverse, symmEquivInverse_obj_unitIso_hom, congrRightFunctor_map, symmEquivInverse_map_app
instInhabited 📖	CompOp	—
instPowInt 📖	CompOp	3 math math: pow_one, pow_zero, pow_neg_one
invFunIdAssoc 📖	CompOp	12 math math: CategoryTheory.Limits.Cones.equivalenceOfReindexing_inverse, congrLeft_counitIso_inv_app, CategoryTheory.Limits.Cones.whiskeringEquivalence_inverse, CategoryTheory.Limits.Cones.equivalenceOfReindexing_counitIso, CategoryTheory.Limits.Cones.whiskeringEquivalence_unitIso, invFunIdAssoc_hom_app, CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence_inv, invFunIdAssoc_inv_app, CategoryTheory.Limits.Cones.whiskeringEquivalence_counitIso, CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence_hom, CategoryTheory.Limits.Cones.equivalenceOfReindexing_unitIso, congrLeft_counitIso_hom_app
inverse 📖	CompOp	869 math math: CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_app_eq, CategoryTheory.MorphismProperty.inverseImage_equivalence_inverse_eq_map_functor, prod_unitIso, CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_hom_app_zero, CategoryTheory.Sum.natTransOfWhiskerLeftInlInr_app, leftOp_unitIso_hom_app, sheafCongrPrecoherent_counitIso_hom_app_val_app, CategoryTheory.ComposableArrows.opEquivalence_counitIso_inv_app_app, preregular_isSheaf_iff, CategoryTheory.Adjunction.toEquivalence_inverse, CategoryTheory.Limits.IsLimit.ofConeEquiv_symm_apply_desc, AlgebraicTopology.DoldKan.Compatibility.equivalence₀_unitIso_hom_app, CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalence_counitIso_inv_app, sheafCongr.counitIso_hom_app_val_app, isLeftAdjoint_inverse, congrFullSubcategory_inverse, CategoryTheory.Comma.mapLeftIso_inverse_map_right, CategoryTheory.sum.associativity_inverse, mapGrp_counitIso, CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ_hom_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_add_unitIso_hom_app_eq, sheafCongrPreregular_counitIso_inv_app_val_app, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_X_d, CategoryTheory.Pretriangulated.Opposite.mem_distinguishedTriangles_iff, isEquivalence_inverse, CategoryTheory.Join.mapPairEquiv_inverse, CategoryTheory.Groupoid.invEquivalence_inverse_map, mapMon_inverse, AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso_inv_app, CategoryTheory.Limits.walkingSpanOpEquiv_inverse_map, unitIso_hom_app_comp_inverse_map_η_functor_assoc, CategoryTheory.MonoOver.congr_unitIso, counitInv_app_tensor_comp_functor_map_δ_inverse, CategoryTheory.Limits.Cones.equivalenceOfReindexing_inverse, isDenseSubsite_inverse_of_isCocontinuous, counitIso_inv_app_comp_functor_map_η_inverse, BddDistLat.dualEquiv_inverse, CategoryTheory.Idempotents.KaroubiKaroubi.equivalence.additive_inverse, CategoryTheory.Limits.HasColimit.isoOfEquivalence_inv_π, CategoryTheory.Monoidal.transportStruct_associator, CategoryTheory.Comma.toIdPUnitEquiv_inverse_map_right, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_map_app, CategoryTheory.Over.mapIso_inverse, CategoryTheory.WithInitial.isColimitEquiv_apply_desc_right, CategoryTheory.Join.mapPairEquiv_unitIso, CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse, CategoryTheory.Join.mapPairEquiv_counitIso, mapCommMon_inverse, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_inverse, rightOp_counitIso_inv_app, Bipointed.swapEquiv_inverse_obj_toProd, CategoryTheory.Limits.widePushoutShapeOpEquiv_inverse, CategoryTheory.MonoidalClosed.ofEquiv_uncurry_def, CategoryTheory.CatCommSq.hInv_iso_inv_app, leftOp_unitIso_inv_app, CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence_inverse, alexDiscEquivPreord_inverse_obj_carrier, CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_obj_obj_iso_inv, faithful_inverse, CategoryTheory.StructuredArrow.mapIso_inverse_obj_hom, CategoryTheory.Join.inclRightCompOpEquivInverse_inv_app_op, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_left, CategoryTheory.WithTerminal.opEquiv_inverse_obj, core_inverse_map_iso_hom, CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_obj_map_snd, ModuleCat.matrixEquivalence_inverse, CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_hom_app_op_one, CondensedMod.isDiscrete_tfae, CategoryTheory.piEquivalenceFunctorDiscrete_inverse_obj, CategoryTheory.prodOpEquiv_inverse_map, AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso_hom_app, Action.functorCategoryEquivalence_inverse, AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso_inv_app, precoherent_isSheaf_iff_of_essentiallySmall, CategoryTheory.CostructuredArrow.mapNatIso_inverse_obj_left, CategoryTheory.simplicialCosimplicialEquiv_inverse_map, CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_left_inv, CategoryTheory.Iso.isoInverseComp_inv_app, CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_map_base, CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_obj_str, prod_counitIso, CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso_inverse, Action.leftUnitor_inv_hom, CategoryTheory.WithTerminal.coneEquiv_inverse_obj_π_app_left, AlgebraicTopology.DoldKan.Compatibility.equivalence_functor, leftOp_counitIso_inv_app, CategoryTheory.Monoidal.instIsMonoidalUnitTransportedEquivalenceTransported, CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_inv_app_op_zero, AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso_hom_app, FinBoolAlg.dualEquiv_inverse, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_inverse_obj, cancel_unit_right, CategoryTheory.WithInitial.coconeEquiv_inverse_obj_pt_right, CategoryTheory.Functor.currying_inverse_obj_obj_obj, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_p_f, AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso_hom_app, pi_inverse, CategoryTheory.Comon.monoidal_rightUnitor_inv_hom, CategoryTheory.MonoidalOpposite.mopMopEquivalenceInverseMonoidal_ε_unmop_unmop, CategoryTheory.Monad.algebraEquivOfIsoMonads_inverse, congrFullSubcategory_counitIso, cancel_counit_right, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_right, MulEquiv.toSingleObjEquiv_inverse_map, CategoryTheory.Functor.currying₃_unitIso_hom_app_app_app_app, CategoryTheory.Monoidal.transportStruct_tensorHom, CategoryTheory.Idempotents.functorExtension_map_app, unitInv_naturality, CategoryTheory.WithTerminal.equivComma_inverse_obj_obj, functor_unit_comp, Action.whiskerRight_hom, inv_fun_map, CategoryTheory.WithInitial.isColimitEquiv_symm_apply_desc, CategoryTheory.CostructuredArrow.mapNatIso_inverse_map_right, CategoryTheory.functorProdFunctorEquiv_inverse, sheafCongrPreregular_unitIso_hom_app_val_app, CategoryTheory.Sieve.pullback_functorPushforward_equivalence_eq, CategoryTheory.CostructuredArrow.overEquivPresheafCostructuredArrow_inverse_map_toOverCompCoyoneda, CategoryTheory.Iso.isoInverseComp_hom_app, CategoryTheory.Sum.Swap.equivalence_inverse, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_map_app, CategoryTheory.Discrete.sumEquiv_inverse_map, CategoryTheory.Comma.mapRightIso_inverse_map_right, core_unitIso_hom_app_iso_inv, CategoryTheory.prod.associativity_inverse, CategoryTheory.Limits.Cocones.whiskeringEquivalence_unitIso, CategoryTheory.Sum.functorEquiv_unit_app_app_inr, CategoryTheory.Monoidal.transportStruct_tensorObj, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_single, AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso_inv_app, CategoryTheory.Sum.functorEquiv_unitIso_inv_app_app_inl, CategoryTheory.Limits.Cocones.whiskeringEquivalence_inverse, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₂, CoalgCat.comonEquivalence_inverse, CategoryTheory.Functor.flipping_inverse_obj_obj_map, CategoryTheory.Comma.toPUnitIdEquiv_counitIso_hom_app, mkHom_id_inverse, Rep.homEquiv_apply_hom, CategoryTheory.MonoidalOpposite.unmopEquiv_inverse_map_unmop, Types.monoOverEquivalenceSet_inverse_map, CategoryTheory.MonoidalCategory.DayFunctor.equiv_inverse_obj_functor, sheafCongrPreregular_inverse_obj_val_map, SSet.opEquivalence_inverse, congrLeft_counitIso_inv_app, CategoryTheory.Limits.HasColimit.isoOfEquivalence_hom_π, inverseFunctor_obj, alexDiscEquivPreord_inverse_obj_str, CategoryTheory.Monoidal.instIsMonoidalTransportedCounitEquivalenceTransported, symm_unitIso, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_naturality_assoc, mapHomologicalComplex_unitIso, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_mul_app, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_p_f, CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_zero, funInvIdAssoc_hom_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_naturality, CategoryTheory.WithInitial.coconeEquiv_inverse_obj_pt_hom, AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso_inv_app, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_inverse_map_hom, CategoryTheory.MonoidalOpposite.mopMopEquivalence_unitIso_hom_app_unmop_unmop, CategoryTheory.Comma.mapLeftIso_inverse_obj_left, CategoryTheory.CostructuredArrow.mapIso_inverse_obj_right, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_naturality, AddMonCat.equivalence_inverse_map, CategoryTheory.ObjectProperty.fullSubcategoryCongr_inverse, CategoryTheory.shiftEquiv'_inverse, refl_inverse, Rep.MonoidalClosed.linearHomEquivComm_hom, CategoryTheory.MonoidalCategory.DayFunctor.equiv_inverse_map_natTrans, sheafCongrPrecoherent_functor_obj_val_obj, changeInverse_inverse, CategoryTheory.Limits.spanOp_hom_app, CategoryTheory.Localization.equivalence_counitIso_app, Preord.dualEquiv_inverse, AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso_inv_app, CategoryTheory.Join.opEquiv_inverse_map_inclRight_op, CategoryTheory.Sum.functorEquiv_inverse_map, CategoryTheory.Over.opEquivOpUnder_inverse_obj, CategoryTheory.Limits.widePullbackShapeOpEquiv_inverse, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_obj_map, CategoryTheory.Functor.currying_inverse_obj_obj_map, CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_inverse, CategoryTheory.Comma.mapLeftIso_inverse_obj_right, CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_inverse_map_left, CategoryTheory.MonoidalOpposite.unmopEquiv_inverse_obj_unmop, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_obj_obj, CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_inverse_obj_left, cancel_counitInv_right, ContAction.resEquiv_inverse, CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_inv_app_unop, changeFunctor_unitIso_hom_app, CategoryTheory.ComposableArrows.opEquivalence_unitIso_inv_app, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₃, map_η_comp_η, counit_naturality_assoc, CategoryTheory.StructuredArrow.mapIso_inverse_obj_right, CategoryTheory.StructuredArrow.mapNatIso_inverse_map_right, CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_obj_a, CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence_inverse, Bipointed.swapEquiv_inverse_map_toFun, Bipointed.swapEquiv_inverse_obj_X, CategoryTheory.Limits.IsColimit.ofCoconeEquiv_symm_apply_desc, CategoryTheory.Limits.PullbackCone.op_ι_app, AlgebraicTopology.DoldKan.Compatibility.equivalence₀_inverse, TopCat.Presheaf.presheafEquivOfIso_inverse_obj_map, CategoryTheory.typeEquiv_inverse_obj, symmEquivInverse_obj_counitIso_hom, CategoryTheory.Idempotents.DoldKan.N₂_map_isoΓ₀_hom_app_f, inverseFunctor_map, CategoryTheory.CostructuredArrow.ofCommaFstEquivalence_inverse, functor_map_μ_inverse_comp_counitIso_hom_app_tensor_assoc, sheafCongrPreregular_functor_obj_val_obj, CategoryTheory.skeletonEquivalence_inverse, alexDiscEquivPreord_inverse_map, CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork_inverse_obj_ι, CategoryTheory.Limits.Cone.equivCostructuredArrow_inverse, CategoryTheory.Limits.Cones.whiskeringEquivalence_inverse, sheafCongrPreregular_functor_map_val_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_naturality_assoc, CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_map_val, CategoryTheory.Adjunction.Equivalence.instIsMonoidalCounit, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app_shift, CategoryTheory.Limits.opParallelPairIso_hom_app_zero, CategoryTheory.Limits.walkingCospanOpEquiv_inverse_obj, CategoryTheory.StructuredArrow.mapNatIso_inverse_obj_left, TwoP.swapEquiv_inverse_obj_X, CategoryTheory.Limits.walkingSpanOpEquiv_inverse_obj, CategoryTheory.Subfunctor.equivalenceMonoOver_inverse_map, CategoryTheory.Comon.monoidal_whiskerLeft_hom, CategoryTheory.StructuredArrow.preEquivalence_inverse, CategoryTheory.MonoidalOpposite.mopMopEquivalence_inverse_map_unmop_unmop, mapMon_unitIso, pi_unitIso, counitInv_functor_comp, CategoryTheory.Mon.limit_mon_mul, sheafCongrPreregular_inverse_map_val_app, sheafCongrPrecoherent_functor_obj_val_map, CategoryTheory.WithInitial.opEquiv_inverse_obj, rightOp_inverse_map, CategoryTheory.Idempotents.functorExtension_obj_obj, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_obj, CategoryTheory.Adjunction.Equivalence.instIsMonoidalUnit, CategoryTheory.Over.opEquivOpUnder_inverse_map, CategoryTheory.Limits.opParallelPairIso_hom_app_one, symmEquivFunctor_map, sheafCongrPreregular_functor_obj_val_map, CategoryTheory.Over.equivalenceOfIsTerminal_inverse_map, CategoryTheory.Over.postEquiv_inverse, CategoryTheory.Limits.instHasColimitDiscreteOppositeCompInverseOppositeOpFunctor, CategoryTheory.Pseudofunctor.DescentData.pullFunctorEquivalence_inverse, CategoryTheory.CostructuredArrow.prodEquivalence_inverse, CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_map_app_snd, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_map_hom, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_app, CategoryTheory.eq_inverse_obj, unitIso_hom_app_tensor_comp_inverse_map_δ_functor, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_one_app, CategoryTheory.prod.rightUnitorEquivalence_inverse, CategoryTheory.Comon.monoidal_leftUnitor_hom_hom, CategoryTheory.Square.flipEquivalence_inverse, sheafCongrPrecoherent_inverse_map_val_app, CategoryTheory.Limits.spanOp_inv_app, rightOp_unitIso_hom_app, CategoryTheory.Groupoid.invEquivalence_inverse_obj, CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInrIso_inv_app_app, CategoryTheory.Limits.colimitLimitToLimitColimitCone_hom, unitIso_hom_app_tensor_comp_inverse_map_δ_functor_assoc, CategoryTheory.Comma.equivProd_inverse_map_left, CategoryTheory.cosimplicialSimplicialEquiv_inverse_obj, CategoryTheory.Limits.Cones.equivalenceOfReindexing_counitIso, CategoryTheory.monoOver_terminal_to_subterminals_comp, CommShift.instCommShiftHomFunctorCounitIso, congrLeft_functor, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_zero_unitIso_inv_app, CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalence_counitIso_inv_app_assoc, CategoryTheory.opOpEquivalence_inverse, CategoryTheory.Iso.compInverseIso_inv_app, TopCat.Presheaf.presheafEquivOfIso_unitIso_hom_app_app, unitInv_naturality_assoc, CategoryTheory.CatCommSq.vInv_iso_hom_app, CategoryTheory.Sum.natIsoOfWhiskerLeftInlInr_eq, CategoryTheory.sheafBotEquivalence_inverse_map_val, Action.diagonalSuccIsoTensorTrivial_inv_hom_apply, CategoryTheory.Comma.toIdPUnitEquiv_unitIso_inv_app_right, CategoryTheory.Limits.Cones.whiskeringEquivalence_unitIso, CategoryTheory.Comma.toPUnitIdEquiv_unitIso_inv_app_left, CategoryTheory.Join.opEquiv_inverse_obj_right_op, CategoryTheory.MonoidalOpposite.unmopEquiv_unitIso_inv_app_unmop, changeFunctor_counitIso_hom_app, AddMonCat.equivalence_inverse_obj_coe, CategoryTheory.Subfunctor.equivalenceMonoOver_inverse_obj, CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_inverse_obj, CategoryTheory.Limits.IsLimit.ofConeEquiv_apply_desc, CategoryTheory.Limits.HasLimit.isoOfEquivalence_hom_π, CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_obj_base, CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_inverse, CategoryTheory.Under.postEquiv_counitIso, CategoryTheory.WithTerminal.coneEquiv_inverse_obj_pt_left, counitInv_app_comp_functor_map_η_inverse_assoc, sheafCongrPrecoherent_inverse_obj_val_obj, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_left_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app, unop_counitIso, CategoryTheory.Idempotents.DoldKan.equivalence_inverse, CategoryTheory.AsSmall.equiv_inverse, CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInlIso_hom_app_app, mapGrp_inverse, CategoryTheory.ComposableArrows.opEquivalence_inverse_obj, mapCommGrp_unitIso, cancel_unitInv_right, invFunIdAssoc_hom_app, CategoryTheory.Limits.pullbackConeEquivBinaryFan_inverse_obj, unitIso_hom_app_comp_inverse_map_η_functor, CategoryTheory.algebraEquivUnder_inverse, CategoryTheory.Iso.compInverseIso_hom_app, CategoryTheory.sheafBotEquivalence_inverse_obj_val, CategoryTheory.WithInitial.coconeEquiv_inverse_obj_pt_left_as, MonObj.mopEquiv_inverse_map_hom, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_inverse, CategoryTheory.Limits.Cones.functorialityEquivalence_unitIso, functor_map_ε_inverse_comp_counit_app_assoc, CategoryTheory.Sieve.functorPushforward_inverse, congrFullSubcategory_unitIso, inverseFunctorObjIso_inv, changeInverse_counitIso_inv_app, CategoryTheory.subterminalsEquivMonoOverTerminal_inverse_map, CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_inverse_map_right, AlgebraicTopology.DoldKan.compatibility_N₂_N₁_karoubi, mapCommMon_unitIso, instIsDenseSubsiteInducedTopologyInverseFunctor, CategoryTheory.Square.arrowArrowEquivalence_inverse, changeInverse_unitIso_inv_app, CategoryTheory.Over.equivalenceOfIsTerminal_inverse_obj, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_zero_unitIso_hom_app, rightOp_inverse_obj, MulEquiv.toSingleObjEquiv_inverse_obj, CategoryTheory.WithInitial.equivComma_inverse_map_app, CategoryTheory.Comon.monoidal_whiskerRight_hom, CategoryTheory.Functor.IsDenseSubsite.sheafEquiv_inverse, CategoryTheory.CostructuredArrow.mapNatIso_inverse_map_left, CategoryTheory.WithTerminal.isLimitEquiv_symm_apply_lift, CategoryTheory.Cat.opEquivalence_inverse, CategoryTheory.Comma.toIdPUnitEquiv_unitIso_hom_app_right, functor_map_ε_inverse_comp_counitIso_hom_app, CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_inverse_map, CategoryTheory.TwoSquare.equivalenceJ_inverse, CategoryTheory.ComposableArrows.opEquivalence_unitIso_hom_app, MonObj.mopEquiv_inverse_obj_X, CategoryTheory.Comma.mapRightIso_inverse_obj_right, CategoryTheory.Pretriangulated.mem_distTriang_op_iff, CategoryTheory.Functor.opUnopEquiv_inverse, CategoryTheory.Idempotents.KaroubiKaroubi.equivalence_inverse, PartOrdEmb.dualEquiv_inverse, symmEquivInverse_obj_functor, cancel_counitInv_right_assoc, CategoryTheory.Join.opEquiv_inverse_map_inclLeft_op, CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_apply, CategoryTheory.WithTerminal.coneEquiv_inverse_obj_pt_hom, CategoryTheory.Over.postEquiv_counitIso, CategoryTheory.WithInitial.coconeEquiv_inverse_obj_ι_app_right, CategoryTheory.Endofunctor.Algebra.equivOfNatIso_inverse, CategoryTheory.CategoryOfElements.structuredArrowEquivalence_inverse, CategoryTheory.Comma.toIdPUnitEquiv_inverse_obj_left_as, sheafCongr.unitIso_hom_app_val_app, CategoryTheory.Comon.monoidal_associator_hom_hom, CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_inverse_obj_right, CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence_inv, TopologicalSpace.Opens.mapMapIso_inverse, invFunIdAssoc_inv_app, CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_inv_app_zero, CategoryTheory.toOverIteratedSliceForwardIsoPullback_hom_app_left, CategoryTheory.Monoidal.transportStruct_whiskerRight, induced_inverse_map, CategoryTheory.Functor.Initial.conesEquiv_inverse, groupAddGroupEquivalence_inverse, CategoryTheory.Limits.Cones.whiskeringEquivalence_counitIso, CategoryTheory.StructuredArrow.mapNatIso_inverse_obj_hom, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_right, CategoryTheory.Limits.PushoutCocone.op_π_app, congrLeft_unitIso_inv_app, CategoryTheory.MonoidalOpposite.unmopEquiv_counitIso_hom_app, CategoryTheory.Adjunction.rightOp_eq, CategoryTheory.Idempotents.DoldKan.N_obj, cancel_unit_right_assoc, mapGrp_unitIso, CategoryTheory.Functor.leftOpRightOpEquiv_inverse_map, CategoryTheory.Iso.isoFunctorOfIsoInverse_inv_app, CategoryTheory.CostructuredArrow.mapNatIso_inverse_obj_hom, counitInv_app_comp_functor_map_η_inverse, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_X_X, CategoryTheory.WithInitial.equivComma_inverse_obj_map, sheafCongrPreregular_counitIso_hom_app_val_app, CategoryTheory.prod.leftUnitorEquivalence_inverse, CategoryTheory.Comma.toIdPUnitEquiv_counitIso_hom_app, congrLeft_unitIso_hom_app, sheafCongrPrecoherent_counitIso_inv_app_val_app, partialFunEquivPointed_inverse_obj, unitInv_app_inverse, sheafCongr.functor_map_val_app, CategoryTheory.ForgetEnrichment.equiv_inverse, ext_iff, CategoryTheory.Comma.toPUnitIdEquiv_inverse_map_left, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence_inverse, symmEquivInverse_obj_counitIso_inv, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality_assoc, CategoryTheory.Join.inclRightCompOpEquivInverse_hom_app_op, CategoryTheory.Limits.cospanOp_hom_app, changeFunctor_unitIso_inv_app, AddCommMonCat.equivalence_inverse_obj_coe, CategoryTheory.Monoidal.transportStruct_leftUnitor, inverseFunctorObj'_hom_app, CategoryTheory.Sieve.mem_functorPushforward_inverse, CategoryTheory.Monoidal.transportStruct_rightUnitor, CategoryTheory.Idempotents.DoldKan.η_inv_app_f, CategoryTheory.typeEquiv_inverse_map, CategoryTheory.Comma.equivProd_inverse_map_right, Lat.dualEquiv_inverse, commAlgCatEquivUnder_inverse_obj_carrier, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_left_app, BoolAlg.dualEquiv_inverse, CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_inverse_obj_hom_app, leftOp_inverse_map, CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_inverse, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_inverse, boolRingCatEquivBoolAlg_inverse, CategoryTheory.Under.mapIso_inverse, changeInverse_counitIso_hom_app, toAdjunction_counit, CategoryTheory.Join.opEquiv_inverse_obj_left_op, fun_inv_map, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_naturality_assoc, CategoryTheory.subterminalsEquivMonoOverTerminal_inverse_obj_obj, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_map_f_f, CategoryTheory.Limits.reflexiveCoforkEquivCofork_inverse_obj_pt, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_obj, CategoryTheory.Limits.Cones.functorialityEquivalence_inverse, CategoryTheory.Limits.instHasLimitDiscreteOppositeCompInverseOppositeOpFunctor, congrLeftFunctor_map, CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_inv_app_one, CategoryTheory.Join.inclLeftCompOpEquivInverse_inv_app_op, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_map_hom_hom_app, CategoryTheory.HasExactColimitsOfShape.of_codomain_equivalence, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_inverse_obj_pt, CategoryTheory.Comma.mapLeftIso_inverse_obj_hom, CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_hom_app_unop, mapCommMon_counitIso, CategoryTheory.Square.arrowArrowEquivalence'_inverse, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_map_f_f, TopCat.Presheaf.presheafEquivOfIso_unitIso_inv_app_app, SemilatSupCatEquivSemilatInfCat_inverse, CategoryTheory.MonoidalOpposite.mopMopEquivalence_counitIso_inv_app, CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_inv_app_unop_assoc, CategoryTheory.MonoOver.congr_inverse, cancel_unit_right_assoc', CategoryTheory.Functor.fun_inv_map, CategoryTheory.Iso.isoCompInverse_inv_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_naturality, CategoryTheory.Limits.Cocones.functorialityEquivalence_counitIso, CategoryTheory.WithTerminal.widePullbackShapeEquiv_inverse_obj, mapMon_counitIso, CategoryTheory.Comma.equivProd_inverse_obj_right, sheafCongr.functor_obj_val_map, CategoryTheory.forgetEnrichmentOppositeEquivalence_inverse, CompleteLat.dualEquiv_inverse, CategoryTheory.Iso.isoInverseOfIsoFunctor_inv_app, CategoryTheory.GradedObject.comapEquiv_inverse, CategoryTheory.Limits.Fork.equivOfIsos_inverse_obj_ι, core_counitIso_hom_app_iso_hom, inv_fun_map_assoc, inverse_counitInv_comp_assoc, sheafCongrPrecoherent_unitIso_inv_app_val_app, induced_inverse_obj, core_inverse_map_iso_inv, symm_functor, trans_counitIso, CategoryTheory.Comma.toPUnitIdEquiv_unitIso_hom_app_left, CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence_inverse_map, CategoryTheory.CatCommSq.vInv_iso_inv_app, counitIso_inv_app_tensor_comp_functor_map_δ_inverse_assoc, functor_map_ε_inverse_comp_counitIso_hom_app_assoc, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_inverse, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_obj_π_app, map_η_comp_η_assoc, FinPartOrd.dualEquiv_inverse, CategoryTheory.simplicialCosimplicialEquiv_inverse_obj, CategoryTheory.Limits.IsColimit.ofCoconeEquiv_apply_desc, CondensedSet.isDiscrete_tfae, precoherent_isSheaf_iff, HomologicalComplex₂.flipEquivalence_inverse, CategoryTheory.Adjunction.leftOp_eq, CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInrIso_hom_app_app, CategoryTheory.ShortComplex.opEquiv_inverse, counitIso_inv_app_comp_functor_map_η_inverse_assoc, CategoryTheory.Subobject.lowerEquivalence_counitIso, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app_assoc, mapHomologicalComplex_counitIso, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app, CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_obj_map_fst, CategoryTheory.Monad.monadMonEquiv_inverse, CategoryTheory.Abelian.DoldKan.equivalence_inverse, counitInv_app_functor, CategoryTheory.Functor.flipping_inverse_obj_map_app, inverseLinear, rightOp_counitIso_hom_app, CategoryTheory.Limits.Cones.functorialityEquivalence_counitIso, CategoryTheory.Pretriangulated.unop_distinguished, CategoryTheory.MonoidalOpposite.unmopEquiv_unitIso_hom_app_unmop, CategoryTheory.Under.postEquiv_inverse, SSet.Truncated.HomotopyCategory.BinaryProduct.associativity'Iso_hom_app, CategoryTheory.Sum.functorEquiv_unitIso_inv_app_app_inr, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_inverse_obj_ι_app, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_obj_pt, TwoP.swapEquiv_inverse_obj_toTwoPointing_toProd, counitInv_functor_comp_assoc, CategoryTheory.Join.inclLeftCompOpEquivInverse_hom_app_op, functor_map_ε_inverse_comp_counit_app, CategoryTheory.Functor.currying₃_unitIso_inv_app_app_app_app, fun_inv_map_assoc, CategoryTheory.Comma.toPUnitIdEquiv_inverse_obj_right_as, ε_comp_map_ε, CategoryTheory.ShiftedHom.opEquiv'_symm_op_opShiftFunctorEquivalence_counitIso_inv_app_op_shift, core_inverse_obj_of, instIsDenseSubsiteRegularTopologyInverse, CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_hom_app_unop_assoc, CategoryTheory.Pi.optionEquivalence_inverse, AlgebraicTopology.DoldKan.Compatibility.equivalence_inverse, mapCommGrp_inverse, CategoryTheory.WithInitial.equivComma_inverse_obj_obj, CategoryTheory.RelCat.opEquivalence_inverse, unit_naturality_assoc, unit_app_tensor_comp_inverse_map_δ_functor_assoc, Action.tensorHom_hom, AlgebraicTopology.DoldKan.Compatibility.υ_hom_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_add_unitIso_inv_app_eq, Action.associator_hom_hom, CategoryTheory.MonoidalOpposite.mopMopEquivalence_unitIso_inv_app_unmop_unmop, CategoryTheory.equivOfTensorIsoUnit_inverse, CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv_inverse, CategoryTheory.Subobject.lowerEquivalence_unitIso, unit_naturality, CategoryTheory.Sieve.mem_functorPushforward_functor, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_hom_app_app, functor_unitIso_comp, CategoryTheory.Sheaf.isConstant_iff_of_equivalence, CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_obj, eq_inducedTopology_of_isDenseSubsite, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_right, CategoryTheory.Prod.braiding_inverse, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_inv_app_app, CategoryTheory.Sieve.functorPushforward_functor, CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_obj_obj_iso_hom, CategoryTheory.Preadditive.DoldKan.equivalence_inverse, OrderIso.equivalence_inverse, CategoryTheory.MonoidalOpposite.mopMopEquivalenceInverseMonoidal_δ_unmop_unmop, sheafCongrPrecoherent_inverse_obj_val_map, TopologicalSpace.Opens.coe_overEquivalence_inverse_obj_left, CategoryTheory.Comma.toPUnitIdEquiv_inverse_obj_left, core_counitIso_hom_app_iso_inv, sheafCongrPrecoherent_unitIso_hom_app_val_app, OrderHom.equivalenceFunctor_inverse_obj, TwoP.swapEquiv_inverse_map_hom_toFun, cancel_counitInv_right_assoc', CategoryTheory.piEquivalenceFunctorDiscrete_inverse_map, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_inverse_obj, CategoryTheory.Join.opEquiv_inverse_map_edge_op, symm_counitIso, commAlgCatEquivUnder_inverse_map, CategoryTheory.Discrete.productEquiv_inverse_obj_as, AlgebraicTopology.DoldKan.Compatibility.τ₁_hom_app, unit_app_comp_inverse_map_η_functor, TopCat.Presheaf.presheafEquivOfIso_counitIso_inv_app_app, CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_one, CategoryTheory.Limits.Cocone.equivStructuredArrow_inverse, PartOrd.dualEquiv_inverse, CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproducts_inverse, CategoryTheory.equivToOverUnit_inverse, functor_map_μ_inverse_comp_counit_app_tensor_assoc, CategoryTheory.WithInitial.coconeEquiv_inverse_map_hom_right, IsTriangulated.instIsTriangulatedInverseSymmOfFunctor, Action.whiskerLeft_hom, changeFunctor_inverse, core_unitIso_hom_app_iso_hom, symmEquiv_inverse, inverse_additive, NonemptyFinLinOrd.dualEquiv_inverse, sheafCongrPreregular_inverse_obj_val_obj, CategoryTheory.WithTerminal.isLimitEquiv_apply_lift_left, rightOp_unitIso_inv_app, CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_map_app_fst, Rep.MonoidalClosed.linearHomEquiv_hom, CategoryTheory.Over.postEquiv_unitIso, CategoryTheory.prodOpEquiv_inverse_obj, CategoryTheory.equivEssImageOfReflective_inverse, CategoryTheory.Idempotents.functorExtension_obj_map, unit_app_inverse, CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence_hom, CategoryTheory.Iso.isoCompInverse_hom_app, CategoryTheory.Iso.isoInverseOfIsoFunctor_hom_app, CategoryTheory.ComposableArrows.opEquivalence_inverse_map, CategoryTheory.Comon.monoidal_leftUnitor_inv_hom, CategoryTheory.Limits.reflexiveCoforkEquivCofork_inverse_obj_π, CategoryTheory.Functor.inv_fun_map, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_app_assoc, CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_obj_fiber_as, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app_assoc, CategoryTheory.Functor.flipping_inverse_map_app_app, CategoryTheory.Comma.mapRightIso_inverse_obj_hom, CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_zero, CategoryTheory.StructuredArrow.mapIso_inverse_map_right, CategoryTheory.Pretriangulated.shift_unop_opShiftFunctorEquivalence_counitIso_hom_app, CategoryTheory.Idempotents.karoubiUniversal₁_inverse, CategoryTheory.Discrete.sumEquiv_inverse_obj, CategoryTheory.Comon.monoidal_rightUnitor_hom_hom, Types.monoOverEquivalenceSet_inverse_obj, SimplicialObject.opEquivalence_inverse, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_inverse, Rep.homEquiv_symm_apply_hom, counitInv_naturality, CategoryTheory.Comma.opEquiv_inverse, AlgebraicTopology.DoldKan.Compatibility.equivalence₁_inverse, unit_inverse_comp, CategoryTheory.CostructuredArrow.mapNatIso_inverse_obj_right, CategoryTheory.coalgebraEquivOver_inverse, functor_map_μ_inverse_comp_counitIso_hom_app_tensor, CategoryTheory.Limits.Cones.equivalenceOfReindexing_unitIso, commBialgCatEquivComonCommAlgCat_inverse_obj, CategoryTheory.WithInitial.liftFromUnder_map_app, CategoryTheory.Iso.inverseCompIso_inv_app, CategoryTheory.Comma.equivProd_inverse_obj_left, CategoryTheory.eq_inverse_map, CategoryTheory.Limits.coconeEquivalenceOpConeOp_inverse_obj, TopCat.Presheaf.presheafEquivOfIso_counitIso_hom_app_app, sheafCongr_inverse, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_X_X, CategoryTheory.StructuredArrow.prodEquivalence_inverse, CategoryTheory.Iso.isoFunctorOfIsoInverse_hom_app, Action.resEquiv_inverse, CategoryTheory.Discrete.opposite_inverse_obj, CategoryTheory.ShiftedHom.opEquiv_symm_apply, HomologicalComplex.opEquivalence_inverse, CategoryTheory.effectiveEpiFamilyStructOfEquivalence_aux, CategoryTheory.Limits.Cocones.precomposeEquivalence_inverse, CategoryTheory.Limits.cospanOp_inv_app, AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso_hom_app, unit_app_comp_inverse_map_η_functor_assoc, Rep.ihom_coev_app_hom, CategoryTheory.simplicialCosimplicialAugmentedEquiv_inverse, BddLat.dualEquiv_inverse, leftOp_counitIso_hom_app, CategoryTheory.Comma.toPUnitIdEquiv_counitIso_inv_app, CategoryTheory.toOverIteratedSliceForwardIsoPullback_inv_app_left, functor_map_μ_inverse_comp_counit_app_tensor, CategoryTheory.Mon.limit_mon_one, CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ_inv_app, mapCommGrp_counitIso, CategoryTheory.MonoidalOpposite.mopEquiv_inverse, CategoryTheory.MorphismProperty.inverseImage_equivalence_functor_eq_map_inverse, CategoryTheory.Under.opEquivOpOver_inverse_obj, Action.rightUnitor_hom_hom, MonObj.mopEquiv_inverse_obj_mon_one, core_counitIso_inv_app_iso_hom, TopCat.Presheaf.presheafEquivOfIso_inverse_obj_obj, partialFunEquivPointed_inverse_map_Dom, CategoryTheory.Iso.inverseCompIso_hom_app, congrLeft_counitIso_hom_app, CategoryTheory.Over.iteratedSliceEquiv_inverse, CategoryTheory.StructuredArrow.mapIso_inverse_obj_left, AlgebraicTopology.DoldKan.Compatibility.τ₀_hom_app, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_inverse_map_hom, CategoryTheory.Discrete.equivOfEquivalence_symm_apply, unop_inverse, commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom, CategoryTheory.Under.equivalenceOfIsInitial_inverse_map, CategoryTheory.StructuredArrow.ofCommaSndEquivalence_inverse, CategoryTheory.Limits.Cocones.functorialityEquivalence_inverse, CategoryTheory.WithTerminal.equivComma_inverse_map_app, CategoryTheory.ShrinkHoms.equivalence_inverse, CategoryTheory.Sum.functorEquiv_unit_app_app_inl, CategoryTheory.MonoidalOpposite.unmopEquiv_counitIso_inv_app, CategoryTheory.Abelian.DoldKan.comparisonN_hom_app_f, CategoryTheory.Pi.equivalenceOfEquiv_inverse, preregular_isSheaf_iff_of_essentiallySmall, CategoryTheory.WithTerminal.equivComma_inverse_obj_map, CategoryTheory.Comon.monoidal_associator_inv_hom, CategoryTheory.Comma.toIdPUnitEquiv_counitIso_inv_app, Action.associator_inv_hom, CategoryTheory.Comon.Comon_EquivMon_OpOp_inverse, CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_inv_app_unop, CategoryTheory.regularTopology.equalizerCondition_iff_of_equivalence, partialFunEquivPointed_inverse_map_get_coe, CategoryTheory.ShortComplex.functorEquivalence_inverse, CategoryTheory.WithTerminal.liftFromOver_map_app, HomologicalComplex.dgoEquivHomologicalComplex_inverse, CategoryTheory.WithTerminal.coneEquiv_inverse_map_hom_left, CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_inv_app_unop_assoc, unop_unitIso, CategoryTheory.cosimplicialSimplicialEquiv_inverse_map, inverseFunctorObjIso_hom, toOrderIso_symm_apply, HomologicalComplex.unopEquivalence_inverse, SimplexCategory.revEquivalence_inverse, congrLeft_inverse, CategoryTheory.Preadditive.commGrpEquivalence_inverse_map, TopCat.Presheaf.presheafEquivOfIso_functor_map_app, inverseFunctorObj'_inv_app, CategoryTheory.Under.equivalenceOfIsInitial_inverse_obj, CategoryTheory.MonoidalOpposite.mopMopEquivalence_inverse_obj_unmop_unmop, symmEquivInverse_obj_unitIso_inv, TopologicalSpace.Opens.overEquivalence_inverse_obj_right_as, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₁, CategoryTheory.MonoOver.mapIso_inverse, CategoryTheory.Monoidal.comonFunctorCategoryEquivalence_inverse, counitIso_inv_app_tensor_comp_functor_map_δ_inverse, CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_obj_obj_snd, congrRight_inverse, CategoryTheory.Sum.functorEquiv_inverse_obj, CategoryTheory.Comma.mapLeftIso_inverse_map_left, CategoryTheory.MonoOver.congr_counitIso, AddCommMonCat.equivalence_inverse_map, CategoryTheory.Functor.flipping_inverse_obj_obj_obj, op_unitIso, CategoryTheory.Limits.coconeEquivalenceOpConeOp_inverse_map_hom, CategoryTheory.Discrete.equivalence_inverse, CategoryTheory.CatCommSq.hInv_iso_hom_app, op_inverse, CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_left_inv_assoc, CategoryTheory.Subobject.lowerEquivalence_inverse, isRightAdjoint_inverse, CategoryTheory.orderDualEquivalence_inverse_obj, leftOp_inverse_obj, CategoryTheory.MonoidalClosed.ofEquiv_curry_def, changeInverse_unitIso_hom_app, Action.rightUnitor_inv_hom, CategoryTheory.StructuredArrow.mapIso_inverse_map_left, CategoryTheory.CostructuredArrow.overEquivPresheafCostructuredArrow_inverse_map_toOverCompYoneda, congrRight_unitIso_hom_app, CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_hom_app_one, sheafCongrPrecoherent_functor_map_val_app, CategoryTheory.Monoidal.transportStruct_whiskerLeft, CategoryTheory.Functor.equiv_inverse, ε_comp_map_ε_assoc, core_unitIso_inv_app_iso_hom, FundamentalGroupoid.punitEquivDiscretePUnit_inverse, CategoryTheory.WithInitial.opEquiv_inverse_map, sheafCongr.functor_obj_val_obj, FinBddDistLat.dualEquiv_inverse, sheafCongrPreregular_unitIso_inv_app_val_app, CategoryTheory.Over.ConstructProducts.conesEquiv_inverse, CategoryTheory.Pretriangulated.triangleRotation_inverse, CategoryTheory.HasExactLimitsOfShape.of_codomain_equivalence, CategoryTheory.CostructuredArrow.mapIso_inverse_obj_hom, CategoryTheory.Limits.opParallelPairIso_inv_app_zero, trans_unitIso, CategoryTheory.Under.postEquiv_unitIso, sheafCongr.unitIso_inv_app_val_app, CategoryTheory.ObjectProperty.topEquivalence_inverse, CategoryTheory.ComposableArrows.opEquivalence_counitIso_hom_app_app, CategoryTheory.Limits.opParallelPairIso_inv_app_one, CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_one, full_inverse, CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_hom_app_unop_assoc, CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_obj_val, AlgebraicTopology.DoldKan.Compatibility.equivalence₂_functor, funInvIdAssoc_inv_app, CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_obj_obj_fst, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_X_d, symmEquivInverse_obj_inverse, CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_map_f, CategoryTheory.CostructuredArrow.mapIso_inverse_map_right, trans_inverse, CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence_inverse_obj, AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso_inv_app, AlgebraicTopology.DoldKan.Compatibility.equivalence₂_inverse, CategoryTheory.Functor.leftOpRightOpEquiv_inverse_obj, op_counitIso, CategoryTheory.Comon.monoidal_tensorHom_hom, mapHomologicalComplex_inverse, CategoryTheory.instIsDenseSubsiteOverLeftDiscretePUnitOverInverseIteratedSliceEquiv, CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_map, CategoryTheory.CostructuredArrow.mapIso_inverse_map_left, CategoryTheory.StructuredArrow.mapNatIso_inverse_map_left, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_app_eq, toAdjunction_unit, CategoryTheory.MonoidalOpposite.mopMopEquivalence_counitIso_hom_app, core_unitIso_inv_app_iso_inv, LinOrd.dualEquiv_inverse, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_inverse_map, counitInv_app_tensor_comp_functor_map_δ_inverse_assoc, counitInv_naturality_assoc, CategoryTheory.Comma.toIdPUnitEquiv_inverse_obj_right, CategoryTheory.Idempotents.DoldKan.N_map, CategoryTheory.Comma.mapRightIso_inverse_obj_left, CategoryTheory.Pretriangulated.shift_unop_opShiftFunctorEquivalence_counitIso_inv_app, CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalenceSymmHomEquiv_unop, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_map, CategoryTheory.comonEquiv_inverse, instIsDenseSubsiteCoherentTopologyInverse, CategoryTheory.Comma.mapRightIso_inverse_map_left, counit_app_functor, CommShift.instCommShiftHomFunctorUnitIso, CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_inv_app_op_one, sheafCongr.counitIso_inv_app_val_app, CategoryTheory.Sieve.functorPushforward_equivalence_eq_pullback, CategoryTheory.MonoidalOpposite.mopMopEquivalenceInverseMonoidal_μ_unmop_unmop, CategoryTheory.MonoidalOpposite.mopMopEquivalenceInverseMonoidal_η_unmop_unmop, CategoryTheory.Discrete.productEquiv_inverse_map, CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_hom_app_unop, mapAction_inverse, CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_hom_app_op_zero, pi_counitIso, CategoryTheory.Preadditive.commGrpEquivalence_inverse_obj, symmEquivInverse_obj_unitIso_hom, CategoryTheory.Under.opEquivOpOver_inverse_map, CategoryTheory.Abelian.DoldKan.comparisonN_inv_app_f, TopCat.Presheaf.presheafEquivOfIso_inverse_map_app, CategoryTheory.ULift.equivalence_inverse, CategoryTheory.Comon.monoidal_tensorObj_comon_counit, inverse_counitInv_comp, CategoryTheory.orderDualEquivalence_inverse_map, IsTriangulated.instIsTriangulatedInverse, core_counitIso_inv_app_iso_inv, unit_app_tensor_comp_inverse_map_δ_functor, CategoryTheory.Limits.Cocones.whiskeringEquivalence_counitIso, AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso_hom_app, CategoryTheory.Limits.Cones.postcomposeEquivalence_inverse, CategoryTheory.Limits.Cocones.functorialityEquivalence_unitIso, CategoryTheory.Functor.Final.coconesEquiv_inverse, AlgebraicTopology.DoldKan.Compatibility.υ_inv_app, unit_inverse_comp_assoc, symm_inverse, congrRight_counitIso_inv_app, counit_naturality, CategoryTheory.Monoidal.monFunctorCategoryEquivalence_inverse, CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_inverse, Action.leftUnitor_hom_hom, commGroupAddCommGroupEquivalence_inverse, DistLat.dualEquiv_inverse, congrRight_counitIso_hom_app, CategoryTheory.Pretriangulated.triangleOpEquivalence_inverse, CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalenceSymmHomEquiv_unop_assoc, CategoryTheory.WithTerminal.coneEquiv_inverse_obj_pt_right_as, CategoryTheory.Limits.walkingParallelPairOpEquiv_inverse, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality, CategoryTheory.Idempotents.DoldKan.η_hom_app_f, CategoryTheory.Limits.walkingCospanOpEquiv_inverse_map, trans_toAdjunction, CategoryTheory.Limits.pullbackConeEquivBinaryFan_inverse_map_hom, CategoryTheory.StructuredArrow.mapNatIso_inverse_obj_right, TopCat.Presheaf.generateEquivalenceOpensLe_inverse, changeFunctor_counitIso_inv_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_apply_assoc, congrRight_unitIso_inv_app, BddOrd.dualEquiv_inverse, functor_unit_comp_assoc, additive_inverse_of_FullyFaithful, CategoryTheory.Functor.currying_inverse_map_app_app, CategoryTheory.WithTerminal.opEquiv_inverse_map, symmEquivInverse_map_app, AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso_hom_app, essSurj_inverse, prod_inverse, CategoryTheory.Comon.monoidal_tensorObj_comon_comul, MonObj.mopEquiv_inverse_obj_mon_mul, CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInlIso_inv_app_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app_shift, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_app_assoc, CategoryTheory.CostructuredArrow.mapIso_inverse_obj_left, CategoryTheory.Functor.currying_inverse_obj_map_app
mk 📖	CompOp	—
mkHom 📖	CompOp	12 math math: mkHom_id_inverse, symmEquivFunctor_map, mkIso_hom, congrLeftFunctor_map, mkHom_asNatTrans, mkHom_id_functor, mkHom_comp, mkIso_inv, asNatTrans_mkHom, mkHom_comp_assoc, congrRightFunctor_map, symmEquivInverse_map_app
mkIso 📖	CompOp	2 math math: mkIso_hom, mkIso_inv
pow 📖	CompOp	—
powNat 📖	CompOp	—
refl 📖	CompOp	15 math math: CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_snd_fst, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_snd_snd, CommShift.instRefl, refl_inverse, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_snd_snd, refl_functor, refl_counitIso, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_fst, refl_toAdjunction, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_snd_fst, pow_zero, isMonoidal_refl, refl_unitIso, IsTriangulated.refl, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_fst
trans 📖	CompOp	23 math math: CategoryTheory.ComposableArrows.opEquivalence_counitIso_inv_app_app, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_snd_fst, CommShift.instTrans, CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_inv_app_fst, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_snd_snd, CategoryTheory.ComposableArrows.opEquivalence_unitIso_inv_app, CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_hom_app_snd, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_snd_snd, isMonoidal_trans, CategoryTheory.ComposableArrows.opEquivalence_functor_map_app, IsTriangulated.trans, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_fst, CategoryTheory.ComposableArrows.opEquivalence_unitIso_hom_app, trans_counitIso, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_snd_fst, CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_hom_app_fst, CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_inv_app_snd, trans_functor, CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_fst, trans_unitIso, CategoryTheory.ComposableArrows.opEquivalence_counitIso_hom_app_app, trans_inverse, trans_toAdjunction
unit 📖	CompOp	38 math math: CategoryTheory.Sum.natTransOfWhiskerLeftInlInr_app, symm_unit, CategoryTheory.Monoidal.instIsMonoidalUnitTransportedEquivalenceTransported, cancel_unit_right, functor_unit_comp, inv_fun_map, CategoryTheory.Sieve.pullback_functorPushforward_equivalence_eq, CategoryTheory.CostructuredArrow.overEquivPresheafCostructuredArrow_inverse_map_toOverCompCoyoneda, CategoryTheory.Sum.functorEquiv_unit_app_app_inr, CategoryTheory.Limits.HasColimit.isoOfEquivalence_hom_π, CategoryTheory.Adjunction.Equivalence.instIsMonoidalUnit, cancel_unit_right_assoc, CategoryTheory.toOverIsoToOverUnit_hom_app_left, Equivalence_mk'_unit, cancel_unit_right_assoc', inv_fun_map_assoc, CategoryTheory.Limits.IsColimit.ofCoconeEquiv_apply_desc, counitInv_app_functor, CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitorCorepresentingIso_inv_app_app, ε_comp_map_ε, unit_naturality_assoc, unit_app_tensor_comp_inverse_map_δ_functor_assoc, unit_naturality, CategoryTheory.MonoidalCategory.DayConvolution.associatorCorepresentingIso_inv_app_app, unit_app_comp_inverse_map_η_functor, unit_app_inverse, CategoryTheory.Functor.inv_fun_map, unit_inverse_comp, unit_app_comp_inverse_map_η_functor_assoc, CategoryTheory.Sum.functorEquiv_unit_app_app_inl, CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitorCorepresentingIso_inv_app_app, CategoryTheory.CostructuredArrow.overEquivPresheafCostructuredArrow_inverse_map_toOverCompYoneda, ε_comp_map_ε_assoc, funInvIdAssoc_inv_app, toAdjunction_unit, unit_app_tensor_comp_inverse_map_δ_functor, unit_inverse_comp_assoc, functor_unit_comp_assoc
unitInv 📖	CompOp	26 math math: CategoryTheory.Sum.natTransOfWhiskerLeftInlInr_app, CategoryTheory.ComposableArrows.opEquivalence_counitIso_inv_app_app, unitInv_naturality, inv_fun_map, funInvIdAssoc_hom_app, counitInv_functor_comp, unitInv_naturality_assoc, cancel_unitInv_right, CategoryTheory.toOverIteratedSliceForwardIsoPullback_hom_app_left, unitInv_app_inverse, symm_counit, inv_fun_map_assoc, inverse_counitInv_comp_assoc, CategoryTheory.Limits.IsColimit.ofCoconeEquiv_apply_desc, counitInv_functor_comp_assoc, CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitorCorepresentingIso_inv_app_app, CategoryTheory.Sieve.mem_functorPushforward_functor, CategoryTheory.Sieve.functorPushforward_functor, CategoryTheory.MonoidalCategory.DayConvolution.associatorCorepresentingIso_inv_app_app, CategoryTheory.Functor.inv_fun_map, CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitorCorepresentingIso_inv_app_app, Equivalence_mk'_unitInv, counit_app_functor, CategoryTheory.Sieve.functorPushforward_equivalence_eq_pullback, inverse_counitInv_comp, symmEquivInverse_map_app
unitIso 📖	CompOp	390 math math: CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_app_eq, prod_unitIso, CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_hom_app_zero, leftOp_unitIso_hom_app, CategoryTheory.WithTerminal.coneEquiv_unitIso_hom_app_hom_left, CategoryTheory.Monad.monadMonEquiv_unitIso_inv_app_toNatTrans_app, AlgebraicTopology.DoldKan.Compatibility.equivalence₀_unitIso_hom_app, CategoryTheory.comonEquiv_unitIso, CategoryTheory.equivOfTensorIsoUnit_unitIso, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_add_unitIso_hom_app_eq, CategoryTheory.Limits.coconeEquivalenceOpConeOp_unitIso, CategoryTheory.equivEssImageOfReflective_unitIso, AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso_inv_app, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_unitIso_inv_app_hom, unitIso_hom_app_comp_inverse_map_η_functor_assoc, CategoryTheory.MonoOver.congr_unitIso, counitInv_app_tensor_comp_functor_map_δ_inverse, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_unitIso, CategoryTheory.Discrete.sumEquiv_unitIso_inv_app, CategoryTheory.WithInitial.opEquiv_unitIso_inv_app, CategoryTheory.orderDualEquivalence_unitIso, AddCommMonCat.equivalence_unitIso, commBialgCatEquivComonCommAlgCat_unitIso_inv_app, TopCat.Presheaf.generateEquivalenceOpensLe_unitIso, partialFunEquivPointed_unitIso_hom_app, CategoryTheory.Monoidal.transportStruct_associator, CategoryTheory.Join.mapPairEquiv_unitIso, CategoryTheory.CatCommSq.hInv_iso_inv_app, leftOp_unitIso_inv_app, AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso_eq, CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_unitIso_hom_app_f, CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_unitIso_hom_app, AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso_hom_app, AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso_inv_app, CategoryTheory.MonoidalCategory.DayFunctor.equiv_unitIso_hom_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_left_inv, CategoryTheory.Preadditive.DoldKan.equivalence_unitIso, Action.functorCategoryEquivalence_unitIso, CategoryTheory.Comma.mapLeftIso_unitIso_inv_app_left, AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso_hom_app, CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_unitIso, HomologicalComplex₂.flipEquivalence_unitIso, CategoryTheory.MonoOver.mapIso_unitIso, CategoryTheory.Functor.currying₃_unitIso_hom_app_app_app_app, CategoryTheory.Pretriangulated.triangleOpEquivalence_unitIso, partialFunEquivPointed_unitIso_inv_app, CategoryTheory.Functor.Final.coconesEquiv_unitIso, CategoryTheory.Pi.equivalenceOfEquiv_unitIso, CategoryTheory.Monad.algebraEquivOfIsoMonads_unitIso, sheafCongrPreregular_unitIso_hom_app_val_app, CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_hom_app_fiber, CategoryTheory.Over.opEquivOpUnder_unitIso, core_unitIso_hom_app_iso_inv, CategoryTheory.Limits.Cocones.whiskeringEquivalence_unitIso, SimplexCategory.revEquivalence_unitIso, CategoryTheory.CostructuredArrow.mapNatIso_unitIso_inv_app_left, AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso_inv_app, CategoryTheory.Sum.functorEquiv_unitIso_inv_app_app_inl, CategoryTheory.TwoSquare.equivalenceJ_unitIso, CategoryTheory.Square.flipEquivalence_unitIso, CategoryTheory.CostructuredArrow.mapIso_unitIso_hom_app_left, CategoryTheory.Comma.mapRightIso_unitIso_inv_app_right, CategoryTheory.Limits.CategoricalPullback.functorEquiv_unitIso_inv_app_app_fst, HomologicalComplex.opEquivalence_unitIso, CategoryTheory.Preadditive.commGrpEquivalence_unitIso_inv_app, FinPartOrd.dualEquiv_unitIso, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, CategoryTheory.Preadditive.commGrpEquivalence_unitIso_hom_app, AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso_eq, CategoryTheory.Over.ConstructProducts.conesEquiv_unitIso, CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_inv_app_fiber, symm_unitIso, HomologicalComplex.dgoEquivHomologicalComplex_unitIso, mapHomologicalComplex_unitIso, CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_unitIso, CategoryTheory.Discrete.equivalence_unitIso, CategoryTheory.equivToOverUnit_unitIso, CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence_unitIso, CategoryTheory.StructuredArrow.preEquivalence_unitIso, CategoryTheory.MonoidalOpposite.mopMopEquivalence_unitIso_hom_app_unmop_unmop, CategoryTheory.Limits.Cocones.precomposeEquivalence_unitIso, CategoryTheory.Comma.equivProd_unitIso_hom_app_left, CategoryTheory.StructuredArrow.ofCommaSndEquivalence_unitIso, AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso_inv_app, CategoryTheory.Prod.braiding_unitIso, CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_unitIso, CategoryTheory.skeletonEquivalence_unitIso, CategoryTheory.prodOpEquiv_unitIso_hom_app, CategoryTheory.WithTerminal.opEquiv_unitIso_hom_app, CategoryTheory.Functor.leftOpRightOpEquiv_unitIso_inv_app, CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_inv_app_unop, CategoryTheory.ObjectProperty.fullSubcategoryCongr_unitIso, changeFunctor_unitIso_hom_app, CategoryTheory.ComposableArrows.opEquivalence_unitIso_inv_app, CategoryTheory.CostructuredArrow.mapIso_unitIso_inv_app_left, CategoryTheory.Monoidal.monFunctorCategoryEquivalence_unitIso, CategoryTheory.prod.associativity_unitIso, CategoryTheory.StructuredArrow.prodEquivalence_unitIso, CategoryTheory.ObjectProperty.topEquivalence_unitIso, CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_hom_app, Bipointed.swapEquiv_unitIso_inv_app_toFun, symmEquivInverse_obj_counitIso_hom, CategoryTheory.AsSmall.equiv_unitIso, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_hom_app_f_f, CategoryTheory.ForgetEnrichment.equiv_unitIso, CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_inv_app_base, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app_shift, MulEquiv.toSingleObjEquiv_unitIso_hom, mapMon_unitIso, pi_unitIso, CategoryTheory.simplicialCosimplicialEquiv_unitIso_hom_app, CategoryTheory.Limits.walkingCospanOpEquiv_unitIso_inv_app, CategoryTheory.MonoidalOpposite.mopEquiv_unitIso, CategoryTheory.typeEquiv_unitIso_hom_app, CategoryTheory.Over.postEquiv_inverse, CategoryTheory.StructuredArrow.mapNatIso_unitIso_hom_app_right, CategoryTheory.WithInitial.coconeEquiv_unitIso_hom_app_hom_right, CategoryTheory.Pi.optionEquivalence_unitIso, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_app, CategoryTheory.ULift.equivalence_unitIso_inv, unitIso_hom_app_tensor_comp_inverse_map_δ_functor, rightOp_unitIso_hom_app, CategoryTheory.Limits.colimitLimitToLimitColimitCone_hom, unitIso_hom_app_tensor_comp_inverse_map_δ_functor_assoc, CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_hom_app_base, CategoryTheory.GradedObject.comapEquiv_unitIso, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_zero_unitIso_inv_app, CategoryTheory.Pretriangulated.triangleRotation_unitIso, CategoryTheory.Iso.compInverseIso_inv_app, CategoryTheory.Cat.opEquivalence_unitIso, CategoryTheory.Comma.equivProd_unitIso_hom_app_right, TopCat.Presheaf.presheafEquivOfIso_unitIso_hom_app_app, CategoryTheory.Discrete.sumEquiv_unitIso_hom_app, CategoryTheory.CatCommSq.vInv_iso_hom_app, CategoryTheory.Sum.natIsoOfWhiskerLeftInlInr_eq, CategoryTheory.typeEquiv_unitIso_inv_app, TwoP.swapEquiv_unitIso_hom_app_hom_toFun, CategoryTheory.Comma.toIdPUnitEquiv_unitIso_inv_app_right, CategoryTheory.Limits.Cones.whiskeringEquivalence_unitIso, CategoryTheory.Comma.toPUnitIdEquiv_unitIso_inv_app_left, CategoryTheory.MonoidalOpposite.unmopEquiv_unitIso_inv_app_unmop, CategoryTheory.Limits.IsLimit.ofConeEquiv_apply_desc, CategoryTheory.forgetEnrichmentOppositeEquivalence_unitIso, CategoryTheory.Under.postEquiv_counitIso, CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence_unitIso, CategoryTheory.Adjunction.toEquivalence_unitIso_hom_app, CategoryTheory.piEquivalenceFunctorDiscrete_unitIso, CategoryTheory.sheafBotEquivalence_unitIso, TopologicalSpace.Opens.mapMapIso_unitIso, CategoryTheory.Comma.mapLeftIso_unitIso_inv_app_right, TopologicalSpace.Opens.overEquivalence_unitIso_hom_app_left, CategoryTheory.Comma.mapLeftIso_unitIso_hom_app_left, mapCommGrp_unitIso, CategoryTheory.Limits.Cones.postcomposeEquivalence_unitIso, unitIso_hom_app_comp_inverse_map_η_functor, CategoryTheory.Iso.compInverseIso_hom_app, CategoryTheory.Adjunction.toEquivalence_unitIso_inv_app, HomologicalComplex.unopEquivalence_unitIso, CategoryTheory.Limits.Cones.functorialityEquivalence_unitIso, CategoryTheory.Limits.Cocone.equivStructuredArrow_unitIso, CategoryTheory.Functor.Initial.conesEquiv_unitIso, congrFullSubcategory_unitIso, mapCommMon_unitIso, changeInverse_unitIso_inv_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_zero_unitIso_hom_app, CategoryTheory.Comma.toIdPUnitEquiv_unitIso_hom_app_right, MulEquiv.toSingleObjEquiv_unitIso_inv, CategoryTheory.ComposableArrows.opEquivalence_unitIso_hom_app, CategoryTheory.functorProdFunctorEquiv_unitIso, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_unitIso, CategoryTheory.ULift.equivalence_unitIso_hom, CategoryTheory.Idempotents.KaroubiKaroubi.equivalence_unitIso, CategoryTheory.prodOpEquiv_unitIso_inv_app, CategoryTheory.Over.postEquiv_counitIso, CategoryTheory.Monoidal.comonFunctorCategoryEquivalence_unitIso, sheafCongr.unitIso_hom_app_val_app, ModuleCat.matrixEquivalence_unitIso, CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_unitIso, CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_inv_app_zero, CategoryTheory.CostructuredArrow.prodEquivalence_unitIso, congrLeft_unitIso_inv_app, CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_unitIso, mapGrp_unitIso, CategoryTheory.Limits.CategoricalPullback.functorEquiv_unitIso_hom_app_app_snd, CategoryTheory.Iso.isoFunctorOfIsoInverse_inv_app, CategoryTheory.Functor.leftOpRightOpEquiv_unitIso_hom_app, CategoryTheory.Limits.walkingSpanOpEquiv_unitIso_inv_app, congrLeft_unitIso_hom_app, ext_iff, CategoryTheory.Under.equivalenceOfIsInitial_unitIso, symmEquivInverse_obj_counitIso_inv, CoalgCat.comonEquivalence_unitIso, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality_assoc, CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_unitIso_inv_app, CategoryTheory.cosimplicialSimplicialEquiv_unitIso_hom_app, changeFunctor_unitIso_inv_app, TopologicalSpace.Opens.overEquivalence_unitIso_inv_app_left, CategoryTheory.Monoidal.transportStruct_leftUnitor, CategoryTheory.Functor.flipping_unitIso_hom_app_app_app, CategoryTheory.Monoidal.transportStruct_rightUnitor, CategoryTheory.Idempotents.DoldKan.η_inv_app_f, CategoryTheory.CostructuredArrow.mapNatIso_unitIso_hom_app_left, CategoryTheory.Functor.equiv_unitIso, CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_inv_app, CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_unitIso_inv_app_f, CategoryTheory.Comon.Comon_EquivMon_OpOp_unitIso, CategoryTheory.StructuredArrow.mapIso_unitIso_inv_app_right, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_naturality_assoc, CategoryTheory.opOpEquivalence_unitIso, CategoryTheory.Limits.Cones.functorialityEquivalence_inverse, CategoryTheory.Functor.flipping_unitIso_inv_app_app_app, CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_inv_app_one, FundamentalGroupoid.punitEquivDiscretePUnit_unitIso, CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence_unitIso, TopCat.Presheaf.presheafEquivOfIso_unitIso_inv_app_app, CategoryTheory.MonoOver.congr_inverse, CategoryTheory.Iso.isoCompInverse_inv_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_naturality, CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso_unitIso, CategoryTheory.cosimplicialSimplicialEquiv_unitIso_inv_app, CategoryTheory.Limits.Cocones.functorialityEquivalence_counitIso, commAlgCatEquivUnder_unitIso, induced_unitIso, MonObj.mopEquiv_unitIso_hom_app_hom, CategoryTheory.Iso.isoInverseOfIsoFunctor_inv_app, CategoryTheory.algebraEquivUnder_unitIso, sheafCongrPrecoherent_unitIso_inv_app_val_app, SimplicialObject.opEquivalence_unitIso, CategoryTheory.Over.iteratedSliceEquiv_unitIso, CategoryTheory.Comma.toPUnitIdEquiv_unitIso_hom_app_left, CategoryTheory.CatCommSq.vInv_iso_inv_app, counitIso_inv_app_tensor_comp_functor_map_δ_inverse_assoc, CategoryTheory.Comma.mapRightIso_unitIso_hom_app_left, CategoryTheory.WithInitial.equivComma_unitIso_inv_app_app, CategoryTheory.prod.rightUnitorEquivalence_unitIso, symmEquiv_unitIso, CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_unitIso, CategoryTheory.Functor.currying_unitIso_inv_app_app_app, CategoryTheory.Functor.currying_unitIso_hom_app_app_app, SSet.opEquivalence_unitIso, alexDiscEquivPreord_unitIso, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_inv_app_app, CategoryTheory.Comma.mapLeftIso_unitIso_hom_app_right, CategoryTheory.Limits.CategoricalPullback.functorEquiv_unitIso_inv_app_app_snd, CategoryTheory.Limits.Cones.functorialityEquivalence_counitIso, CategoryTheory.Comma.opEquiv_unitIso, CategoryTheory.MonoidalOpposite.unmopEquiv_unitIso_hom_app_unmop, CategoryTheory.Under.postEquiv_inverse, CategoryTheory.Functor.opUnopEquiv_unitIso, CategoryTheory.Presheaf.coherentExtensiveEquivalence_unitIso, CategoryTheory.Sum.functorEquiv_unitIso_inv_app_app_inr, CategoryTheory.Functor.currying₃_unitIso_inv_app_app_app_app, OrderHom.equivalenceFunctor_unitIso_hom_app, CategoryTheory.WithInitial.equivComma_unitIso_hom_app_app, CategoryTheory.prod.leftUnitorEquivalence_unitIso, CategoryTheory.shiftEquiv'_unitIso, CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_hom_app_unop_assoc, groupAddGroupEquivalence_unitIso, CategoryTheory.Endofunctor.Algebra.equivOfNatIso_unitIso, unit_app_tensor_comp_inverse_map_δ_functor_assoc, AlgebraicTopology.DoldKan.Compatibility.υ_hom_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_add_unitIso_inv_app_eq, CategoryTheory.MonoidalOpposite.mopMopEquivalence_unitIso_inv_app_unmop_unmop, CategoryTheory.simplicialCosimplicialEquiv_unitIso_inv_app, CategoryTheory.Subobject.lowerEquivalence_unitIso, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_hom_app_app, functor_unitIso_comp, CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_obj, CategoryTheory.Subfunctor.equivalenceMonoOver_unitIso, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_inv_app_app, CategoryTheory.Comma.equivProd_unitIso_inv_app_right, CategoryTheory.Over.equivalenceOfIsTerminal_unitIso, sheafCongrPrecoherent_unitIso_hom_app_val_app, CategoryTheory.StructuredArrow.mapIso_unitIso_hom_app_right, symm_counitIso, CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_one, CategoryTheory.eq_unitIso, core_unitIso_hom_app_iso_hom, CategoryTheory.StructuredArrow.mapNatIso_unitIso_inv_app_right, CategoryTheory.subterminalsEquivMonoOverTerminal_unitIso, rightOp_unitIso_inv_app, commGroupAddCommGroupEquivalence_unitIso, CategoryTheory.Over.postEquiv_unitIso, CategoryTheory.Iso.isoCompInverse_hom_app, CategoryTheory.Iso.isoInverseOfIsoFunctor_hom_app, CategoryTheory.Idempotents.karoubiUniversal₁_unitIso, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence_unitIso, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_app_assoc, CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_zero, CategoryTheory.Pretriangulated.shift_unop_opShiftFunctorEquivalence_counitIso_hom_app, CategoryTheory.WithTerminal.coneEquiv_unitIso_inv_app_hom_left, CategoryTheory.Square.arrowArrowEquivalence'_unitIso, CategoryTheory.ShortComplex.functorEquivalence_unitIso, CategoryTheory.CategoryOfElements.structuredArrowEquivalence_unitIso, CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv_unitIso, CategoryTheory.Limits.Cones.equivalenceOfReindexing_unitIso, CategoryTheory.Comma.mapRightIso_unitIso_inv_app_left, CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_unitIso_hom_app_right_app, CategoryTheory.Iso.isoFunctorOfIsoInverse_hom_app, CategoryTheory.ShiftedHom.opEquiv_symm_apply, AddMonCat.equivalence_unitIso, AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso_hom_app, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_inv_app_f_f, Types.monoOverEquivalenceSet_unitIso, CategoryTheory.CostructuredArrow.ofCommaFstEquivalence_unitIso, CategoryTheory.coalgebraEquivOver_unitIso, CategoryTheory.Limits.Cone.equivCostructuredArrow_unitIso, CategoryTheory.Limits.Cocones.functorialityEquivalence_inverse, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_unitIso, CategoryTheory.Abelian.DoldKan.comparisonN_hom_app_f, CategoryTheory.MonoidalCategory.DayFunctor.equiv_unitIso_inv_app, CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_inv_app_unop_assoc, unop_unitIso, CategoryTheory.Limits.walkingSpanOpEquiv_unitIso_hom_app, refl_unitIso, symmEquivInverse_obj_unitIso_inv, counitIso_inv_app_tensor_comp_functor_map_δ_inverse, CategoryTheory.MonoOver.congr_counitIso, op_unitIso, CategoryTheory.Groupoid.invEquivalence_unitIso, CategoryTheory.CatCommSq.hInv_iso_hom_app, CategoryTheory.ShortComplex.opEquiv_unitIso, MonObj.mopEquiv_unitIso_inv_app_hom, CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_left_inv_assoc, changeInverse_unitIso_hom_app, Bipointed.swapEquiv_unitIso_hom_app_toFun, CategoryTheory.Monad.monadMonEquiv_unitIso_hom_app_toNatTrans_app, congrRight_unitIso_hom_app, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_unitIso_hom_app_hom, CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_hom_app_one, OrderHom.equivalenceFunctor_unitIso_inv_app, CategoryTheory.Under.opEquivOpOver_unitIso, core_unitIso_inv_app_iso_hom, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_unitIso, CategoryTheory.Limits.CategoricalPullback.functorEquiv_unitIso_hom_app_app_fst, sheafCongrPreregular_unitIso_inv_app_val_app, CategoryTheory.Square.arrowArrowEquivalence_unitIso, AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso_eq, trans_unitIso, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_inv_app_f_f, CategoryTheory.Under.postEquiv_unitIso, sheafCongr.unitIso_inv_app_val_app, CategoryTheory.Comma.equivProd_unitIso_inv_app_left, CategoryTheory.Limits.pullbackConeEquivBinaryFan_unitIso, CategoryTheory.ShrinkHoms.equivalence_unitIso, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_unitIso, CategoryTheory.Limits.walkingCospanOpEquiv_unitIso_hom_app, CategoryTheory.Pseudofunctor.DescentData.pullFunctorEquivalence_unitIso, AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso_inv_app, CategoryTheory.Sum.functorEquiv_unitIso, CategoryTheory.WithInitial.opEquiv_unitIso_hom_app, CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_map, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_hom_app_f_f, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_app_eq, core_unitIso_inv_app_iso_inv, sheafCongr_unitIso, CategoryTheory.WithTerminal.equivComma_unitIso_hom_app_app, counitInv_app_tensor_comp_functor_map_δ_inverse_assoc, CategoryTheory.Pretriangulated.shift_unop_opShiftFunctorEquivalence_counitIso_inv_app, CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalenceSymmHomEquiv_unop, CategoryTheory.WithTerminal.opEquiv_unitIso_inv_app, CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_unitIso_inv_app_hom, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_app, OrderIso.equivalence_unitIso, CommShift.instCommShiftHomFunctorUnitIso, CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_hom_app_unop, CategoryTheory.WithInitial.coconeEquiv_unitIso_inv_app_hom_right, symmEquivInverse_obj_unitIso_hom, CategoryTheory.Abelian.DoldKan.comparisonN_inv_app_f, unit_app_tensor_comp_inverse_map_δ_functor, CategoryTheory.WithTerminal.equivComma_unitIso_inv_app_app, AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso_hom_app, CategoryTheory.Limits.Cocones.functorialityEquivalence_unitIso, AlgebraicTopology.DoldKan.Compatibility.υ_inv_app, CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_unitIso_inv_app_right_app, CategoryTheory.RelCat.opEquivalence_unitIso, CategoryTheory.Limits.widePushoutShapeOpEquiv_unitIso, CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_unitIso_hom_app_hom, CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalenceSymmHomEquiv_unop_assoc, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality, CategoryTheory.Idempotents.DoldKan.η_hom_app_f, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_hom_app_app, CategoryTheory.Comma.mapRightIso_unitIso_hom_app_right, TwoP.swapEquiv_unitIso_inv_app_hom_toFun, congrRight_unitIso_inv_app, CategoryTheory.Idempotents.DoldKan.equivalence_unitIso, AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso_hom_app, CategoryTheory.Limits.widePullbackShapeOpEquiv_unitIso, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app_shift, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_app_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Equivalence_mk'_counit 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.CategoryStruct.id	counit mk'	—	—
Equivalence_mk'_counitInv 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.CategoryStruct.id	counitInv mk' CategoryTheory.Iso.inv	—	—
Equivalence_mk'_unit 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.CategoryStruct.id	unit mk'	—	—
Equivalence_mk'_unitInv 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.CategoryStruct.id	unitInv mk' CategoryTheory.Iso.inv	—	—
adjointify_η_ε 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category adjointifyη CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.comp_id CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp CategoryTheory.NatTrans.naturality CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.id_comp
adjointify_η_ε_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category adjointifyη	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' adjointify_η_ε
asNatTrans_mkHom 📖	mathematical	—	asNatTrans mkHom	—	—
cancel_counitInv_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.comp inverse functor CategoryTheory.NatTrans.app CategoryTheory.Functor.id counitInv	—	CategoryTheory.IsIso.mono_of_iso CategoryTheory.NatIso.inv_app_isIso
cancel_counitInv_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.comp inverse functor CategoryTheory.NatTrans.app CategoryTheory.Functor.id counitInv	—	CategoryTheory.IsIso.mono_of_iso CategoryTheory.NatIso.inv_app_isIso
cancel_counitInv_right_assoc' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.comp inverse functor CategoryTheory.NatTrans.app CategoryTheory.Functor.id counitInv	—	CategoryTheory.IsIso.mono_of_iso CategoryTheory.NatIso.inv_app_isIso
cancel_counit_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor inverse CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Functor.comp counit	—	CategoryTheory.IsIso.mono_of_iso CategoryTheory.NatIso.hom_app_isIso
cancel_unitInv_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj inverse functor CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Functor.comp unitInv	—	CategoryTheory.IsIso.mono_of_iso CategoryTheory.NatIso.inv_app_isIso
cancel_unit_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.comp functor inverse CategoryTheory.NatTrans.app CategoryTheory.Functor.id unit	—	CategoryTheory.IsIso.mono_of_iso CategoryTheory.NatIso.hom_app_isIso
cancel_unit_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.comp functor inverse CategoryTheory.NatTrans.app CategoryTheory.Functor.id unit	—	CategoryTheory.IsIso.mono_of_iso CategoryTheory.NatIso.hom_app_isIso
cancel_unit_right_assoc' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.comp functor inverse CategoryTheory.NatTrans.app CategoryTheory.Functor.id unit	—	CategoryTheory.IsIso.mono_of_iso CategoryTheory.NatIso.hom_app_isIso
changeFunctor_counitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp inverse CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category counitIso changeFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor CategoryTheory.Iso.inv	—	—
changeFunctor_counitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp inverse CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category counitIso changeFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor CategoryTheory.Iso.hom	—	—
changeFunctor_functor 📖	mathematical	—	functor changeFunctor	—	—
changeFunctor_inverse 📖	mathematical	—	inverse changeFunctor	—	—
changeFunctor_refl 📖	mathematical	—	changeFunctor functor CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category	—	ext CategoryTheory.Iso.ext CategoryTheory.NatTrans.ext' CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
changeFunctor_trans 📖	mathematical	—	changeFunctor CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category functor	—	ext CategoryTheory.Iso.ext CategoryTheory.NatTrans.ext' CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp
changeFunctor_unitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp inverse CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category unitIso changeFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor CategoryTheory.Functor.map	—	—
changeFunctor_unitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp inverse CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category unitIso changeFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor CategoryTheory.Functor.map	—	—
changeInverse_counitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp functor CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category counitIso changeInverse CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj inverse CategoryTheory.Functor.map CategoryTheory.Iso.inv	—	—
changeInverse_counitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp functor CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category counitIso changeInverse CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj inverse CategoryTheory.Functor.map CategoryTheory.Iso.hom	—	—
changeInverse_functor 📖	mathematical	—	functor changeInverse	—	—
changeInverse_inverse 📖	mathematical	—	inverse changeInverse	—	—
changeInverse_unitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp functor CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category unitIso changeInverse CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj inverse	—	—
changeInverse_unitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp functor CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category unitIso changeInverse CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj inverse	—	—
comp_asNatTrans 📖	mathematical	—	asNatTrans CategoryTheory.CategoryStruct.comp CategoryTheory.Equivalence CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor CategoryTheory.Functor.category functor	—	—
comp_asNatTrans_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category functor asNatTrans CategoryTheory.Equivalence instCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_asNatTrans
congrLeft_counitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft functor inverse CategoryTheory.Functor.id CategoryTheory.Iso.hom counitIso congrLeft invFunIdAssoc	—	—
congrLeft_counitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft functor inverse CategoryTheory.Iso.inv counitIso congrLeft invFunIdAssoc	—	—
congrLeft_functor 📖	mathematical	—	functor CategoryTheory.Functor CategoryTheory.Functor.category congrLeft CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft inverse	—	—
congrLeft_inverse 📖	mathematical	—	inverse CategoryTheory.Functor CategoryTheory.Functor.category congrLeft CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft functor	—	—
congrLeft_unitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft inverse functor CategoryTheory.Iso.hom unitIso congrLeft CategoryTheory.Iso.inv funInvIdAssoc	—	—
congrLeft_unitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft inverse functor CategoryTheory.Functor.id CategoryTheory.Iso.inv unitIso congrLeft CategoryTheory.Iso.hom funInvIdAssoc	—	—
congrRightFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Equivalence instCategory CategoryTheory.Functor CategoryTheory.Functor.category congrRightFunctor mkHom congrRight CategoryTheory.Functor.whiskeringRight functor asNatTrans	—	—
congrRightFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Equivalence instCategory CategoryTheory.Functor CategoryTheory.Functor.category congrRightFunctor congrRight	—	—
congrRight_counitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight inverse functor CategoryTheory.Functor.id CategoryTheory.Iso.hom counitIso congrRight CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.associator CategoryTheory.Functor.whiskerLeft CategoryTheory.Functor.rightUnitor	—	—
congrRight_counitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight inverse functor CategoryTheory.Iso.inv counitIso congrRight CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.rightUnitor CategoryTheory.Functor.whiskerLeft CategoryTheory.Functor.associator	—	CategoryTheory.Category.assoc
congrRight_functor 📖	mathematical	—	functor CategoryTheory.Functor CategoryTheory.Functor.category congrRight CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight	—	—
congrRight_inverse 📖	mathematical	—	inverse CategoryTheory.Functor CategoryTheory.Functor.category congrRight CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight	—	—
congrRight_unitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight functor inverse CategoryTheory.Iso.hom unitIso congrRight CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv CategoryTheory.Functor.rightUnitor CategoryTheory.Functor.whiskerLeft CategoryTheory.Functor.associator	—	—
congrRight_unitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight functor inverse CategoryTheory.Functor.id CategoryTheory.Iso.inv unitIso congrRight CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.associator CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.hom CategoryTheory.Functor.rightUnitor	—	CategoryTheory.Category.assoc
counitInv_app_functor 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp inverse functor counitInv CategoryTheory.Functor.obj CategoryTheory.Functor.map unit	—	CategoryTheory.Iso.app_inv CategoryTheory.Iso.comp_hom_eq_id CategoryTheory.Iso.app_hom functor_unit_comp
counitInv_functor_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id functor CategoryTheory.Functor.comp inverse CategoryTheory.NatTrans.app counitInv CategoryTheory.Functor.map unitInv CategoryTheory.CategoryStruct.id	—	functor_unit_comp CategoryTheory.Iso.inv_eq_inv
counitInv_functor_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor inverse CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp counitInv CategoryTheory.Functor.map unitInv	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' counitInv_functor_comp
counitInv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp inverse functor CategoryTheory.NatTrans.app counitInv CategoryTheory.Functor.map	—	CategoryTheory.NatTrans.naturality
counitInv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor inverse CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp counitInv CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' counitInv_naturality
counit_app_functor 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp inverse functor CategoryTheory.Functor.id counit CategoryTheory.Functor.obj CategoryTheory.Functor.map unitInv	—	functor_unit_comp CategoryTheory.Iso.hom_comp_eq_id
counit_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor inverse CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp counit	—	CategoryTheory.NatTrans.naturality
counit_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor inverse CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id counit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' counit_naturality
essSurjInducedFunctor 📖	mathematical	—	CategoryTheory.Functor.EssSurj CategoryTheory.InducedCategory DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.InducedCategory.instCategory CategoryTheory.inducedFunctor	—	Equiv.apply_symm_apply
essSurj_functor 📖	mathematical	—	CategoryTheory.Functor.EssSurj functor	—	—
essSurj_inverse 📖	mathematical	—	CategoryTheory.Functor.EssSurj inverse	—	essSurj_functor
ext 📖	—	functor inverse CategoryTheory.Iso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp unitIso counitIso	—	—	—
ext_iff 📖	mathematical	—	functor inverse CategoryTheory.Iso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp unitIso counitIso	—	ext
faithful_functor 📖	mathematical	—	CategoryTheory.Functor.Faithful functor	—	CategoryTheory.Functor.FullyFaithful.faithful
faithful_inverse 📖	mathematical	—	CategoryTheory.Functor.Faithful inverse	—	CategoryTheory.Functor.FullyFaithful.faithful
full_functor 📖	mathematical	—	CategoryTheory.Functor.Full functor	—	CategoryTheory.Functor.FullyFaithful.full
full_inverse 📖	mathematical	—	CategoryTheory.Functor.Full inverse	—	CategoryTheory.Functor.FullyFaithful.full
fullyFaithfulToEssImage 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence CategoryTheory.Functor.EssImageSubcategory CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.essImage CategoryTheory.Functor.toEssImage	—	CategoryTheory.Functor.Faithful.toEssImage CategoryTheory.Functor.Full.toEssImage CategoryTheory.Functor.EssSurj.toEssImage
funInvIdAssoc_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp functor inverse CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category funInvIdAssoc CategoryTheory.Functor.map CategoryTheory.Functor.obj CategoryTheory.Functor.id unitInv	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
funInvIdAssoc_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp functor inverse CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category funInvIdAssoc CategoryTheory.Functor.map CategoryTheory.Functor.obj CategoryTheory.Functor.id unit	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
fun_inv_map 📖	mathematical	—	CategoryTheory.Functor.map functor CategoryTheory.Functor.obj inverse CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.NatTrans.app counit counitInv	—	CategoryTheory.NatIso.naturality_2
fun_inv_map_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor inverse CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id counit counitInv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fun_inv_map
functorFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Equivalence instCategory CategoryTheory.Functor CategoryTheory.Functor.category functorFunctor asNatTrans	—	—
functorFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Equivalence instCategory CategoryTheory.Functor CategoryTheory.Functor.category functorFunctor functor	—	—
functor_unitIso_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor CategoryTheory.Functor.id CategoryTheory.Functor.comp inverse CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category unitIso counitIso CategoryTheory.CategoryStruct.id	—	—
functor_unit_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor CategoryTheory.Functor.id CategoryTheory.Functor.comp inverse CategoryTheory.Functor.map CategoryTheory.NatTrans.app unit counit CategoryTheory.CategoryStruct.id	—	functor_unitIso_comp
functor_unit_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor inverse CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp unit counit	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' functor_unit_comp
hom_ext 📖	—	asNatTrans	—	—	—
hom_ext_iff 📖	mathematical	—	asNatTrans	—	hom_ext
id_asNatTrans 📖	mathematical	—	asNatTrans CategoryTheory.CategoryStruct.id CategoryTheory.Equivalence CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor CategoryTheory.Functor.category functor	—	—
inducedFunctorOfEquiv 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence CategoryTheory.InducedCategory DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.InducedCategory.instCategory CategoryTheory.inducedFunctor	—	CategoryTheory.InducedCategory.faithful CategoryTheory.InducedCategory.full essSurjInducedFunctor
invFunIdAssoc_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp inverse functor CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category invFunIdAssoc CategoryTheory.Functor.map CategoryTheory.Functor.obj CategoryTheory.Functor.id counit	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
invFunIdAssoc_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp inverse functor CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category invFunIdAssoc CategoryTheory.Functor.map CategoryTheory.Functor.obj CategoryTheory.Functor.id counitInv	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
inv_fun_map 📖	mathematical	—	CategoryTheory.Functor.map inverse CategoryTheory.Functor.obj functor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.NatTrans.app unitInv unit	—	CategoryTheory.NatIso.naturality_1
inv_fun_map_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj inverse functor CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id unitInv unit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inv_fun_map
inverse_counitInv_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj inverse CategoryTheory.Functor.id CategoryTheory.Functor.comp functor CategoryTheory.Functor.map CategoryTheory.NatTrans.app counitInv unitInv CategoryTheory.CategoryStruct.id	—	unit_inverse_comp CategoryTheory.Iso.inv_eq_inv
inverse_counitInv_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj inverse functor CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp counitInv unitInv	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' inverse_counitInv_comp
isEquivalence_functor 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence functor	—	faithful_functor full_functor essSurj_functor
isEquivalence_inverse 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence inverse	—	isEquivalence_functor
mkHom_asNatTrans 📖	mathematical	—	mkHom asNatTrans	—	—
mkHom_comp 📖	mathematical	—	mkHom CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category functor CategoryTheory.Equivalence instCategory	—	—
mkHom_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Equivalence CategoryTheory.Category.toCategoryStruct instCategory mkHom CategoryTheory.Functor CategoryTheory.Functor.category functor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mkHom_comp
mkHom_id_functor 📖	mathematical	—	mkHom CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category functor CategoryTheory.Equivalence instCategory	—	—
mkHom_id_inverse 📖	mathematical	—	mkHom symm CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category inverse CategoryTheory.Equivalence instCategory	—	—
mkIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Equivalence instCategory mkIso mkHom CategoryTheory.Functor CategoryTheory.Functor.category functor	—	—
mkIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Equivalence instCategory mkIso mkHom CategoryTheory.Functor CategoryTheory.Functor.category functor	—	—
pow_neg_one 📖	mathematical	—	CategoryTheory.Equivalence instPowInt symm	—	—
pow_one 📖	mathematical	—	CategoryTheory.Equivalence instPowInt	—	—
pow_zero 📖	mathematical	—	CategoryTheory.Equivalence instPowInt refl	—	—
refl_counitIso 📖	mathematical	—	counitIso refl CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.id	—	—
refl_functor 📖	mathematical	—	functor refl CategoryTheory.Functor.id	—	—
refl_inverse 📖	mathematical	—	inverse refl CategoryTheory.Functor.id	—	—
refl_unitIso 📖	mathematical	—	unitIso refl CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id	—	—
symm_counit 📖	mathematical	—	counit symm unitInv	—	—
symm_counitIso 📖	mathematical	—	counitIso symm CategoryTheory.Iso.symm CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp functor inverse unitIso	—	—
symm_functor 📖	mathematical	—	functor symm inverse	—	—
symm_inverse 📖	mathematical	—	inverse symm functor	—	—
symm_unit 📖	mathematical	—	unit symm counitInv	—	—
symm_unitIso 📖	mathematical	—	unitIso symm CategoryTheory.Iso.symm CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp inverse functor CategoryTheory.Functor.id counitIso	—	—
trans_counitIso 📖	mathematical	—	counitIso trans CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp inverse functor CategoryTheory.Functor.id CategoryTheory.Iso.symm CategoryTheory.Functor.associator CategoryTheory.Functor.isoWhiskerRight CategoryTheory.Functor.isoWhiskerLeft CategoryTheory.Functor.rightUnitor	—	—
trans_functor 📖	mathematical	—	functor trans CategoryTheory.Functor.comp	—	—
trans_inverse 📖	mathematical	—	inverse trans CategoryTheory.Functor.comp	—	—
trans_unitIso 📖	mathematical	—	unitIso trans CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp functor inverse CategoryTheory.Functor.isoWhiskerRight CategoryTheory.Iso.symm CategoryTheory.Functor.rightUnitor CategoryTheory.Functor.isoWhiskerLeft CategoryTheory.Functor.associator	—	—
unitInv_app_inverse 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp functor inverse CategoryTheory.Functor.id unitInv CategoryTheory.Functor.obj CategoryTheory.Functor.map counit	—	CategoryTheory.Iso.app_inv CategoryTheory.Iso.app_hom CategoryTheory.Functor.mapIso_hom CategoryTheory.Iso.hom_eq_inv unit_app_inverse
unitInv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj inverse functor CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp unitInv	—	CategoryTheory.NatTrans.naturality
unitInv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj inverse functor CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id unitInv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unitInv_naturality
unit_app_inverse 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp functor inverse unit CategoryTheory.Functor.obj CategoryTheory.Functor.map counitInv	—	unit_inverse_comp CategoryTheory.Iso.comp_hom_eq_id
unit_inverse_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id inverse CategoryTheory.Functor.comp functor CategoryTheory.NatTrans.app unit CategoryTheory.Functor.map counit CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.id_comp CategoryTheory.Functor.map_id counitInv_functor_comp CategoryTheory.Functor.map_comp CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.Iso.app_hom CategoryTheory.Iso.app_inv CategoryTheory.Category.assoc unit_naturality counit_naturality CategoryTheory.Iso.hom_inv_id_app counitInv_naturality unitInv_naturality
unit_inverse_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj inverse functor CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp unit CategoryTheory.Functor.map counit	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' unit_inverse_comp
unit_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp functor inverse CategoryTheory.NatTrans.app unit CategoryTheory.Functor.map	—	CategoryTheory.NatTrans.naturality
unit_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj inverse functor CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp unit CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unit_naturality

CategoryTheory.Functor

Definitions

Name	Category	Theorems
IsEquivalence 📖	CompData	116 math math: CategoryTheory.Pseudofunctor.DescentData.isEquivalence_toDescentData_of_sieve_le, CategoryTheory.LocalizerMorphism.isEquivalence, CategoryTheory.instIsEquivalenceOppositeUnopUnop, Action.instIsEquivalenceFunctorSingleObjInverse, CategoryTheory.CoreSmallCategoryOfSet.instIsEquivalenceElemObjSmallCategoryOfSetFunctor, CategoryTheory.Equivalence.isEquivalence_inverse, IsDenseSubsite.instIsEquivalenceSheafSheafPushforwardContinuous, CategoryTheory.Pseudofunctor.isEquivalence_toDescentData, CategoryTheory.Idempotents.toKaroubi_isEquivalence, CategoryTheory.Prod.swapIsEquivalence, CategoryTheory.Idempotents.instIsEquivalenceFunctorKaroubiFunctorExtension₂, CategoryTheory.ComonadicLeftAdjoint.eqv, isEquivalence_of_comp_left, CategoryTheory.Localization.instIsEquivalenceLocalizationLift, CategoryTheory.CostructuredArrow.isEquivalence_pre, CategoryTheory.Idempotents.instIsEquivalenceFunctorKaroubiObjWhiskeringLeftToKaroubi, CategoryTheory.Over.instIsEquivalenceObjPost, CategoryTheory.ThinSkeleton.fromThinSkeleton_isEquivalence, CategoryTheory.Pseudofunctor.CoGrothendieck.instIsEquivalenceαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, CategoryTheory.CostructuredArrow.isEquivalenceMap₂, AlgebraicGeometry.AffineScheme.instIsEquivalenceOppositeCommRingCatOpRightOpΓ, isEquivalence_trans, CategoryTheory.Join.isEquivalenceMapPair, AlgebraicGeometry.AffineScheme.instIsEquivalenceOppositeCommRingCatRightOpΓ, CategoryTheory.prod.associatorIsEquivalence, instIsEquivalenceFGModuleCatUlift, ModuleCat.restrictScalars_isEquivalence_of_ringEquiv, CategoryTheory.fromSkeleton.isEquivalence, CategoryTheory.LocalizerMorphism.localizedFunctor_isEquivalence, CategoryTheory.prod.inverseAssociatorIsEquivalence, CategoryTheory.Idempotents.instIsEquivalenceFunctorKaroubiFunctorExtension, CategoryTheory.Pseudofunctor.isStackFor_ofArrows_iff, CategoryTheory.StructuredArrow.isEquivalence_pre, instIsEquivalenceUliftFunctorOfUnivLE, isEquivalence_of_isRightAdjoint, compactumToCompHaus.isEquivalence, CategoryTheory.RelCat.instIsEquivalenceOppositeUnopFunctor, FintypeCat.Skeleton.instIsEquivalenceIncl, isEquivalence_of_iso, CategoryTheory.Under.instIsEquivalenceMapOfIsIso, instIsEquivalenceRightExtensionPostcomp₁OfIsIso, CategoryTheory.sum.associatorIsEquivalence, CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor_isEquivalence, CategoryTheory.PreGaloisCategory.instIsEquivalenceContActionFintypeCatHomCarrierAutFunctorFunctorToContAction, CategoryTheory.LocalizerMorphism.isEquivalence_imp, CategoryTheory.sum.inverseAssociatorIsEquivalence, instIsEquivalenceLeftExtensionPostcomp₁OfIsIso, CategoryTheory.StructuredArrow.isEquivalence_toUnder, Action.instIsEquivalenceFunctorSingleObjFunctor, CategoryTheory.Comma.isEquivalence_post, CategoryTheory.instIsEquivalenceOppositeOpOp, CategoryTheory.Types.instIsEquivalenceForgetTypeHom, isEquivalence_refl, CategoryTheory.Comma.isEquivalenceMap, CategoryTheory.Comma.isEquivalence_preLeft, CategoryTheory.Localization.instIsEquivalenceFunctorFunctorsInvertingWhiskeringLeftFunctor, CategoryTheory.Pseudofunctor.isStackFor_iff, CategoryTheory.StructuredArrow.isEquivalenceMap₂, CategoryTheory.StructuredArrow.isEquivalence_post, SimplexCategory.SkeletalFunctor.isEquivalence, FGModuleRepr.instIsEquivalenceFGModuleCatEmbed, isEquivalence_iff_of_iso, CategoryTheory.Subobject.instIsEquivalenceMonoOverRepresentative, instIsEquivalenceOppositeOp, CategoryTheory.prod.rightUnitor_isEquivalence, instIsEquivalenceObjWhiskeringLeft, CategoryTheory.Over.instIsEquivalenceMapOfIsIso, CategoryTheory.Adjunction.isEquivalence_right_of_isEquivalence_left, FintypeCat.instIsEquivalenceUSwitch, instIsEquivalenceLeftExtensionCompPrecomp, instIsEquivalenceLightDiagramLightProfiniteLightDiagramToLightProfinite, HasFibers.equiv, isEquivalence_mapArrow, CategoryTheory.Sum.Swap.isEquivalence, CategoryTheory.instIsEquivalenceDecomposedDecomposedTo, CategoryTheory.Equivalence.isEquivalence_functor, CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.isEquivalence, CategoryTheory.instIsEquivalenceCoalgebraToComonadComonadicAdjunctionComparison, CategoryTheory.Under.instIsEquivalenceObjPost, CategoryTheory.ObjectProperty.instIsEquivalenceFullSubcategoryIsoClosureιOfLE, instIsEquivalenceObjWhiskeringRight, CategoryTheory.ShrinkHoms.instIsEquivalenceInverse, CategoryTheory.prod.leftUnitor_isEquivalence, CategoryTheory.Pseudofunctor.IsStackFor.isEquivalence, CategoryTheory.Adjunction.isEquivalence_left_of_isEquivalence_right, instIsEquivalenceLightDiagram'LightDiagramToLightFunctor, CategoryTheory.Mat.instIsEquivalenceMat_SingleObjMulOppositeEquivalenceSingleObjInverse, HasFibers.instIsEquivalenceFibFiberInducedFunctor, CategoryTheory.Comma.isEquivalence_preRight, isEquivalence_inv, instIsEquivalenceOppositeLeftOp, CategoryTheory.IsSkeletonOf.eqv, IsEquivalence.mk', CategoryTheory.Pseudofunctor.DescentData.isEquivalence_toDescentData_iff_of_sieve_eq, CategoryTheory.instIsEquivalenceShiftFunctor, localCohomology.SelfLERadical.cast_isEquivalence, CategoryTheory.MonadicRightAdjoint.eqv, CategoryTheory.Equivalence.fullyFaithfulToEssImage, instIsEquivalenceOppositeRightOp, CategoryTheory.ShrinkHoms.instIsEquivalenceFunctor, CategoryTheory.CostructuredArrow.isEquivalence_toOver, IsLocalization.isEquivalence, CategoryTheory.LocalizerMorphism.isEquivalence_iff, CategoryTheory.instIsEquivalenceAlgebraToMonadMonadicAdjunctionComparison, instIsEquivalenceLightProfiniteLightDiagramLightProfiniteToLightDiagram, CategoryTheory.RelCat.instIsEquivalenceOppositeOpFunctor, ModuleCat.forget₂AddCommGroupIsEquivalence, CategoryTheory.ObjectProperty.isEquivalence_ιOfLE_iff, isEquivalence_of_comp_right, CategoryTheory.CostructuredArrow.isEquivalence_post, CategoryTheory.Equivalence.inducedFunctorOfEquiv, AlgebraicGeometry.AffineScheme.ΓIsEquiv, CategoryTheory.Pretriangulated.instIsEquivalenceTriangleInvRotate, CategoryTheory.Localization.isEquivalence, CategoryTheory.Pretriangulated.instIsEquivalenceTriangleRotate, instIsEquivalenceRightExtensionCompPrecomp
asEquivalence 📖	CompOp	3 math math: asEquivalence_functor, fun_inv_map, inv_fun_map
inv 📖	CompOp	3 math math: fun_inv_map, isEquivalence_inv, inv_fun_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
asEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor asEquivalence	—	—
fun_inv_map 📖	mathematical	—	map obj inv CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct comp CategoryTheory.Equivalence.inverse asEquivalence CategoryTheory.Equivalence.functor id CategoryTheory.NatTrans.app CategoryTheory.Equivalence.counit CategoryTheory.Equivalence.counitInv	—	CategoryTheory.NatIso.naturality_2
instIsEquivalenceObjWhiskeringLeft 📖	mathematical	—	IsEquivalence CategoryTheory.Functor category obj whiskeringLeft	—	CategoryTheory.Equivalence.isEquivalence_inverse
instIsEquivalenceObjWhiskeringRight 📖	mathematical	—	IsEquivalence CategoryTheory.Functor category obj whiskeringRight	—	CategoryTheory.Equivalence.isEquivalence_functor
inv_fun_map 📖	mathematical	—	map inv obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct comp CategoryTheory.Equivalence.functor asEquivalence CategoryTheory.Equivalence.inverse id CategoryTheory.NatTrans.app CategoryTheory.Equivalence.unitInv CategoryTheory.Equivalence.unit	—	CategoryTheory.NatIso.naturality_1
isEquivalence_iff_of_iso 📖	mathematical	—	IsEquivalence	—	isEquivalence_of_iso
isEquivalence_inv 📖	mathematical	—	IsEquivalence inv	—	CategoryTheory.Equivalence.isEquivalence_functor
isEquivalence_of_comp_left 📖	mathematical	—	IsEquivalence	—	isEquivalence_iff_of_iso CategoryTheory.Equivalence.isEquivalence_functor
isEquivalence_of_comp_right 📖	mathematical	—	IsEquivalence	—	isEquivalence_iff_of_iso CategoryTheory.Equivalence.isEquivalence_functor
isEquivalence_of_iso 📖	mathematical	—	IsEquivalence	—	CategoryTheory.Equivalence.isEquivalence_functor
isEquivalence_refl 📖	mathematical	—	IsEquivalence id	—	CategoryTheory.Equivalence.isEquivalence_functor
isEquivalence_trans 📖	mathematical	—	IsEquivalence comp	—	Faithful.comp IsEquivalence.faithful Full.comp IsEquivalence.full essSurj_comp IsEquivalence.essSurj

CategoryTheory.Functor.IsEquivalence

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
essSurj 📖	mathematical	—	CategoryTheory.Functor.EssSurj	—	—
faithful 📖	mathematical	—	CategoryTheory.Functor.Faithful	—	—
full 📖	mathematical	—	CategoryTheory.Functor.Full	—	—
mk' 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence	—	CategoryTheory.Equivalence.isEquivalence_functor

CategoryTheory.Iso

Definitions

Name	Category	Theorems
compInverseIso 📖	CompOp	4 math math: CategoryTheory.MonoidalClosed.ofEquiv_uncurry_def, compInverseIso_inv_app, compInverseIso_hom_app, CategoryTheory.MonoidalClosed.ofEquiv_curry_def
inverseCompIso 📖	CompOp	2 math math: inverseCompIso_inv_app, inverseCompIso_hom_app
isoCompInverse 📖	CompOp	4 math math: CategoryTheory.CostructuredArrow.overEquivPresheafCostructuredArrow_inverse_map_toOverCompCoyoneda, isoCompInverse_inv_app, isoCompInverse_hom_app, CategoryTheory.CostructuredArrow.overEquivPresheafCostructuredArrow_inverse_map_toOverCompYoneda
isoFunctorOfIsoInverse 📖	CompOp	4 math math: isoFunctorOfIsoInverse_isoInverseOfIsoFunctor, isoInverseOfIsoFunctor_isoFunctorOfIsoInverse, isoFunctorOfIsoInverse_inv_app, isoFunctorOfIsoInverse_hom_app
isoInverseComp 📖	CompOp	2 math math: isoInverseComp_inv_app, isoInverseComp_hom_app
isoInverseOfIsoFunctor 📖	CompOp	5 math math: isoFunctorOfIsoInverse_isoInverseOfIsoFunctor, isoInverseOfIsoFunctor_isoFunctorOfIsoInverse, CategoryTheory.Equivalence.inverseFunctorMapIso_symm_eq_isoInverseOfIsoFunctor, isoInverseOfIsoFunctor_inv_app, isoInverseOfIsoFunctor_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compInverseIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse hom CategoryTheory.Functor CategoryTheory.Functor.category compInverseIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor CategoryTheory.Functor.map CategoryTheory.Functor.id inv CategoryTheory.Equivalence.unitIso	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
compInverseIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse inv CategoryTheory.Functor CategoryTheory.Functor.category compInverseIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor CategoryTheory.Functor.id hom CategoryTheory.Equivalence.unitIso CategoryTheory.Functor.map	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
inverseCompIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse hom CategoryTheory.Functor CategoryTheory.Functor.category inverseCompIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor CategoryTheory.Functor.map CategoryTheory.Functor.id CategoryTheory.Equivalence.counitIso	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
inverseCompIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse inv CategoryTheory.Functor CategoryTheory.Functor.category inverseCompIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor CategoryTheory.Functor.map CategoryTheory.Functor.id CategoryTheory.Equivalence.counitIso	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
isoCompInverse_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse hom CategoryTheory.Functor CategoryTheory.Functor.category isoCompInverse CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor CategoryTheory.Functor.id CategoryTheory.Equivalence.unitIso CategoryTheory.Functor.map	—	CategoryTheory.Category.id_comp
isoCompInverse_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse inv CategoryTheory.Functor CategoryTheory.Functor.category isoCompInverse CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor CategoryTheory.Functor.map CategoryTheory.Functor.id CategoryTheory.Equivalence.unitIso	—	CategoryTheory.Category.comp_id
isoFunctorOfIsoInverse_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.symm hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.functor isoFunctorOfIsoInverse CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp inv CategoryTheory.Equivalence.counitIso CategoryTheory.Functor.map CategoryTheory.Equivalence.unitIso	—	isoCompInverse_hom_app CategoryTheory.Functor.map_comp CategoryTheory.Category.comp_id
isoFunctorOfIsoInverse_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.symm inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.functor isoFunctorOfIsoInverse CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Functor.id CategoryTheory.Functor.comp hom CategoryTheory.Equivalence.unitIso CategoryTheory.Equivalence.counitIso	—	isoCompInverse_inv_app CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.Category.id_comp
isoFunctorOfIsoInverse_isoInverseOfIsoFunctor 📖	mathematical	—	isoFunctorOfIsoInverse isoInverseOfIsoFunctor	—	ext CategoryTheory.NatTrans.ext' isoFunctorOfIsoInverse_hom_app isoInverseOfIsoFunctor_inv_app CategoryTheory.Functor.map_comp CategoryTheory.Equivalence.fun_inv_map CategoryTheory.Category.assoc CategoryTheory.Equivalence.counitInv_functor_comp CategoryTheory.Category.comp_id inv_hom_id_app_assoc CategoryTheory.Equivalence.counitInv_functor_comp_assoc
isoInverseComp_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse hom CategoryTheory.Functor CategoryTheory.Functor.category isoInverseComp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor CategoryTheory.Functor.map CategoryTheory.Functor.id inv CategoryTheory.Equivalence.counitIso	—	CategoryTheory.Category.id_comp
isoInverseComp_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse inv CategoryTheory.Functor CategoryTheory.Functor.category isoInverseComp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor CategoryTheory.Functor.map CategoryTheory.Functor.id hom CategoryTheory.Equivalence.counitIso	—	CategoryTheory.Category.comp_id
isoInverseOfIsoFunctor_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Equivalence.inverse hom CategoryTheory.Functor CategoryTheory.Functor.category isoInverseOfIsoFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Equivalence.unitIso CategoryTheory.Functor.map inv CategoryTheory.Equivalence.counitIso	—	isoCompInverse_hom_app CategoryTheory.Functor.map_comp CategoryTheory.Category.comp_id
isoInverseOfIsoFunctor_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Equivalence.inverse inv CategoryTheory.Functor CategoryTheory.Functor.category isoInverseOfIsoFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor CategoryTheory.Functor.map CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Equivalence.counitIso hom CategoryTheory.Equivalence.unitIso	—	isoCompInverse_inv_app CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.Category.id_comp
isoInverseOfIsoFunctor_isoFunctorOfIsoInverse 📖	mathematical	—	isoInverseOfIsoFunctor isoFunctorOfIsoInverse	—	isoFunctorOfIsoInverse_isoInverseOfIsoFunctor

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
fullSubcategoryCongr 📖	CompOp	4 math math: fullSubcategoryCongr_inverse, fullSubcategoryCongr_unitIso, fullSubcategoryCongr_counitIso, fullSubcategoryCongr_functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fullSubcategoryCongr_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso FullSubcategory FullSubcategory.category fullSubcategoryCongr CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp ιOfLE	—	—
fullSubcategoryCongr_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor FullSubcategory FullSubcategory.category fullSubcategoryCongr ιOfLE	—	—
fullSubcategoryCongr_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse FullSubcategory FullSubcategory.category fullSubcategoryCongr ιOfLE	—	—
fullSubcategoryCongr_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso FullSubcategory FullSubcategory.category fullSubcategoryCongr CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id	—	—

---

← Back to Index