| Name | Category | Theorems |
|---|
associator π | CompOp | 280 mathmath: Bicategory.Opposite.op2_associator, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom, CategoryTheory.LaxFunctor.mapComp'_whiskerRight_comp_mapComp', CategoryTheory.Pseudofunctor.mapβ_associator_assoc, CategoryTheory.LaxFunctor.mapβ_associator_assoc, CategoryTheory.LaxFunctor.whiskerLeft_mapComp'_comp_mapComp'_assoc, Comonad.comul_assoc_flip, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_comp_mapComp'βββ_hom_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_app_assoc, Bicategory.Opposite.op2_associator_inv, CategoryTheory.Pseudofunctor.mapβ_associator_app_assoc, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerRight_naturality, CategoryTheory.Lax.StrongTrans.vComp_naturality_hom, Adj.associator_inv_Οr, whiskerRight_comp_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_comp_mapComp'_hom_whiskerRight_assoc, CategoryTheory.Cat.Hom.toNatIso_associator, InducedBicategory.bicategory_associator_inv_hom, CategoryTheory.OplaxFunctor.mapβ_associator, mateEquiv_comp_id_right, CategoryTheory.Cat.associator_hom_app, pentagon_inv, Adjunction.homEquivβ_symm_apply, CategoryTheory.OplaxFunctor.mapβ_associator_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp'_hom_comp_whiskerLeft_mapComp'_hom, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp_assoc, CategoryTheory.StrictlyUnitaryLaxFunctorCore.mapβ_associator, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_comp_naturality_hom, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_comp_whiskerLeft_mapComp'_hom, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id_assoc, pentagon_hom_hom_inv_hom_hom_assoc, associatorNatIsoLeft_inv_app, pentagon_inv_hom_hom_hom_hom, CategoryTheory.OplaxFunctor.mapComp_assoc_left_app_assoc, Adjunction.homEquivβ_apply, CategoryTheory.StrictPseudofunctorCore.mapβ_associator, associator_inv_naturality_middle, associator_naturality_right_assoc, triangle_assoc_comp_left, associator_inv_naturality_right, CategoryTheory.Pseudofunctor.mapComp'βββ_inv, whiskerRight_comp_symm, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv, associator_eqToHom_hom_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality, CategoryTheory.Oplax.LaxTrans.naturality_comp_assoc, mateEquiv_id_comp_right, leftUnitor_comp_inv, Bicategory.Opposite.bicategory_associator_hom_unop2, CategoryTheory.LaxFunctor.mapComp_assoc_right_app, CategoryTheory.Oplax.OplaxTrans.associator_hom_as_app, pentagon_inv_hom_hom_hom_inv, CategoryTheory.Pseudofunctor.mapβ_associator_app, CategoryTheory.Lax.OplaxTrans.naturality_comp, leftUnitor_inv_whiskerRight_assoc, whiskerRight_comp_symm_assoc, CategoryTheory.Oplax.StrongTrans.Modification.whiskerRight_naturality, CategoryTheory.Pseudofunctor.mapComp'βββ_hom, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_naturality, comp_whiskerLeft_symm, CategoryTheory.Oplax.StrongTrans.naturality_comp, CategoryTheory.Oplax.OplaxTrans.associator_inv_as_app, Adjunction.homEquivβ_apply, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app, CategoryTheory.Oplax.OplaxTrans.naturality_comp, CategoryTheory.Lax.LaxTrans.naturality_comp, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_naturality_assoc, CategoryTheory.OplaxFunctor.mapComp_assoc_left_app, CategoryTheory.Lax.OplaxTrans.vComp_naturality_comp, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_comp_whiskerLeft_mapComp'_hom_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_assoc, associator_inv_naturality_left, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_comp_mapComp'_inv, CategoryTheory.Cat.associator_inv_app, associator_naturality_right, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_id, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_associator_hom_as_app, Comonad.comul_assoc_flip_assoc, CategoryTheory.OplaxFunctor.mapβ_associator_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp, CategoryTheory.LaxFunctor.mapβ_associator_app_assoc, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_comp_assoc, whiskerLeft_rightUnitor_assoc, leftUnitor_inv_whiskerRight, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality_assoc, CategoryTheory.StrictlyUnitaryPseudofunctorCore.mapβ_associator, associator_eqToHom_inv, Mathlib.Tactic.Bicategory.naturality_associator, CategoryTheory.Pseudofunctor.mapComp'βββ_hom, CategoryTheory.Oplax.OplaxTrans.categoryStruct_comp_naturality, CategoryTheory.OplaxFunctor.mapComp_assoc_right_app, pentagon_inv_inv_hom_hom_inv, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_assoc, CategoryTheory.OplaxFunctor.mapComp_assoc_left, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp_assoc, CategoryTheory.Lax.LaxTrans.naturality_comp_assoc, pentagon_assoc, CategoryTheory.Oplax.LaxTrans.naturality_comp, pentagon_inv_inv_hom_inv_inv, CategoryTheory.OplaxFunctor.mapComp'_comp_mapComp'_whiskerRight, CategoryTheory.OplaxFunctor.mapβ_associator_assoc, CategoryTheory.LaxFunctor.mapComp'_whiskerRight_comp_mapComp'_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id, prod_associator_inv_fst, whiskerLeft_rightUnitor_inv, CategoryTheory.Pseudofunctor.mapComp'βββ_inv, Pith.associator_hom_iso, CategoryTheory.Lax.StrongTrans.naturality_comp_assoc, associator_naturality_left_assoc, triangle_assoc_comp_right_inv_assoc, CategoryTheory.LaxFunctor.whiskerLeft_mapComp'_comp_mapComp', triangle_assoc_comp_right_inv, associator_naturality_middle, CategoryTheory.Oplax.LaxTrans.vComp_naturality_comp, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp_assoc, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_app_assoc, mateEquiv_symm_apply, leftUnitor_whiskerRight, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp_assoc, associator_eqToHom_inv_assoc, CategoryTheory.associator_def, CategoryTheory.OplaxFunctor.mapComp_assoc_right_app_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_assoc, pentagon, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_assoc, CategoryTheory.Oplax.StrongTrans.categoryStruct_comp_naturality, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_assoc, LeftLift.whisker_unit, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id_assoc, pentagon_hom_hom_inv_inv_hom_assoc, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_comp, associator_hom_congr, pentagon_inv_inv_hom_inv_inv_assoc, Comonad.comul_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom, comp_whiskerLeft, prod_associator_hom_fst, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'βββ_inv, CategoryTheory.LaxFunctor.mapβ_associator, associator_inv_naturality_left_assoc, CategoryTheory.Oplax.StrongTrans.naturality_comp_assoc, CategoryTheory.OplaxFunctor.mapComp_assoc_right, mateEquiv_eq_iff, CategoryTheory.OplaxFunctor.mapComp_assoc_left_assoc, pentagon_inv_assoc, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_id_assoc, whiskerRight_comp, CategoryTheory.Pseudofunctor.StrongTrans.associator_inv_as_app, pentagon_inv_hom_hom_hom_hom_assoc, whisker_assoc_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_comp_mapComp'βββ_hom, associator_eqToHom_hom, whisker_assoc_symm, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_comp, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_app, CategoryTheory.Cat.associator_inv_toNatTrans, associator_inv_naturality_right_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp, triangle, CategoryTheory.Pseudofunctor.mapComp'_inv_comp_mapComp'_hom, rightUnitor_comp, triangle_assoc_comp_right, comp_whiskerLeft_assoc, associatorNatIsoMiddle_hom_app, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_comp_mapComp'βββ_hom_assoc, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'βββ_inv_assoc, CategoryTheory.Lax.StrongTrans.naturality_comp, whisker_assoc_symm_assoc, conjugateEquiv_apply', CategoryTheory.OplaxFunctor.mapComp_assoc_right_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app_assoc, CategoryTheory.FreeBicategory.mk_associator_hom, CategoryTheory.LaxFunctor.mapComp_assoc_left_app, pentagon_hom_inv_inv_inv_hom_assoc, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'_inv, CategoryTheory.Pseudofunctor.StrongTrans.associator_hom_as_app, Pith.associator_inv_iso_inv, rightUnitor_comp_inv, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_comp_naturality_inv, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'βββ_inv_assoc, pentagon_hom_inv_inv_inv_inv_assoc, CategoryTheory.Lax.StrongTrans.vComp_naturality_inv, CategoryTheory.LaxFunctor.mapComp_assoc_right_assoc, CategoryTheory.Oplax.StrongTrans.vcomp_naturality_hom, Adj.Bicategory.associator_inv_Οl, CategoryTheory.Pseudofunctor.mapβ_associator, conjugateEquiv_associator_hom, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_assoc, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerRight_naturality_assoc, Adj.associator_inv_Οl, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_assoc, CategoryTheory.OplaxFunctor.mapComp'_comp_whiskerLeft_mapComp', whisker_assoc, associatorNatIsoRight_hom_app, associator_inv_congr, LeftExtension.whisker_unit, Adj.Bicategory.associator_hom_Οr, associatorNatIsoLeft_hom_app, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom, Adj.associator_hom_Οr, whiskerLeft_rightUnitor_inv_assoc, CategoryTheory.Oplax.OplaxTrans.naturality_comp_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_comp_mapComp'βββ_hom, CategoryTheory.Lax.LaxTrans.vComp_naturality_comp, Pith.associator_inv_iso_hom, prod_associator_inv_snd, CategoryTheory.BicategoricalCoherence.assoc_iso, Comonad.comul_assoc_assoc, associator_naturality_left, Adj.Bicategory.associator_inv_Οr, CategoryTheory.LaxFunctor.mapComp_assoc_left, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_app, CategoryTheory.LaxFunctor.mapComp_assoc_right, mateEquiv_apply, Adj.associator_hom_Οl, InducedBicategory.bicategory_associator_hom_hom, pentagon_hom_hom_inv_inv_hom, Bicategory.Opposite.bicategory_associator_inv_unop2, CategoryTheory.Lax.OplaxTrans.naturality_comp_assoc, pentagon_inv_inv_hom_hom_inv_assoc, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality, CategoryTheory.FreeBicategory.mk_associator_inv, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_comp_assoc, rightUnitor_comp_assoc, Adjunction.homEquivβ_symm_apply, CategoryTheory.Oplax.StrongTrans.Modification.whiskerRight_naturality_assoc, CategoryTheory.Lax.StrongTrans.categoryStruct_comp_naturality, Adj.Bicategory.associator_hom_Οl, conjugateEquiv_symm_apply', CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_iso, whiskerLeft_rightUnitor, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_assoc, pentagon_hom_inv_inv_inv_inv, CategoryTheory.LaxFunctor.mapβ_associator_app, CategoryTheory.OplaxFunctor.mapComp'_comp_mapComp'_whiskerRight_assoc, comp_whiskerLeft_symm_assoc, leftUnitor_comp, CategoryTheory.BicategoricalCoherence.assoc'_iso, CategoryTheory.Cat.associator_hom_toNatTrans, CategoryTheory.LaxFunctor.mapComp_assoc_left_assoc, associatorNatIsoMiddle_inv_app, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_assoc, pentagon_hom_hom_inv_hom_hom, prod_associator_hom_snd, triangle_assoc_comp_left_inv, CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerRight_naturality, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv, CategoryTheory.LaxFunctor.mapComp_assoc_right_app_assoc, associatorNatIsoRight_inv_app, leftUnitor_comp_inv_assoc, leftUnitor_whiskerRight_assoc, CategoryTheory.OplaxFunctor.mapComp'_comp_whiskerLeft_mapComp'_assoc, Bicategory.Opposite.op2_associator_hom, pentagon_hom_inv_inv_inv_hom, CategoryTheory.LaxFunctor.mapComp_assoc_left_app_assoc, associator_inv_naturality_middle_assoc, rightUnitor_comp_inv_assoc, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'βββ_inv, Strict.associator_eqToIso, CategoryTheory.Pseudofunctor.mapComp'_hom_comp_mapComp'_hom_whiskerRight, triangle_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_comp_mapComp'_hom_whiskerRight, CategoryTheory.Oplax.StrongTrans.vcomp_naturality_inv, associator_naturality_middle_assoc, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_associator_inv_as_app, triangle_assoc_comp_right_assoc, pentagon_inv_hom_hom_hom_inv_assoc, leftUnitor_comp_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_app, triangle_assoc_comp_left_inv_assoc, CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerRight_naturality_assoc
|
associatorNatIsoLeft π | CompOp | 2 mathmath: associatorNatIsoLeft_inv_app, associatorNatIsoLeft_hom_app
|
associatorNatIsoMiddle π | CompOp | 2 mathmath: associatorNatIsoMiddle_hom_app, associatorNatIsoMiddle_inv_app
|
associatorNatIsoRight π | CompOp | 2 mathmath: associatorNatIsoRight_hom_app, associatorNatIsoRight_inv_app
|
homCategory π | CompOp | 1253 mathmath: iterated_mateEquiv_conjugateEquiv, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id, CategoryTheory.Pseudofunctor.mapComp'_naturality_1_assoc, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_assoc, CategoryTheory.Pseudofunctor.DescentData.isEquivalence_toDescentData_of_sieve_le, prod_whiskerLeft_snd, Bicategory.Opposite.op2_associator, CategoryTheory.StrictPseudofunctorPreCore.map_id, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_mapβ_toNatTrans_app, CategoryTheory.Pseudofunctor.DescentData.ofObj_hom, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom, RightExtension.w_assoc, CategoryTheory.Pseudofunctor.DescentData.subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv, CategoryTheory.LaxFunctor.mapComp'_whiskerRight_comp_mapComp', CategoryTheory.Oplax.StrongTrans.Modification.vcomp_app, AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_adj, CategoryTheory.Pseudofunctor.mapβ_associator_assoc, CategoryTheory.LaxFunctor.mapβ_associator_assoc, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map, CategoryTheory.LaxFunctor.whiskerLeft_mapComp'_comp_mapComp'_assoc, Adj.rightUnitor_hom_Οl, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_naturality_assoc, Comonad.comul_assoc_flip, Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil, CategoryTheory.OplaxFunctor.id_mapComp, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_comp_mapComp'βββ_hom_assoc, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_mapβ, eqToHomTransIso_refl_left, CategoryTheory.StrictlyUnitaryLaxFunctor.id_mapβ, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_app_assoc, Bicategory.Opposite.op2_associator_inv, CategoryTheory.Pseudofunctor.mapβ_associator_app_assoc, Pith.inclusion_mapComp, Pith.pseudofunctorToPith_mapId_hom_iso, CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_inv_app_hom, CategoryTheory.Pseudofunctor.isEquivalence_toDescentData, conjugateEquiv_whiskerRight, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerRight_naturality, LeftLift.whiskering_map, leftUnitor_inv_naturality_assoc, CategoryTheory.Lax.StrongTrans.vComp_naturality_hom, whiskerLeft_inv_hom, CategoryTheory.StrictlyUnitaryLaxFunctor.mapIdIso_hom, CategoryTheory.FreeBicategory.lift_mapId, CategoryTheory.StrictlyUnitaryLaxFunctorCore.mapβ_leftUnitor, Adj.associator_inv_Οr, Prod.sectL_mapId_inv, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'βββ_inv_app, whiskerRight_comp_assoc, Prod.snd_map, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_comp_mapComp'_hom_whiskerRight_assoc, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom, InducedBicategory.bicategory_associator_inv_hom, LeftExtension.w_assoc, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality, CategoryTheory.OplaxFunctor.mapβ_associator, inv_hom_whiskerRight_whiskerRight_assoc, Adj.rIso_inv, mateEquiv_comp_id_right, CategoryTheory.Pseudofunctor.StrongTrans.homCategory_comp_as_app, inv_hom_whiskerRight_assoc, whisker_exchange, inv_hom_whiskerRight, CategoryTheory.LaxFunctor.mapβ_leftUnitor_assoc, CategoryTheory.Cat.associator_hom_app, CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_obj, pentagon_inv, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_comp_whiskerLeft_mapComp'_hom_app_assoc, Adjunction.homEquivβ_symm_apply, InducedBicategory.Hom.category_id_hom, CategoryTheory.LaxFunctor.comp_mapId, CategoryTheory.Pseudofunctor.mapβ_left_unitor_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id_app, CategoryTheory.OplaxFunctor.mapβ_associator_app, CategoryTheory.Oplax.LaxTrans.vComp_naturality_id, CategoryTheory.StrictPseudofunctorCore.mapβ_left_unitor, Lan.existsUnique, CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_id_fiber, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_whiskerRight_as_app, CategoryTheory.Oplax.OplaxTrans.Modification.vcomp_app, eqToHomTransIso_refl_refl, CategoryTheory.FreeBicategory.mk_left_unitor_inv, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality_assoc, RightLift.w_assoc, mateEquiv_vcomp, CategoryTheory.Pseudofunctor.StrongTrans.comp_app, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj, CategoryTheory.Pseudofunctor.mapComp'_hom_comp_whiskerLeft_mapComp'_hom, conjugateEquiv_adjunction_id_symm, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_assoc, Adj.comp_Οl_assoc, CategoryTheory.StrictPseudofunctor.mk'_obj, CategoryTheory.Oplax.OplaxTrans.StrongCore.naturality_hom, Adj.forgetβ_mapId, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp_assoc, CategoryTheory.Oplax.OplaxTrans.homCategory_id_as_app, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app, CategoryTheory.BicategoricalCoherence.left'_iso, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app, CategoryTheory.StrictlyUnitaryLaxFunctorCore.mapβ_associator, Pseudofunctor.ofLaxFunctorToLocallyGroupoid_mapCompIso_inv, LeftExtension.ofCompId_right, CategoryTheory.StrictlyUnitaryLaxFunctorCore.mapβ_id, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp_app, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_comp_naturality_hom, CategoryTheory.OplaxFunctor.mapComp_naturality_right_assoc, CategoryTheory.Oplax.LaxTrans.naturality_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_comp_whiskerLeft_mapComp'_hom, CategoryTheory.StrictPseudofunctor.id_mapComp_hom, InducedBicategory.bicategory_leftUnitor_inv_hom, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_app_assoc, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctor_map_hom, CategoryTheory.Pseudofunctor.StrongTrans.leftUnitor_inv_as_app, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_whiskerLeft_as_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv, pentagon_hom_hom_inv_hom_hom_assoc, CategoryTheory.Functor.toPseudoFunctor'_obj, CategoryTheory.Oplax.OplaxTrans.categoryStruct_id_naturality, CategoryTheory.Pseudofunctor.mapId'_inv_naturality_assoc, Adj.Bicategory.rightUnitor_inv_Οr, LeftLift.w_assoc, whiskerRightIso_hom, associatorNatIsoLeft_inv_app, CategoryTheory.StrictlyUnitaryPseudofunctor.mk'_map, CategoryTheory.Pseudofunctor.mapComp_id_left_inv_app, pentagon_inv_hom_hom_hom_hom, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_app_assoc, rightUnitor_inv_naturality, CategoryTheory.OplaxFunctor.mapComp_assoc_left_app_assoc, CategoryTheory.Pseudofunctor.CoGrothendieck.instIsEquivalenceΞ±CategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, Adjunction.homEquivβ_apply, CategoryTheory.StrictPseudofunctorCore.mapβ_associator, Prod.swap_mapβ, CategoryTheory.Pseudofunctor.DescentData.isoMk_inv_hom, Mathlib.Tactic.Bicategory.naturality_rightUnitor, Pith.whiskerRight_iso_inv, rightUnitor_inv_congr, CategoryTheory.Pseudofunctor.mapβ_left_unitor, CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_base, unitors_inv_equal, Adj.forgetβ_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map, Pith.leftUnitor_inv_iso_hom, leftZigzagIso_symm, CategoryTheory.StrictPseudofunctor.mk''_mapId, associator_inv_naturality_middle, associator_naturality_right_assoc, CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_fiber, CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerLeft_naturality_assoc, hom_inv_whiskerRight_whiskerRight_assoc, CategoryTheory.StrictlyUnitaryLaxFunctor.mapId_isIso, triangle_assoc_comp_left, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom, associator_inv_naturality_right, LanLift.CommuteWith.lanLiftCompIso_hom, Pseudofunctor.ofOplaxFunctorToLocallyGroupoid_mapCompIso_hom, CategoryTheory.StrictlyUnitaryPseudofunctor.id_mapComp_hom, CategoryTheory.FreeBicategory.mk_right_unitor_inv, AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_l, whiskerLeft_comp, CategoryTheory.Pseudofunctor.ObjectProperty.ΞΉ_app_toFunctor, conjugateEquiv_symm_id, CategoryTheory.Pseudofunctor.mapComp'βββ_inv, CategoryTheory.Oplax.StrongTrans.Modification.whiskerLeft_naturality, CategoryTheory.LaxFunctor.mapComp_naturality_left_app_assoc, conjugateEquiv_apply, prod_whiskerRight_fst, CategoryTheory.Pseudofunctor.DescentData.comp_hom, whiskerRight_comp_symm, Adj.Bicategory.rightUnitor_inv_Οl, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv, Pith.compβ_iso_hom_assoc, CategoryTheory.Cat.leftUnitor_hom_app, associator_eqToHom_hom_assoc, whiskerRight_id, CategoryTheory.OplaxFunctor.mapβ_leftUnitor_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality, CategoryTheory.Oplax.LaxTrans.naturality_comp_assoc, CategoryTheory.Oplax.OplaxTrans.categoryStruct_comp_app, CategoryTheory.LaxFunctor.id_mapId, CategoryTheory.StrictPseudofunctor.id_obj, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_id, CategoryTheory.Oplax.StrongTrans.homCategory_id_as_app, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_naturality, InducedBicategory.eqToHom_hom, CategoryTheory.Pseudofunctor.Grothendieck.ext_iff, lanLiftUnit_desc_assoc, whiskerLeft_hom_inv, CategoryTheory.Lax.LaxTrans.id_app, CategoryTheory.StrictlyUnitaryLaxFunctor.id_obj, CategoryTheory.Pseudofunctor.mapComp'_inv_naturality, mateEquiv_id_comp_right, leftUnitor_comp_inv, CategoryTheory.Pseudofunctor.mapComp_id_left, CategoryTheory.Iso.unop2_inv, postcomp_obj, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality_app, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'βββ_inv_app, CategoryTheory.StrictlyUnitaryPseudofunctorCore.mapβ_whisker_right, CategoryTheory.StrictPseudofunctor.comp_mapComp_hom, leftZigzagIso_hom, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_mapComp, CategoryTheory.Functor.toOplaxFunctor'_obj, Bicategory.Opposite.bicategory_associator_hom_unop2, CategoryTheory.OplaxFunctor.PseudoCore.mapCompIso_hom, CategoryTheory.StrictPseudofunctor.comp_mapId_hom, Bicategory.Opposite.unop2_id_bop, CategoryTheory.LaxFunctor.mapComp_assoc_right_app, LeftExtension.ofCompId_left_as, CategoryTheory.Oplax.OplaxTrans.associator_hom_as_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id, CategoryTheory.Pseudofunctor.toOplax_mapComp, Bicategory.Opposite.unopFunctor_map, CategoryTheory.BicategoricalCoherence.tensorRight_iso, inv_hom_whiskerRight_whiskerRight, Prod.sectR_mapComp_inv, Prod.fst_mapComp_hom, whiskerLeft_whiskerLeft_hom_inv_assoc, id_whiskerLeft_symm, CategoryTheory.Pseudofunctor.mapComp'_naturality_1, CategoryTheory.Pseudofunctor.isStackFor_ofArrows_iff, CategoryTheory.LaxFunctor.mapβ_leftUnitor_hom_app, Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_of, LeftLift.IsKan.fac_assoc, postcomposing_obj, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_app, pentagon_inv_hom_hom_hom_inv, Adj.rightUnitor_inv_Οl, Adj.Homβ.conjugateEquiv_symm_Οr, CategoryTheory.LaxFunctor.PseudoCore.mapCompIso_inv, CategoryTheory.Pseudofunctor.mapComp_id_right_inv_app_assoc, CategoryTheory.StrictlyUnitaryLaxFunctor.comp_mapId, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp_val_app, CategoryTheory.Pseudofunctor.mapβ_associator_app, CategoryTheory.Cat.rightUnitor_hom_toNatTrans, Prod.snd_mapβ, CategoryTheory.Lax.OplaxTrans.naturality_comp, leftUnitor_inv_whiskerRight_assoc, whiskerRight_comp_symm_assoc, CategoryTheory.Pseudofunctor.DescentData.iso_hom, CategoryTheory.Oplax.StrongTrans.Modification.whiskerRight_naturality, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app_assoc, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_naturality_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.mk'_mapId, CategoryTheory.StrictlyUnitaryPseudofunctor.id_mapId_inv, CategoryTheory.Pseudofunctor.mapComp'βββ_hom, Adj.rightUnitor_hom_Οr, Pith.pseudofunctorToPith_mapId_inv_iso_inv, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality, CategoryTheory.Pseudofunctor.mapComp_id_right, LeftExtension.whiskering_map, comp_whiskerRight, CategoryTheory.BicategoricalCoherence.left_iso, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_naturality, CategoryTheory.Pseudofunctor.mapComp'_inv_naturality_assoc, Bicategory.Opposite.bicategory_leftUnitor_hom_unop2, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id_app, comp_whiskerLeft_symm, inv_whiskerRight, CategoryTheory.StrictlyUnitaryPseudofunctor.id_mapComp_inv, Pith.idβ_iso_inv, mateEquiv_symm_apply', CategoryTheory.Oplax.LaxTrans.naturality_naturality, CategoryTheory.Pseudofunctor.mapComp'_comp_id, CategoryTheory.Oplax.StrongTrans.naturality_comp, CategoryTheory.OplaxFunctor.mapβ_leftUnitor_assoc, CategoryTheory.Functor.toPseudoFunctor'_map, conjugateEquiv_id_comp_right_apply, CategoryTheory.Oplax.OplaxTrans.associator_inv_as_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp_app, CategoryTheory.Pseudofunctor.presheafHom_obj, Adjunction.homEquivβ_apply, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_assoc, CategoryTheory.Oplax.StrongTrans.naturality_id_assoc, CategoryTheory.StrictlyUnitaryLaxFunctorCore.mapComp_naturality_right, Adj.forgetβ_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app, CategoryTheory.Oplax.LaxTrans.naturality_id, CategoryTheory.StrictlyUnitaryPseudofunctorCore.mapβ_left_unitor, CategoryTheory.Pseudofunctor.toLax_mapComp, CategoryTheory.Pseudofunctor.isoMapOfCommSq_horiz_id, CategoryTheory.Oplax.OplaxTrans.naturality_comp, CategoryTheory.Lax.LaxTrans.naturality_comp, CategoryTheory.Pseudofunctor.DescentData.iso_inv, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_naturality_assoc, CategoryTheory.Oplax.StrongTrans.id_naturality_inv, CategoryTheory.OplaxFunctor.mapComp_assoc_left_app, CategoryTheory.Lax.OplaxTrans.vComp_naturality_comp, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_comp_whiskerLeft_mapComp'_hom_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_assoc, CategoryTheory.Oplax.LaxTrans.id_app, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_leftUnitor_inv_as_app, CategoryTheory.Pseudofunctor.mapβ_right_unitor_assoc, Prod.sectL_mapComp_hom, associator_inv_naturality_left, CategoryTheory.Pseudofunctor.CoGrothendieck.instFullΞ±CategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_comp_mapComp'_inv, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality_app, leftUnitor_inv_naturality, whiskerLeft_whiskerLeft_inv_hom, CategoryTheory.Pseudofunctor.DescentData.nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq, unitors_equal, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerLeft_naturality_assoc, CategoryTheory.Cat.associator_inv_app, associator_naturality_right, whiskerRightIso_inv, precomposing_map_app, Prod.sectL_obj, CategoryTheory.Cat.rightUnitor_hom_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_app_assoc, CategoryTheory.Oplax.LaxTrans.id_naturality, CategoryTheory.Pseudofunctor.ObjectProperty.ΞΉ_naturality, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_id, CategoryTheory.Pseudofunctor.mapComp_id_right_hom, conjugateEquiv_symm_of_iso, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp, CategoryTheory.Oplax.StrongTrans.Modification.naturality_assoc, CategoryTheory.LaxFunctor.mapComp_naturality_right_app_assoc, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_associator_hom_as_app, CategoryTheory.Lax.LaxTrans.vComp_naturality_naturality, prod_whiskerRight_snd, CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_mapβ, Adj.Bicategory.rightUnitor_hom_Οr, CategoryTheory.StrictPseudofunctor.comp_mapId_inv, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_obj, Adj.id_Οl, Adj.comp_Οl, CategoryTheory.Pseudofunctor.ObjectProperty.mapId_inv_app, CategoryTheory.PrelaxFunctor.mkOfHomFunctors_toPrelaxFunctorStruct, Comonad.comul_assoc_flip_assoc, CategoryTheory.OplaxFunctor.mapβ_associator_app_assoc, CategoryTheory.StrictPseudofunctor.mk'_mapComp, CategoryTheory.Pseudofunctor.mapComp_id_left_hom_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp, CategoryTheory.LaxFunctor.mapβ_associator_app_assoc, conjugateEquiv_comp_id_right_apply, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_mapβ_toNatTrans, CategoryTheory.Lax.LaxTrans.id_naturality, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_comp_assoc, whiskerLeft_rightUnitor_assoc, leftUnitor_inv_whiskerRight, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality_assoc, CategoryTheory.StrictlyUnitaryPseudofunctorCore.mapβ_associator, CategoryTheory.pseudofunctorOfIsLocallyDiscrete_obj, CategoryTheory.Functor.toOplaxFunctor_obj, instIsIsoHomLeftZigzagHom, Prod.fst_mapβ, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_comp_mapComp'_hom_whiskerRight_app, Equivalence.right_triangle, CategoryTheory.Functor.toPseudoFunctor_mapComp, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_obj, CategoryTheory.Oplax.OplaxTrans.categoryStruct_id_app, InducedBicategory.forget_map, CategoryTheory.Pseudofunctor.DescentData.instIsIsoΞ±CategoryObjLocallyDiscreteOppositeCatMkOpHom, associator_eqToHom_inv, Equivalence.left_triangle, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_app, CategoryTheory.LaxFunctor.mapβ_leftUnitor_hom_app_assoc, CategoryTheory.PrelaxFunctor.mapβ_eqToHom, Mathlib.Tactic.Bicategory.naturality_associator, Lan.CommuteWith.lanCompIso_inv, CategoryTheory.Pseudofunctor.mapComp'βββ_hom, LanLift.existsUnique, CategoryTheory.Oplax.OplaxTrans.categoryStruct_comp_naturality, CategoryTheory.Iso.op2_hom_unop2, Bicategory.Opposite.bicategory_leftUnitor_inv_unop2, Prod.sectR_mapId_inv, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_naturality, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_app, CategoryTheory.PrelaxFunctor.mapβ_hom_inv, CategoryTheory.StrictlyUnitaryLaxFunctor.id_mapComp, CategoryTheory.OplaxFunctor.mapComp_assoc_right_app, CategoryTheory.Pseudofunctor.CoGrothendieck.ΞΉ_map_base, CategoryTheory.Pseudofunctor.StrongTrans.Modification.naturality, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp_app, CommRingCat.moduleCatRestrictScalarsPseudofunctor_map, pentagon_inv_inv_hom_hom_inv, CategoryTheory.Pseudofunctor.StrongTrans.homCategory_id_as_app, CategoryTheory.Pseudofunctor.isPrestackFor_ofArrows_iff, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_assoc, CategoryTheory.FreeBicategory.mk_left_unitor_hom, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_app_assoc, CategoryTheory.Pseudofunctor.CoGrothendieck.map_obj_fiber, Pseudofunctor.ofLaxFunctorToLocallyGroupoid_mapIdIso_inv, CategoryTheory.oplaxFunctorOfIsLocallyDiscrete_map, CategoryTheory.Pseudofunctor.whiskerLeftIso_mapId, Lan.CommuteWith.lanCompIsoWhisker_hom_right, Prod.swap_map, CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_hom_app, Pith.rightUnitor_hom_iso, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_id_assoc, Comonad.counit_comul_assoc, CategoryTheory.OplaxFunctor.mapComp_assoc_left, Bicategory.Opposite.op2_rightUnitor_inv, CategoryTheory.LaxFunctor.mapβ_rightUnitor_hom_app, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp_assoc, CategoryTheory.Pseudofunctor.id_mapId, CategoryTheory.Pseudofunctor.DescentData.Hom.comm_assoc, CategoryTheory.BicategoricalCoherence.right'_iso, CategoryTheory.Lax.LaxTrans.naturality_comp_assoc, pentagon_assoc, CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj, Adj.id_Οr, CategoryTheory.Oplax.StrongTrans.Modification.id_app, prod_rightUnitor_inv_fst, CategoryTheory.Pseudofunctor.mapComp_id_left_inv_app_assoc, CategoryTheory.Oplax.LaxTrans.naturality_comp, Adj.Bicategory.leftUnitor_hom_Οl, CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_mapβ, CategoryTheory.Functor.toPseudoFunctor_map, whiskerLeft_isIso, CategoryTheory.Oplax.StrongTrans.isoMk_hom_as_app, conjugateIsoEquiv_apply_inv, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id_app, CategoryTheory.PrelaxFunctor.mapβ_inv_hom_isIso, CategoryTheory.Pseudofunctor.mapComp'_hom_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp'_naturality_2_assoc, CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_id_fiber, eqToHomTransIso_refl_right, CategoryTheory.Pseudofunctor.ObjectProperty.map_map_hom, CategoryTheory.Pseudofunctor.mapComp_id_left_inv_assoc, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality_app, pentagon_inv_inv_hom_inv_inv, CategoryTheory.PrelaxFunctor.mapβ_inv_hom_isIso_assoc, CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.congr, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_comp_mapComp'βββ_hom_app, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app_assoc, CategoryTheory.Lax.LaxTrans.naturality_id_assoc, CategoryTheory.LaxFunctor.mapComp_naturality_right_assoc, CategoryTheory.FreeBicategory.preinclusion_mapβ, CategoryTheory.OplaxFunctor.mapComp'_comp_mapComp'_whiskerRight, Pith.pseudofunctorToPith_mapComp_inv_iso_inv, prod_whiskerLeft_fst, CategoryTheory.Oplax.OplaxTrans.rightUnitor_hom_as_app, CategoryTheory.OplaxFunctor.mapβ_associator_assoc, precomp_obj, CategoryTheory.Pseudofunctor.mapβ_whisker_left, CategoryTheory.LaxFunctor.mapComp'_whiskerRight_comp_mapComp'_assoc, CategoryTheory.Pseudofunctor.StrongTrans.isoMk_hom_as_app, adjointifyCounit_left_triangle, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_assoc, CategoryTheory.Lax.StrongTrans.toLax_naturality, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id, CategoryTheory.Pseudofunctor.toOplax_mapId, prod_associator_inv_fst, whiskerLeft_rightUnitor_inv, CategoryTheory.PrelaxFunctor.mapβ_hom_inv_assoc, Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons, CategoryTheory.StrictlyUnitaryLaxFunctor.mapId_eq_eqToHom, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id, CategoryTheory.OplaxFunctor.mapComp_naturality_left_app, CategoryTheory.StrictlyUnitaryLaxFunctor.map_id, CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerLeft_naturality, CategoryTheory.BicategoricalCoherence.tensorRight'_iso, CategoryTheory.oplaxFunctorOfIsLocallyDiscrete_obj, Pith.whiskerRight_iso_hom, comp_whiskerRight_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_inv, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv, hom_inv_whiskerRight_whiskerRight, Pith.rightUnitor_inv_iso_inv, LeftExtension.whiskerIdCancel_right, prod_rightUnitor_inv_snd, Pith.associator_hom_iso, CategoryTheory.Pseudofunctor.mapComp_id_right_hom_assoc, CategoryTheory.Lax.LaxTrans.naturality_id, CategoryTheory.Pseudofunctor.DescentData.ofObj_obj, CategoryTheory.Lax.StrongTrans.naturality_comp_assoc, associator_naturality_left_assoc, CategoryTheory.StrictPseudofunctorCore.mapβ_right_unitor, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_rightUnitor_inv_as_app, prod_leftUnitor_inv_fst, triangle_assoc_comp_right_inv_assoc, CategoryTheory.LaxFunctor.mapβ_rightUnitor_hom_app_assoc, hom_inv_whiskerRight, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_app, prod_rightUnitor_hom_fst, Adjunction.left_triangle, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id_val_app, CategoryTheory.Pseudofunctor.CoGrothendieck.ext_iff, CategoryTheory.Lax.OplaxTrans.naturality_naturality, CategoryTheory.LaxFunctor.whiskerLeft_mapComp'_comp_mapComp', Prod.fst_mapId_hom, triangle_assoc_comp_right_inv, associator_naturality_middle, CategoryTheory.Pseudofunctor.DescentData.hom_comp_assoc, CategoryTheory.Pseudofunctor.Grothendieck.map_obj_fiber, CategoryTheory.Oplax.LaxTrans.vComp_naturality_comp, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp_assoc, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp, prod_leftUnitor_inv_snd, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_app_assoc, CategoryTheory.StrictPseudofunctor.comp_map, Adj.Bicategory.rightUnitor_hom_Οl, LeftExtension.IsKan.fac_assoc, leftUnitorNatIso_hom_app, CategoryTheory.Pseudofunctor.CoGrothendieck.ΞΉ_obj_fiber, CategoryTheory.Iso.unop2_op_inv, CategoryTheory.PrelaxFunctor.mapβ_inv, CategoryTheory.StrictPseudofunctorPreCore.map_comp, Adj.Bicategory.leftUnitor_inv_Οl, CategoryTheory.StrictPseudofunctor.mk''_map, CategoryTheory.Oplax.StrongTrans.naturality_naturality_assoc, CategoryTheory.Pseudofunctor.isStackFor_iff, Bicategory.Opposite.opFunctor_obj, Prod.sectL_mapId_hom, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_id_naturality_hom, InducedBicategory.bicategory_rightUnitor_hom_hom, CategoryTheory.Pseudofunctor.isoMapOfCommSq_vert_id, LeftExtension.IsKan.uniqueUpToIso_hom_right, CommRingCat.moduleCatExtendScalarsPseudofunctor_map, Pith.whiskerLeft_iso_hom, CategoryTheory.Pseudofunctor.bijective_toDescentData_map_iff, mateEquiv_symm_apply, CategoryTheory.Pseudofunctor.mapβ_whisker_left_assoc, Strict.rightUnitor_eqToIso, leftUnitor_whiskerRight, Bicategory.Opposite.homCategory_comp_unop2, CategoryTheory.Pseudofunctor.CoGrothendieck.ΞΉ_map_fiber, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp_assoc, CategoryTheory.StrictPseudofunctor.toFunctor_obj, CategoryTheory.Oplax.StrongTrans.naturality_id, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_assoc, associator_eqToHom_inv_assoc, CategoryTheory.StrictPseudofunctor.map_comp, CategoryTheory.Functor.toOplaxFunctor'_map, HasLeftKanLift.hasInitial, prod_leftUnitor_hom_snd, CategoryTheory.Pseudofunctor.mapComp_id_left_hom_assoc, CategoryTheory.Pseudofunctor.mapComp_id_right_inv_assoc, CategoryTheory.OplaxFunctor.mapComp_assoc_right_app_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.mapId_eq_eqToIso, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.id_obj, whiskerLeft_inv_hom_whiskerRight_assoc, CategoryTheory.Pseudofunctor.StrongTrans.isoMk_inv_as_app, whisker_exchange_assoc, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_rightUnitor_hom_as_app, InducedBicategory.bicategory_rightUnitor_inv_hom, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv, pentagon, CategoryTheory.Oplax.OplaxTrans.homCategory_comp_as_app, Prod.snd_obj, rightUnitor_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_assoc, CategoryTheory.Lax.OplaxTrans.vComp_naturality_naturality, CategoryTheory.OplaxFunctor.mapβ_rightUnitor_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom, CategoryTheory.StrictlyUnitaryPseudofunctorCore.mapβ_id, CategoryTheory.LocallyDiscrete.mkPseudofunctor_map, CategoryTheory.Lax.LaxTrans.vComp_naturality_id, CategoryTheory.Oplax.OplaxTrans.Modification.naturality_assoc, CategoryTheory.Lax.OplaxTrans.id_naturality, Lan.CommuteWith.lanCompIsoWhisker_inv_right, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObj_obj, CategoryTheory.PrelaxFunctor.mapFunctor_map, whiskerRight_congr, CategoryTheory.Oplax.StrongTrans.categoryStruct_comp_naturality, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_assoc, LeftLift.whisker_unit, CategoryTheory.Oplax.OplaxTrans.naturality_id_assoc, prod_homCategory_id_fst, CategoryTheory.OplaxFunctor.mapβ_leftUnitor, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id_assoc, conjugateEquiv_symm_comp, pentagon_hom_hom_inv_inv_hom_assoc, CategoryTheory.StrictPseudofunctor.mk'_map, mateEquiv_hcomp, CategoryTheory.StrictlyUnitaryLaxFunctor.mk'_obj, CategoryTheory.Lax.LaxTrans.naturality_naturality, Adj.leftUnitor_inv_Οl, CommRingCat.moduleCatExtendScalarsPseudofunctor_obj, Bicategory.Opposite.op2_rightUnitor_hom, whiskerLeft_eqToHom, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_comp, Pith.idβ_iso_hom, associator_hom_congr, Mathlib.Tactic.Bicategory.naturality_leftUnitor, Bicategory.Opposite.unopFunctor_obj, pentagon_inv_inv_hom_inv_inv_assoc, CategoryTheory.Functor.toOplaxFunctor_mapComp, CategoryTheory.LaxFunctor.mapβ_rightUnitor_hom_assoc, Comonad.comul_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom, comp_whiskerLeft, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_app, CategoryTheory.OplaxFunctor.mapComp_naturality_left, CategoryTheory.Lax.StrongTrans.naturality_id, LeftLift.whiskerHom_right, prod_associator_hom_fst, LeftExtension.ofCompId_hom, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_leftUnitor_hom_as_app, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'βββ_inv, prod_homCategory_comp_fst, CategoryTheory.Pseudofunctor.toLax_mapId', CategoryTheory.Lax.StrongTrans.categoryStruct_id_naturality, CategoryTheory.StrictlyUnitaryLaxFunctor.id_map, CategoryTheory.Pseudofunctor.mapComp_id_left_inv, CategoryTheory.WithInitial.pseudofunctor_mapId, CategoryTheory.StrictlyUnitaryPseudofunctorCore.mapβ_whisker_left, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_iso, RingCat.moduleCatRestrictScalarsPseudofunctor_map, CategoryTheory.LaxFunctor.mapβ_associator, associator_inv_naturality_left_assoc, CategoryTheory.OplaxFunctor.mapComp_id_right_assoc, whiskerLeftIso_inv, CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_mapId, CategoryTheory.Oplax.StrongTrans.naturality_comp_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_mapComp_hom, CategoryTheory.Iso.unop2_hom, CategoryTheory.OplaxFunctor.mapComp_assoc_right, mateEquiv_eq_iff, LeftLift.ofIdComp_right, CategoryTheory.OplaxFunctor.mapComp_assoc_left_assoc, InducedBicategory.forget_mapId_inv, CategoryTheory.Pseudofunctor.ObjectProperty.IsClosedUnderMapObj.map_obj, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_comp_mapComp'βββ_hom_app_assoc, postcomposing_map_app, Bicategory.Opposite.op2_comp, pentagon_inv_assoc, CategoryTheory.Pseudofunctor.mapComp'_hom_naturality, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_assoc, CategoryTheory.Pseudofunctor.StrongTrans.Modification.id_app, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_id_assoc, whiskerRight_comp, rightUnitorNatIso_inv_app, CategoryTheory.Pseudofunctor.StrongTrans.associator_inv_as_app, Bicategory.Opposite.op2_leftUnitor_hom, Comonad.comul_counit_assoc, congr_whiskerLeft, CategoryTheory.Pseudofunctor.toLax_mapId, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv, CategoryTheory.Oplax.OplaxTrans.isoMk_hom_as_app, CategoryTheory.Cat.leftUnitor_hom_toNatTrans, pentagon_inv_hom_hom_hom_hom_assoc, whiskerLeft_inv_hom_whiskerRight, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app_assoc, Adj.comp_Οr_assoc, whisker_assoc_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_comp_mapComp'βββ_hom, associator_eqToHom_hom, whisker_assoc_symm, CategoryTheory.Lax.StrongTrans.naturality_naturality_assoc, Prod.sectL_mapComp_inv, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_comp, AlgebraicGeometry.Scheme.Modules.pseudofunctor_obj_obj, id_whiskerLeft_assoc, LeftLift.IsKan.fac, InducedBicategory.forget_mapComp_inv, Bicategory.Opposite.op2_id, CategoryTheory.Pseudofunctor.IsStack.essSurj_of_sieve, toNatTrans_mateEquiv, CategoryTheory.Iso.unop2_op_hom, CategoryTheory.OplaxFunctor.mapβ_rightUnitor, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_app_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_app, CategoryTheory.StrictlyUnitaryLaxFunctorCore.mapComp_naturality_left, CategoryTheory.Cat.associator_inv_toNatTrans, CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_mapβ, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp, Mathlib.Tactic.Bicategory.naturality_id, CategoryTheory.Cat.leftUnitor_inv_toNatTrans, CategoryTheory.Pseudofunctor.mapβ_left_unitor_app, associator_inv_naturality_right_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp, CategoryTheory.StrictPseudofunctor.toFunctor_map, Prod.snd_mapId_hom, hom_inv_whiskerRight_assoc, triangle, CategoryTheory.Pseudofunctor.StrongTrans.leftUnitor_hom_as_app, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_mapId_hom, CategoryTheory.Pseudofunctor.ObjectProperty.mapId_hom_app, CategoryTheory.LaxFunctor.mapβ_leftUnitor_hom_assoc, Prod.sectR_mapβ, CategoryTheory.StrictPseudofunctorPreCore.mapβ_whisker_right, Pseudofunctor.ofOplaxFunctorToLocallyGroupoid_mapIdIso_inv, CategoryTheory.PrelaxFunctor.id_toPrelaxFunctorStruct, CategoryTheory.FreeBicategory.normalize_naturality, Adj.rIso_hom, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom, CategoryTheory.StrictPseudofunctor.id_mapβ, Prod.sectL_map, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_app, conjugateIsoEquiv_apply_hom, id_whiskerRight, conjugateIsoEquiv_symm_apply_hom, CategoryTheory.Pseudofunctor.mapComp'_inv_comp_mapComp'_hom, CategoryTheory.Iso.op2_unop_inv_unop2, Pith.homβ_ext_iff, CategoryTheory.Lax.StrongTrans.naturality_id_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id_assoc, iterated_mateEquiv_conjugateEquiv_symm, Adj.rightUnitor_inv_Οr, CategoryTheory.Oplax.OplaxTrans.naturality_id, rightUnitor_comp, whiskerRight_id_symm, whiskerLeft_whiskerLeft_hom_inv, CategoryTheory.StrictlyUnitaryPseudofunctor.mk'_obj, CategoryTheory.OplaxFunctor.mapComp_id_right, triangle_assoc_comp_right, CategoryTheory.Pseudofunctor.toDescentData_obj, comp_whiskerLeft_assoc, InducedBicategory.forget_mapComp_hom, CategoryTheory.Pseudofunctor.mapComp_id_right_inv, CategoryTheory.StrictlyUnitaryPseudofunctor.id_mapβ, whiskerLeft_inv_hom_assoc, associatorNatIsoMiddle_hom_app, instHasInitialLeftExtensionOfHasLeftKanExtension, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_comp_mapComp'βββ_hom_assoc, CategoryTheory.Pseudofunctor.mapβ_whisker_right_app_assoc, mateEquiv_square, CategoryTheory.Pseudofunctor.StrongTrans.Modification.naturality_assoc, LeftExtension.IsKan.uniqueUpToIso_inv_right, CategoryTheory.Lax.LaxTrans.naturality_naturality_assoc, Adj.forgetβ_toPrelaxFunctor_toPrelaxFunctorStruct_mapβ, rightUnitor_naturality, CategoryTheory.StrictlyUnitaryPseudofunctor.id_map, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_val_app, whiskerLeft_comp_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_iso, Pith.whiskerLeft_iso_inv, rightZigzagIso_symm, Pseudofunctor.ofLaxFunctorToLocallyGroupoid_mapIdIso_hom, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'βββ_inv_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_comp_mapComp'βββ_hom_app, CategoryTheory.LaxFunctor.mapβ_rightUnitor_assoc, CategoryTheory.Lax.StrongTrans.naturality_comp, whiskerLeftIso_hom, CategoryTheory.Lax.OplaxTrans.naturality_id_assoc, Mathlib.Tactic.Bicategory.structuralIso_inv, CategoryTheory.Functor.toOplaxFunctor_map, CategoryTheory.Pseudofunctor.mapβ_whisker_right, whiskerRight_id_assoc, Prod.sectR_obj, CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_apply, whisker_assoc_symm_assoc, conjugateEquiv_apply', mateEquiv_conjugateEquiv_vcomp, CategoryTheory.OplaxFunctor.mapComp_assoc_right_assoc, Adj.Bicategory.leftUnitor_hom_Οr, CategoryTheory.Pseudofunctor.StrongTrans.rightUnitor_inv_as_app, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app_assoc, CategoryTheory.Iso.op2_unop_hom_unop2, CategoryTheory.FreeBicategory.mk_associator_hom, Lan.CommuteWith.lanCompIso_hom, CategoryTheory.LaxFunctor.mapβ_leftUnitor, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_id_naturality_inv, CategoryTheory.LaxFunctor.mapComp_assoc_left_app, conjugateEquiv_adjunction_id, CategoryTheory.Cat.rightUnitor_inv_app, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app_assoc, CategoryTheory.Pseudofunctor.Grothendieck.Hom.ext_iff, Prod.snd_mapId_inv, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_as_app, InducedBicategory.bicategory_homCategory_comp_hom, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_as_app, CategoryTheory.Lax.StrongTrans.naturality_naturality, precomposing_obj, CategoryTheory.Cat.rightUnitor_inv_toNatTrans, pentagon_hom_inv_inv_inv_hom_assoc, CategoryTheory.Functor.toPseudoFunctor_mapId, CategoryTheory.Oplax.OplaxTrans.naturality_naturality, conjugateEquiv_of_iso, CategoryTheory.Pseudofunctor.isPrestackFor_iff, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_assoc, CategoryTheory.bicategoricalComp_refl, LeftLift.ofIdComp_hom, rightZigzagIso_inv, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'_inv, CategoryTheory.Pseudofunctor.StrongTrans.associator_hom_as_app, CategoryTheory.Pseudofunctor.mapβ_right_unitor, CategoryTheory.Lax.LaxTrans.StrongCore.naturality_hom, Pith.associator_inv_iso_inv, rightUnitor_comp_inv, CategoryTheory.Pseudofunctor.IsStackFor.isEquivalence, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_app, whiskerLeft_hom_inv_assoc, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_comp_naturality_inv, LeftLift.whiskerOfIdCompIsoSelf_hom_right, CategoryTheory.Pseudofunctor.CoGrothendieck.instEssSurjΞ±CategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_app_assoc, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'βββ_inv_assoc, Mathlib.Tactic.Bicategory.evalWhiskerRight_nil, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_app_assoc, RingCat.moduleCatRestrictScalarsPseudofunctor_obj, CategoryTheory.pseudofunctorOfIsLocallyDiscrete_map, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp_app, HasLeftKanExtension.hasInitial, CategoryTheory.Pseudofunctor.Grothendieck.Hom.congr, CategoryTheory.PrelaxFunctor.mapβ_comp, Bicategory.Opposite.unop2_comp, CategoryTheory.OplaxFunctor.mapComp_naturality_left_assoc, CategoryTheory.StrictlyUnitaryLaxFunctor.mk'_mapβ, CategoryTheory.PrelaxFunctor.mapFunctor_obj, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_map, CategoryTheory.Pseudofunctor.Grothendieck.map_map_fiber, Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_mapβ_iso_hom, CategoryTheory.Pseudofunctor.StrongTrans.rightUnitor_hom_as_app, CategoryTheory.Pseudofunctor.mapβ_whisker_left_app_assoc, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_Ξ±, lanUnit_desc, CategoryTheory.StrictPseudofunctor.comp_mapComp_inv, whiskerLeft_id, pentagon_hom_inv_inv_inv_inv_assoc, CategoryTheory.Lax.StrongTrans.vComp_naturality_inv, Mathlib.Tactic.Bicategory.eval_of, CategoryTheory.LaxFunctor.mapComp_assoc_right_assoc, CategoryTheory.Pseudofunctor.mapComp'_naturality_2, CategoryTheory.Oplax.StrongTrans.vcomp_naturality_hom, CategoryTheory.Pseudofunctor.CoGrothendieck.ΞΉ_obj_base, CategoryTheory.Lax.StrongTrans.id_naturality_inv, CategoryTheory.Pseudofunctor.mapComp_id_right_inv_app, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'βββ_inv_app_assoc, CategoryTheory.Oplax.OplaxTrans.naturality_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp_id_left_hom_app, InducedBicategory.forget_obj, Adj.Bicategory.associator_inv_Οl, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_app_assoc, CategoryTheory.StrictPseudofunctor.id_map, CategoryTheory.Pseudofunctor.toDescentData_map_hom, CategoryTheory.Pseudofunctor.mapβ_associator, conjugateEquiv_associator_hom, Prod.swap_obj, CategoryTheory.PrelaxFunctor.mapβ_hom_inv_isIso, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_assoc, Pith.inclusion_mapId, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerRight_naturality_assoc, CategoryTheory.Pseudofunctor.ObjectProperty.IsClosedUnderIsomorphisms.isClosedUnderIsomorphisms, CategoryTheory.StrictPseudofunctor.id_mapId_hom, Bicategory.Opposite.op2_leftUnitor_inv, InducedBicategory.Hom.category_comp_hom, Prod.fst_map, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_app_assoc, Adj.Homβ.conjugateEquiv_Οl, Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_mapβ_iso_inv, Pseudofunctor.ofOplaxFunctorToLocallyGroupoid_mapCompIso_inv, eqToHom_whiskerRight, Adj.associator_inv_Οl, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq_assoc, CategoryTheory.Oplax.OplaxTrans.rightUnitor_inv_as_app, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_assoc, CategoryTheory.LaxFunctor.mapβ_rightUnitor_app_assoc, CategoryTheory.OplaxFunctor.mapComp'_comp_whiskerLeft_mapComp', Pith.compβ_iso_hom, lanLiftUnit_desc, leftUnitor_naturality_assoc, conjugateEquiv_id, CategoryTheory.Lax.StrongTrans.id_naturality_hom, CategoryTheory.StrictlyUnitaryLaxFunctor.mk'_map, whisker_assoc, CategoryTheory.Lax.OplaxTrans.naturality_id, Adj.comp_Οr, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_mapβ_toNatTrans_app, CategoryTheory.OplaxFunctor.PseudoCore.mapIdIso_hom, conjugateEquiv_symm_iso, InducedBicategory.isoMk_inv_hom, Prod.sectR_mapComp_hom, CategoryTheory.StrictPseudofunctor.mapComp_eq_eqToIso, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_map, CategoryTheory.PrelaxFunctor.mapβ_comp_assoc, CategoryTheory.LaxFunctor.mapComp_naturality_right, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_as_app, CategoryTheory.StrictPseudofunctorPreCore.mapβ_whisker_left, associatorNatIsoRight_hom_app, Adj.lIso_inv, instIsIsoHomRightZigzagHom, CategoryTheory.WithTerminal.pseudofunctor_mapId, associator_inv_congr, inv_whiskerLeft, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_id_app, CategoryTheory.Pseudofunctor.IsStackFor.essSurj, CategoryTheory.Pseudofunctor.id_mapComp, CategoryTheory.StrictPseudofunctor.mk'_mapβ, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_Ξ±, CategoryTheory.Functor.toPseudoFunctor'_mapId, CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, CategoryTheory.Iso.op2_inv_unop2, CategoryTheory.PrelaxFunctor.mapβ_isIso, mateEquiv_leftUnitor_hom_rightUnitor_inv, LeftExtension.whisker_unit, conjugateEquiv_mateEquiv_vcomp, CategoryTheory.LaxFunctor.mapβ_rightUnitor_app, CategoryTheory.Pseudofunctor.mapComp'_id_comp, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_assoc, CategoryTheory.StrictPseudofunctor.comp_mapβ, prod_homCategory_id_snd, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app, Adj.Bicategory.associator_hom_Οr, InducedBicategory.forget_mapβ, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_app_assoc, Bicategory.Opposite.bicategory_homCategory_id_unop2, associatorNatIsoLeft_hom_app, LeftLift.whiskerIdCancel_right, CategoryTheory.PrelaxFunctor.comp_toPrelaxFunctorStruct, CategoryTheory.PrelaxFunctor.mapβ_inv_hom_assoc, CategoryTheory.Oplax.StrongTrans.isoMk_inv_as_app, Prod.fst_mapComp_inv, CategoryTheory.Oplax.StrongTrans.Modification.naturality, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom, CategoryTheory.StrictlyUnitaryPseudofunctorCore.mapβ_comp, CategoryTheory.WithTerminal.pseudofunctor_mapComp, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_Ξ±, CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj, Adj.associator_hom_Οr, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom, Bicategory.Opposite.unop2_id, LeftExtension.whiskerOfCompIdIsoSelf_hom_right, prod_leftUnitor_hom_fst, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'βββ_inv_app_assoc, whiskerLeft_rightUnitor_inv_assoc, CategoryTheory.Oplax.OplaxTrans.naturality_comp_assoc, Adjunction.comp_left_triangle_aux, whiskerLeft_hom_inv_whiskerRight, CategoryTheory.Functor.toPseudoFunctor'_mapComp, CategoryTheory.Pseudofunctor.DescentData.exists_equivalence_of_sieve_eq, LeftLift.IsKan.uniqueUpToIso_hom_right, CategoryTheory.StrictlyUnitaryPseudofunctor.map_id, Bicategory.Opposite.bicategory_homCategory_comp_unop2, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id_app, CategoryTheory.LocallyDiscrete.mkPseudofunctor_obj, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_comp_mapComp'βββ_hom, CategoryTheory.Pseudofunctor.mapComp_id_right_hom_app_assoc, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom, CategoryTheory.Lax.LaxTrans.vComp_naturality_comp, CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_inv_app_hom, id_whiskerLeft, Pith.associator_inv_iso_hom, whiskerLeft_hom_inv_whiskerRight_assoc, CategoryTheory.Pseudofunctor.mapComp_id_left_hom, prod_associator_inv_snd, CategoryTheory.OplaxFunctor.id_mapId, CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom_assoc, CategoryTheory.Oplax.LaxTrans.naturality_id_assoc, CategoryTheory.Pseudofunctor.mapβ_whisker_left_app, CategoryTheory.StrictlyUnitaryLaxFunctorCore.mapβ_rightUnitor, CategoryTheory.Pseudofunctor.DescentData.isEquivalence_toDescentData_iff_of_sieve_eq, CategoryTheory.Pseudofunctor.CoGrothendieck.comp_const, CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, CategoryTheory.StrictlyUnitaryLaxFunctor.ext_iff, Prod.snd_mapComp_hom, leftUnitor_hom_congr, CategoryTheory.Oplax.StrongTrans.Modification.whiskerLeft_naturality_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.id_mapId_hom, Adj.leftUnitor_inv_Οr, whiskerRight_isIso, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_app, CategoryTheory.PrelaxFunctor.mapβ_id, rightUnitor_inv_naturality_assoc, CategoryTheory.Pseudofunctor.CoGrothendieck.compIso_inv_app, CategoryTheory.Oplax.OplaxTrans.isoMk_inv_as_app, CategoryTheory.StrictlyUnitaryLaxFunctor.comp_map, CategoryTheory.StrictPseudofunctor.mk''_mapComp, CategoryTheory.OplaxFunctor.mapβ_leftUnitor_app_assoc, CategoryTheory.Functor.toOplaxFunctor_mapId, CategoryTheory.BicategoricalCoherence.assoc_iso, Comonad.comul_assoc_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_hom_app_hom, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_assoc, Pith.leftUnitor_hom_iso, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app, instHasInitialLeftLiftOfHasLeftKanLift, Mathlib.Tactic.BicategoryCoherence.assoc_liftHomβ, lanUnit_desc_assoc, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_assoc, CategoryTheory.Oplax.LaxTrans.vComp_naturality_naturality, associator_naturality_left, whiskerLeft_whiskerLeft_inv_hom_assoc, Pith.rightUnitor_inv_iso_hom, Pith.compβ_iso_inv_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.mk'_mapβ, prod_homCategory_comp_snd, CategoryTheory.Oplax.StrongTrans.id_naturality_hom, leftUnitor_naturality, InducedBicategory.bicategory_homCategory_id_hom, CategoryTheory.StrictlyUnitaryLaxFunctor.mk'_mapId, Adj.Bicategory.associator_inv_Οr, CategoryTheory.LaxFunctor.mapComp_assoc_left, Comonad.counit_comul, Pith.pseudofunctorToPith_mapId_inv_iso_hom, CategoryTheory.OplaxFunctor.mapβ_rightUnitor_app, CategoryTheory.StrictlyUnitaryPseudofunctorCore.mapβ_right_unitor, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_app, CategoryTheory.LaxFunctor.mapComp_naturality_right_app, CategoryTheory.LaxFunctor.mapComp_assoc_right, LanLift.CommuteWith.lanLiftCompIsoWhisker_inv_right, mateEquiv_apply, Adj.associator_hom_Οl, LeftExtension.whiskerHom_right, CategoryTheory.StrictlyUnitaryLaxFunctor.comp_mapComp, InducedBicategory.bicategory_associator_hom_hom, CategoryTheory.Oplax.StrongTrans.naturality_naturality, pentagon_hom_hom_inv_inv_hom, CategoryTheory.PrelaxFunctor.mapβIso_hom, Pseudofunctor.ofOplaxFunctorToLocallyGroupoid_mapIdIso_hom, CategoryTheory.Oplax.OplaxTrans.leftUnitor_hom_as_app, CategoryTheory.PrelaxFunctor.mapβIso_inv, CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom, CategoryTheory.Pseudofunctor.mapComp_id_right_hom_app, Pith.inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_assoc, Bicategory.Opposite.bicategory_associator_inv_unop2, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_assoc, CategoryTheory.Lax.OplaxTrans.naturality_comp_assoc, CategoryTheory.Pseudofunctor.DescentData.id_hom, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_comp_mapComp'βββ_hom_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id, CategoryTheory.LaxFunctor.mapComp_naturality_left_app, pentagon_inv_inv_hom_hom_inv_assoc, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp, CategoryTheory.OplaxFunctor.mapComp_id_left_assoc, CategoryTheory.StrictPseudofunctor.mk'_mapId, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality, Pseudofunctor.ofLaxFunctorToLocallyGroupoid_mapCompIso_hom, CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_hom_app_hom, Prod.swap_mapComp_hom, CategoryTheory.Pseudofunctor.StrongTrans.Modification.vcomp_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_app, CategoryTheory.Pseudofunctor.DescentData.isoMk_hom_hom, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_assoc, LeftLift.ofIdComp_left_as, CategoryTheory.StrictPseudofunctor.id_mapId_inv, LeftExtension.whiskerOfCompIdIsoSelf_inv_right, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq, CategoryTheory.StrictlyUnitaryLaxFunctor.mapIdIso_inv, Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_as, CategoryTheory.FreeBicategory.mk_associator_inv, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_comp_assoc, rightUnitor_comp_assoc, Mathlib.Tactic.Bicategory.evalComp_nil_cons, Adj.leftUnitor_hom_Οr, CategoryTheory.Pseudofunctor.mapId'_hom_naturality, CategoryTheory.Pseudofunctor.DescentData.hom_self, Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of, CategoryTheory.Pseudofunctor.DescentData.comp_hom_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_app, LeftExtension.IsKan.fac, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_mapId, CategoryTheory.Oplax.StrongTrans.categoryStruct_id_naturality, CategoryTheory.Pseudofunctor.ObjectProperty.map_obj_obj, LeftLift.IsKan.uniqueUpToIso_inv_right, CategoryTheory.FreeBicategory.lift_mapComp, Comonad.comul_counit, leftZigzagIso_inv, CategoryTheory.Functor.toOplaxFunctor'_mapComp, Adjunction.comp_right_triangle_aux, CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_comp_fiber, Adj.lIso_hom, Prod.sectL_mapβ, CategoryTheory.Oplax.StrongTrans.toOplax_naturality, CategoryTheory.Pseudofunctor.mapId'_hom_naturality_assoc, CategoryTheory.OplaxFunctor.mapComp_naturality_right_app_assoc, Adjunction.homEquivβ_symm_apply, CategoryTheory.Oplax.StrongTrans.Modification.whiskerRight_naturality_assoc, toNatTrans_conjugateEquiv, CategoryTheory.Lax.StrongTrans.categoryStruct_comp_naturality, CategoryTheory.FreeBicategory.lift_toPrelaxFunctor_toPrelaxFunctorStruct_mapβ, CategoryTheory.Pseudofunctor.comp_mapComp, Prod.swap_mapComp_inv, CategoryTheory.PrelaxFunctor.mapβIso_eqToIso, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp, Bicategory.Opposite.opFunctor_map, CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_mapComp, CategoryTheory.Pseudofunctor.toOplax_mapId', LeftLift.whiskering_obj, Prod.snd_mapComp_inv, Adj.Bicategory.associator_hom_Οl, CategoryTheory.StrictPseudofunctor.mk''_obj, Pith.compβ_iso_inv, CategoryTheory.Pseudofunctor.mapβ_whisker_right_app, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerLeft_naturality, conjugateEquiv_symm_apply', AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_r, CategoryTheory.Pseudofunctor.CoGrothendieck.instFaithfulΞ±CategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_iso, InducedBicategory.isoMk_hom_hom, Pith.inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj, whiskerLeft_rightUnitor, CategoryTheory.WithInitial.pseudofunctor_mapComp, CategoryTheory.FreeBicategory.preinclusion_obj, CategoryTheory.Pseudofunctor.mapβ_left_unitor_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_assoc, CategoryTheory.Pseudofunctor.mapβ_right_unitor_app_assoc, pentagon_hom_inv_inv_inv_inv, CategoryTheory.Pseudofunctor.mapβ_right_unitor_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_naturality_app, CategoryTheory.FreeBicategory.lift_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map, CategoryTheory.LaxFunctor.comp_mapComp, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, CategoryTheory.PrelaxFunctor.mapβ_hom_inv_isIso_assoc, Pith.inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_mapβ, CategoryTheory.PrelaxFunctor.mapβ_inv_hom, conjugateEquiv_iso, Prod.sectR_mapId_hom, CategoryTheory.OplaxFunctor.mapComp_naturality_right, Strict.leftUnitor_eqToIso, CategoryTheory.OplaxFunctor.mapComp_naturality_left_app_assoc, CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_symm_apply, Prod.swap_mapId_hom, conjugateEquiv_whiskerLeft, CategoryTheory.StrictlyUnitaryLaxFunctor.id_mapId, CategoryTheory.LaxFunctor.mapβ_associator_app, CategoryTheory.FreeBicategory.mk_right_unitor_hom, LeftExtension.whiskering_obj, CategoryTheory.Pseudofunctor.toLax_mapComp', CategoryTheory.OplaxFunctor.mapComp'_comp_mapComp'_whiskerRight_assoc, CategoryTheory.StrictPseudofunctor.comp_obj, Bicategory.Opposite.homCategory_id_unop2, CategoryTheory.StrictPseudofunctor.id_mapComp_inv, InducedBicategory.mkHom_eqToHom, comp_whiskerLeft_symm_assoc, CommRingCat.moduleCatRestrictScalarsPseudofunctor_obj, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_app_assoc, Bicategory.Opposite.op2_id_unbop, leftUnitor_comp, CategoryTheory.BicategoricalCoherence.assoc'_iso, LeftExtension.w, CategoryTheory.Lax.OplaxTrans.vComp_naturality_id, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_comp_whiskerLeft_mapComp'_hom_app, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id, CategoryTheory.Cat.associator_hom_toNatTrans, Mathlib.Tactic.Bicategory.evalComp_nil_nil, CategoryTheory.Pseudofunctor.isoMapOfCommSq_eq, CategoryTheory.LaxFunctor.mapComp_naturality_left, CategoryTheory.LaxFunctor.mapComp_assoc_left_assoc, LeftLift.whiskerOfIdCompIsoSelf_inv_right, associatorNatIsoMiddle_inv_app, CategoryTheory.Pseudofunctor.mapβ_whisker_right_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_app_assoc, InducedBicategory.forget_mapId_hom, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_assoc, Pith.pseudofunctorToPith_mapComp_inv_iso_hom, prod_rightUnitor_hom_snd, precomp_map, pentagon_hom_hom_inv_hom_hom, conjugateEquiv_symm_apply, prod_associator_hom_snd, Adjunction.right_triangle, triangle_assoc_comp_left_inv, CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerRight_naturality, CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_inv_app, CategoryTheory.Oplax.OplaxTrans.Modification.naturality, CategoryTheory.BicategoricalCoherence.right_iso, Equivalence.right_triangle_hom, Prod.fst_obj, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_inv, CategoryTheory.LaxFunctor.mapComp_assoc_right_app_assoc, associatorNatIsoRight_inv_app, leftUnitor_comp_inv_assoc, leftUnitor_whiskerRight_assoc, leftUnitor_inv_congr, conjugateIsoEquiv_symm_apply_inv, Adj.forgetβ_mapComp, rightUnitor_hom_congr, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_mapComp_inv, CategoryTheory.Pseudofunctor.comp_mapId, Prod.swap_mapId_inv, CategoryTheory.OplaxFunctor.mapComp_naturality_right_app, Prod.sectR_map, CategoryTheory.StrictPseudofunctor.mk''_mapβ, CategoryTheory.OplaxFunctor.mapComp'_comp_whiskerLeft_mapComp'_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_mapId_inv, Bicategory.Opposite.op2_associator_hom, pentagon_hom_inv_inv_inv_hom, Adj.Bicategory.leftUnitor_inv_Οr, CategoryTheory.LaxFunctor.mapComp_assoc_left_app_assoc, CategoryTheory.Lax.OplaxTrans.id_app, CategoryTheory.Oplax.StrongTrans.homCategory_comp_as_app, rightZigzagIso_hom, CategoryTheory.LaxFunctor.id_mapComp, CategoryTheory.Cat.leftUnitor_inv_app, CategoryTheory.Functor.toPseudoFunctor_obj, associator_inv_naturality_middle_assoc, CategoryTheory.LaxFunctor.mapβ_leftUnitor_app, CategoryTheory.BicategoricalCoherence.refl_iso, rightUnitor_comp_inv_assoc, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, CategoryTheory.Lax.OplaxTrans.naturality_naturality_assoc, InducedBicategory.bicategory_leftUnitor_hom_hom, CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_comp_fiber, CategoryTheory.StrictlyUnitaryLaxFunctor.comp_mapβ, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_app, Bicategory.Opposite.bicategory_rightUnitor_hom_unop2, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'βββ_inv, CategoryTheory.Pseudofunctor.CoGrothendieck.compIso_hom_app, CategoryTheory.Pseudofunctor.DescentData.hom_comp, Strict.associator_eqToIso, CategoryTheory.Pseudofunctor.IsPrestackFor.nonempty_fullyFaithful, CategoryTheory.Pseudofunctor.mapComp'_hom_comp_mapComp'_hom_whiskerRight, RightLift.w, CategoryTheory.Pseudofunctor.ObjectProperty.mapβ_app_hom, triangle_assoc, leftUnitorNatIso_inv_app, CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.ext_iff, CategoryTheory.OplaxFunctor.mapβ_rightUnitor_app_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_comp_mapComp'_hom_whiskerRight, CategoryTheory.Oplax.StrongTrans.vcomp_naturality_inv, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv, CategoryTheory.Oplax.OplaxTrans.whiskerRight_as_app, associator_naturality_middle_assoc, Bicategory.Opposite.bicategory_rightUnitor_inv_unop2, CategoryTheory.Pseudofunctor.whiskerRightIso_mapId, CategoryTheory.Pseudofunctor.Grothendieck.map_map_base, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_associator_inv_as_app, CategoryTheory.Pseudofunctor.toOplax_mapComp', CategoryTheory.Oplax.OplaxTrans.leftUnitor_inv_as_app, CategoryTheory.FreeBicategory.lift_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj, CategoryTheory.Functor.toOplaxFunctor'_mapId, CategoryTheory.LaxFunctor.mapβ_leftUnitor_hom, RightExtension.w, Prod.fst_mapId_inv, CategoryTheory.LaxFunctor.mapβ_rightUnitor_hom, Adj.leftUnitor_hom_Οl, LanLift.CommuteWith.lanLiftCompIso_inv, CategoryTheory.Oplax.OplaxTrans.Modification.id_app, CategoryTheory.StrictlyUnitaryLaxFunctor.comp_obj, Pith.pseudofunctorToPith_mapComp_hom_iso, mateEquiv_apply', Equivalence.left_triangle_hom, conjugateEquiv_comp, CategoryTheory.OplaxFunctor.mapComp_id_left, CategoryTheory.LaxFunctor.mapβ_leftUnitor_app_assoc, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor, postcomp_map, CategoryTheory.LaxFunctor.mapβ_rightUnitor, LanLift.CommuteWith.lanLiftCompIsoWhisker_hom_right, triangle_assoc_comp_right_assoc, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_app_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_mapβ, rightUnitorNatIso_hom_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_app, pentagon_inv_hom_hom_hom_inv_assoc, CategoryTheory.LaxFunctor.PseudoCore.mapIdIso_inv, leftUnitor_comp_assoc, LeftLift.w, CategoryTheory.Pseudofunctor.mapId'_inv_naturality, CategoryTheory.LaxFunctor.mapComp_naturality_left_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_comp_mapComp'_hom_whiskerRight_app_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_app, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_app, CategoryTheory.Pseudofunctor.DescentData.Hom.comm, CategoryTheory.StrictlyUnitaryLaxFunctorCore.mapβ_comp, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map, triangle_assoc_comp_left_inv_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_map, CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerRight_naturality_assoc
|
leftUnitor π | CompOp | 200 mathmath: eqToHomTransIso_refl_left, leftUnitor_inv_naturality_assoc, CategoryTheory.StrictlyUnitaryLaxFunctorCore.mapβ_leftUnitor, Prod.sectL_mapId_inv, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom, mateEquiv_comp_id_right, CategoryTheory.LaxFunctor.mapβ_leftUnitor_assoc, CategoryTheory.Pseudofunctor.mapβ_left_unitor_assoc, CategoryTheory.Oplax.LaxTrans.vComp_naturality_id, CategoryTheory.StrictPseudofunctorCore.mapβ_left_unitor, eqToHomTransIso_refl_refl, CategoryTheory.FreeBicategory.mk_left_unitor_inv, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_assoc, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id, CategoryTheory.BicategoricalCoherence.left'_iso, InducedBicategory.bicategory_leftUnitor_inv_hom, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id_assoc, CategoryTheory.Pseudofunctor.StrongTrans.leftUnitor_inv_as_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv, CategoryTheory.Oplax.OplaxTrans.categoryStruct_id_naturality, Adj.Bicategory.rightUnitor_inv_Οr, CategoryTheory.Pseudofunctor.mapComp_id_left_inv_app, Adjunction.homEquivβ_apply, CategoryTheory.Pseudofunctor.mapβ_left_unitor, unitors_inv_equal, Pith.leftUnitor_inv_iso_hom, triangle_assoc_comp_left, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom, conjugateEquiv_apply, CategoryTheory.Cat.leftUnitor_hom_app, CategoryTheory.OplaxFunctor.mapβ_leftUnitor_app, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_id, mateEquiv_id_comp_right, leftUnitor_comp_inv, CategoryTheory.Pseudofunctor.mapComp_id_left, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id, id_whiskerLeft_symm, CategoryTheory.LaxFunctor.mapβ_leftUnitor_hom_app, leftUnitor_inv_whiskerRight_assoc, Adj.rightUnitor_hom_Οr, CategoryTheory.BicategoricalCoherence.left_iso, Bicategory.Opposite.bicategory_leftUnitor_hom_unop2, CategoryTheory.OplaxFunctor.mapβ_leftUnitor_assoc, conjugateEquiv_id_comp_right_apply, CategoryTheory.Oplax.StrongTrans.naturality_id_assoc, CategoryTheory.Oplax.LaxTrans.naturality_id, CategoryTheory.StrictlyUnitaryPseudofunctorCore.mapβ_left_unitor, CategoryTheory.Pseudofunctor.isoMapOfCommSq_horiz_id, CategoryTheory.Oplax.StrongTrans.id_naturality_inv, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_leftUnitor_inv_as_app, Prod.sectL_mapComp_hom, leftUnitor_inv_naturality, unitors_equal, CategoryTheory.Oplax.LaxTrans.id_naturality, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_id, Adj.Bicategory.rightUnitor_hom_Οr, CategoryTheory.Pseudofunctor.mapComp_id_left_hom_app_assoc, conjugateEquiv_comp_id_right_apply, CategoryTheory.Lax.LaxTrans.id_naturality, leftUnitor_inv_whiskerRight, Equivalence.right_triangle, Equivalence.left_triangle, CategoryTheory.LaxFunctor.mapβ_leftUnitor_hom_app_assoc, Bicategory.Opposite.bicategory_leftUnitor_inv_unop2, CategoryTheory.FreeBicategory.mk_left_unitor_hom, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_id_assoc, Comonad.counit_comul_assoc, Bicategory.Opposite.op2_rightUnitor_inv, CategoryTheory.Pseudofunctor.mapComp_id_left_inv_app_assoc, Adj.Bicategory.leftUnitor_hom_Οl, CategoryTheory.Pseudofunctor.mapComp_id_left_inv_assoc, CategoryTheory.Lax.LaxTrans.naturality_id_assoc, adjointifyCounit_left_triangle, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id, CategoryTheory.Lax.LaxTrans.naturality_id, prod_leftUnitor_inv_fst, triangle_assoc_comp_right_inv_assoc, Adjunction.left_triangle, triangle_assoc_comp_right_inv, prod_leftUnitor_inv_snd, leftUnitorNatIso_hom_app, Adj.Bicategory.leftUnitor_inv_Οl, Prod.sectL_mapId_hom, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_id_naturality_hom, CategoryTheory.Pseudofunctor.isoMapOfCommSq_vert_id, leftUnitor_whiskerRight, CategoryTheory.Oplax.StrongTrans.naturality_id, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_assoc, prod_leftUnitor_hom_snd, CategoryTheory.Pseudofunctor.mapComp_id_left_hom_assoc, CategoryTheory.Lax.LaxTrans.vComp_naturality_id, CategoryTheory.Lax.OplaxTrans.id_naturality, Bicategory.Opposite.op2_rightUnitor, CategoryTheory.Oplax.OplaxTrans.naturality_id_assoc, CategoryTheory.OplaxFunctor.mapβ_leftUnitor, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id_assoc, Adj.leftUnitor_inv_Οl, Bicategory.Opposite.op2_rightUnitor_hom, Mathlib.Tactic.Bicategory.naturality_leftUnitor, CategoryTheory.Lax.StrongTrans.naturality_id, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_leftUnitor_hom_as_app, CategoryTheory.Lax.StrongTrans.categoryStruct_id_naturality, CategoryTheory.Pseudofunctor.mapComp_id_left_inv, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_iso, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_assoc, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_id_assoc, Bicategory.Opposite.op2_leftUnitor_hom, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv, CategoryTheory.Cat.leftUnitor_hom_toNatTrans, Prod.sectL_mapComp_inv, id_whiskerLeft_assoc, CategoryTheory.Cat.leftUnitor_inv_toNatTrans, CategoryTheory.Pseudofunctor.mapβ_left_unitor_app, triangle, CategoryTheory.Pseudofunctor.StrongTrans.leftUnitor_hom_as_app, CategoryTheory.LaxFunctor.mapβ_leftUnitor_hom_assoc, CategoryTheory.Lax.StrongTrans.naturality_id_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id_assoc, Adj.rightUnitor_inv_Οr, CategoryTheory.Oplax.OplaxTrans.naturality_id, triangle_assoc_comp_right, CategoryTheory.Cat.Hom.toNatIso_leftUnitor, CategoryTheory.Lax.OplaxTrans.naturality_id_assoc, conjugateEquiv_apply', CategoryTheory.LaxFunctor.mapβ_leftUnitor, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_id_naturality_inv, LeftLift.ofIdComp_hom, LeftLift.whiskerOfIdCompIsoSelf_hom_right, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_app_assoc, CategoryTheory.Lax.StrongTrans.id_naturality_inv, CategoryTheory.Pseudofunctor.mapComp_id_left_hom_app, Bicategory.Opposite.op2_leftUnitor_inv, leftUnitor_naturality_assoc, CategoryTheory.Lax.StrongTrans.id_naturality_hom, CategoryTheory.Lax.OplaxTrans.naturality_id, Bicategory.Opposite.op2_leftUnitor, mateEquiv_leftUnitor_hom_rightUnitor_inv, CategoryTheory.Pseudofunctor.mapComp'_id_comp, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_assoc, LeftLift.whiskerIdCancel_right, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom, prod_leftUnitor_hom_fst, Adjunction.comp_left_triangle_aux, id_whiskerLeft, CategoryTheory.Pseudofunctor.mapComp_id_left_hom, CategoryTheory.Oplax.LaxTrans.naturality_id_assoc, leftUnitor_hom_congr, Adj.leftUnitor_inv_Οr, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_app, CategoryTheory.OplaxFunctor.mapβ_leftUnitor_app_assoc, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_assoc, Pith.leftUnitor_hom_iso, CategoryTheory.Oplax.StrongTrans.id_naturality_hom, leftUnitor_naturality, Comonad.counit_comul, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_assoc, CategoryTheory.Oplax.OplaxTrans.leftUnitor_hom_as_app, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id, CategoryTheory.OplaxFunctor.mapComp_id_left_assoc, Adj.leftUnitor_hom_Οr, CategoryTheory.Oplax.StrongTrans.categoryStruct_id_naturality, Adjunction.comp_right_triangle_aux, Adjunction.homEquivβ_symm_apply, conjugateEquiv_symm_apply', CategoryTheory.leftUnitor_def, CategoryTheory.Pseudofunctor.mapβ_left_unitor_app_assoc, Strict.leftUnitor_eqToIso, leftUnitor_comp, CategoryTheory.Lax.OplaxTrans.vComp_naturality_id, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id, LeftLift.whiskerOfIdCompIsoSelf_inv_right, conjugateEquiv_symm_apply, Adjunction.right_triangle, triangle_assoc_comp_left_inv, Equivalence.right_triangle_hom, leftUnitor_comp_inv_assoc, leftUnitor_whiskerRight_assoc, leftUnitor_inv_congr, CategoryTheory.Cat.leftUnitor_inv_app, CategoryTheory.LaxFunctor.mapβ_leftUnitor_app, InducedBicategory.bicategory_leftUnitor_hom_hom, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_app, Bicategory.Opposite.bicategory_rightUnitor_hom_unop2, triangle_assoc, leftUnitorNatIso_inv_app, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv, Bicategory.Opposite.bicategory_rightUnitor_inv_unop2, CategoryTheory.Pseudofunctor.whiskerRightIso_mapId, CategoryTheory.Oplax.OplaxTrans.leftUnitor_inv_as_app, CategoryTheory.LaxFunctor.mapβ_leftUnitor_hom, Adj.leftUnitor_hom_Οl, Equivalence.left_triangle_hom, CategoryTheory.OplaxFunctor.mapComp_id_left, CategoryTheory.LaxFunctor.mapβ_leftUnitor_app_assoc, triangle_assoc_comp_right_assoc, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_app_assoc, leftUnitor_comp_assoc, triangle_assoc_comp_left_inv_assoc
|
leftUnitorNatIso π | CompOp | 2 mathmath: leftUnitorNatIso_hom_app, leftUnitorNatIso_inv_app
|
postcomp π | CompOp | 23 mathmath: LeftLift.whiskering_map, RightLift.w_assoc, LeftLift.w_assoc, postcomp_obj, postcomposing_obj, HasLeftKanLift.hasInitial, LeftLift.whiskerHom_right, LeftLift.ofIdComp_right, postcomposing_map_app, LeftLift.ofIdComp_hom, LeftLift.whiskerOfIdCompIsoSelf_hom_right, LeftLift.whiskerIdCancel_right, LeftLift.IsKan.uniqueUpToIso_hom_right, instHasInitialLeftLiftOfHasLeftKanLift, LanLift.CommuteWith.lanLiftCompIsoWhisker_inv_right, LeftLift.ofIdComp_left_as, LeftLift.IsKan.uniqueUpToIso_inv_right, LeftLift.whiskering_obj, LeftLift.whiskerOfIdCompIsoSelf_inv_right, RightLift.w, postcomp_map, LanLift.CommuteWith.lanLiftCompIsoWhisker_hom_right, LeftLift.w
|
postcomposing π | CompOp | 8 mathmath: associatorNatIsoLeft_inv_app, postcomposing_obj, postcomposing_map_app, rightUnitorNatIso_inv_app, associatorNatIsoMiddle_hom_app, associatorNatIsoLeft_hom_app, associatorNatIsoMiddle_inv_app, rightUnitorNatIso_hom_app
|
precomp π | CompOp | 23 mathmath: RightExtension.w_assoc, LeftExtension.w_assoc, LeftExtension.ofCompId_right, LeftExtension.ofCompId_left_as, LeftExtension.whiskering_map, precomposing_map_app, Lan.CommuteWith.lanCompIsoWhisker_hom_right, precomp_obj, LeftExtension.whiskerIdCancel_right, LeftExtension.IsKan.uniqueUpToIso_hom_right, Lan.CommuteWith.lanCompIsoWhisker_inv_right, LeftExtension.ofCompId_hom, instHasInitialLeftExtensionOfHasLeftKanExtension, LeftExtension.IsKan.uniqueUpToIso_inv_right, precomposing_obj, HasLeftKanExtension.hasInitial, LeftExtension.whiskerOfCompIdIsoSelf_hom_right, LeftExtension.whiskerHom_right, LeftExtension.whiskerOfCompIdIsoSelf_inv_right, LeftExtension.whiskering_obj, LeftExtension.w, precomp_map, RightExtension.w
|
precomposing π | CompOp | 8 mathmath: precomposing_map_app, leftUnitorNatIso_hom_app, associatorNatIsoMiddle_hom_app, precomposing_obj, associatorNatIsoRight_hom_app, associatorNatIsoMiddle_inv_app, associatorNatIsoRight_inv_app, leftUnitorNatIso_inv_app
|
rightUnitor π | CompOp | 207 mathmath: CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_assoc, Adj.rightUnitor_hom_Οl, mateEquiv_comp_id_right, Adjunction.homEquivβ_symm_apply, CategoryTheory.Oplax.LaxTrans.vComp_naturality_id, conjugateEquiv_adjunction_id_symm, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_assoc, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv, CategoryTheory.Oplax.OplaxTrans.categoryStruct_id_naturality, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_app_assoc, rightUnitor_inv_naturality, Mathlib.Tactic.Bicategory.naturality_rightUnitor, rightUnitor_inv_congr, unitors_inv_equal, triangle_assoc_comp_left, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom, CategoryTheory.FreeBicategory.mk_right_unitor_inv, conjugateEquiv_apply, Adj.Bicategory.rightUnitor_inv_Οl, whiskerRight_id, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_id, mateEquiv_id_comp_right, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id, CategoryTheory.BicategoricalCoherence.tensorRight_iso, Prod.sectR_mapComp_inv, Adj.rightUnitor_inv_Οl, CategoryTheory.Pseudofunctor.mapComp_id_right_inv_app_assoc, CategoryTheory.Cat.rightUnitor_hom_toNatTrans, Adj.rightUnitor_hom_Οr, CategoryTheory.Pseudofunctor.mapComp_id_right, Bicategory.Opposite.bicategory_leftUnitor_hom_unop2, CategoryTheory.Pseudofunctor.mapComp'_comp_id, conjugateEquiv_id_comp_right_apply, Adjunction.homEquivβ_apply, CategoryTheory.Oplax.StrongTrans.naturality_id_assoc, CategoryTheory.Oplax.LaxTrans.naturality_id, CategoryTheory.Pseudofunctor.isoMapOfCommSq_horiz_id, CategoryTheory.Oplax.StrongTrans.id_naturality_inv, CategoryTheory.Pseudofunctor.mapβ_right_unitor_assoc, Prod.sectL_mapComp_hom, unitors_equal, CategoryTheory.Cat.rightUnitor_hom_app, CategoryTheory.Oplax.LaxTrans.id_naturality, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_id, CategoryTheory.Pseudofunctor.mapComp_id_right_hom, conjugateEquiv_comp_id_right_apply, CategoryTheory.Lax.LaxTrans.id_naturality, whiskerLeft_rightUnitor_assoc, Equivalence.right_triangle, Equivalence.left_triangle, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_app, Bicategory.Opposite.bicategory_leftUnitor_inv_unop2, Prod.sectR_mapId_inv, CategoryTheory.Pseudofunctor.whiskerLeftIso_mapId, Pith.rightUnitor_hom_iso, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_id_assoc, Bicategory.Opposite.op2_rightUnitor_inv, CategoryTheory.LaxFunctor.mapβ_rightUnitor_hom_app, CategoryTheory.BicategoricalCoherence.right'_iso, prod_rightUnitor_inv_fst, eqToHomTransIso_refl_right, CategoryTheory.Lax.LaxTrans.naturality_id_assoc, CategoryTheory.Oplax.OplaxTrans.rightUnitor_hom_as_app, adjointifyCounit_left_triangle, CategoryTheory.rightUnitor_def, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id, whiskerLeft_rightUnitor_inv, CategoryTheory.BicategoricalCoherence.tensorRight'_iso, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv, Pith.rightUnitor_inv_iso_inv, LeftExtension.whiskerIdCancel_right, prod_rightUnitor_inv_snd, CategoryTheory.Pseudofunctor.mapComp_id_right_hom_assoc, CategoryTheory.Lax.LaxTrans.naturality_id, CategoryTheory.StrictPseudofunctorCore.mapβ_right_unitor, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_rightUnitor_inv_as_app, triangle_assoc_comp_right_inv_assoc, CategoryTheory.LaxFunctor.mapβ_rightUnitor_hom_app_assoc, prod_rightUnitor_hom_fst, Adjunction.left_triangle, triangle_assoc_comp_right_inv, Adj.Bicategory.rightUnitor_hom_Οl, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_id_naturality_hom, InducedBicategory.bicategory_rightUnitor_hom_hom, CategoryTheory.Pseudofunctor.isoMapOfCommSq_vert_id, Strict.rightUnitor_eqToIso, CategoryTheory.Oplax.StrongTrans.naturality_id, CategoryTheory.Pseudofunctor.mapComp_id_right_inv_assoc, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_rightUnitor_hom_as_app, InducedBicategory.bicategory_rightUnitor_inv_hom, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv, rightUnitor_naturality_assoc, CategoryTheory.OplaxFunctor.mapβ_rightUnitor_assoc, CategoryTheory.Lax.LaxTrans.vComp_naturality_id, CategoryTheory.Lax.OplaxTrans.id_naturality, Bicategory.Opposite.op2_rightUnitor, CategoryTheory.Oplax.OplaxTrans.naturality_id_assoc, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id_assoc, Bicategory.Opposite.op2_rightUnitor_hom, Mathlib.Tactic.Bicategory.naturality_leftUnitor, CategoryTheory.LaxFunctor.mapβ_rightUnitor_hom_assoc, CategoryTheory.Lax.StrongTrans.naturality_id, LeftExtension.ofCompId_hom, CategoryTheory.Lax.StrongTrans.categoryStruct_id_naturality, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_iso, CategoryTheory.OplaxFunctor.mapComp_id_right_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_assoc, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_id_assoc, rightUnitorNatIso_inv_app, Bicategory.Opposite.op2_leftUnitor_hom, Comonad.comul_counit_assoc, Prod.sectL_mapComp_inv, CategoryTheory.OplaxFunctor.mapβ_rightUnitor, triangle, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_app, CategoryTheory.Lax.StrongTrans.naturality_id_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id_assoc, Adj.rightUnitor_inv_Οr, CategoryTheory.Oplax.OplaxTrans.naturality_id, rightUnitor_comp, whiskerRight_id_symm, CategoryTheory.OplaxFunctor.mapComp_id_right, triangle_assoc_comp_right, CategoryTheory.Pseudofunctor.mapComp_id_right_inv, rightUnitor_naturality, CategoryTheory.LaxFunctor.mapβ_rightUnitor_assoc, CategoryTheory.Lax.OplaxTrans.naturality_id_assoc, whiskerRight_id_assoc, CategoryTheory.Cat.Hom.toNatIso_rightUnitor, conjugateEquiv_apply', Adj.Bicategory.leftUnitor_hom_Οr, CategoryTheory.Pseudofunctor.StrongTrans.rightUnitor_inv_as_app, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_id_naturality_inv, conjugateEquiv_adjunction_id, CategoryTheory.Cat.rightUnitor_inv_app, CategoryTheory.Cat.rightUnitor_inv_toNatTrans, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_assoc, CategoryTheory.Pseudofunctor.mapβ_right_unitor, rightUnitor_comp_inv, CategoryTheory.Pseudofunctor.StrongTrans.rightUnitor_hom_as_app, CategoryTheory.Lax.StrongTrans.id_naturality_inv, CategoryTheory.Pseudofunctor.mapComp_id_right_inv_app, Bicategory.Opposite.op2_leftUnitor_inv, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_app_assoc, CategoryTheory.Oplax.OplaxTrans.rightUnitor_inv_as_app, CategoryTheory.LaxFunctor.mapβ_rightUnitor_app_assoc, CategoryTheory.Lax.StrongTrans.id_naturality_hom, CategoryTheory.Lax.OplaxTrans.naturality_id, Prod.sectR_mapComp_hom, Bicategory.Opposite.op2_leftUnitor, mateEquiv_leftUnitor_hom_rightUnitor_inv, CategoryTheory.LaxFunctor.mapβ_rightUnitor_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_assoc, LeftExtension.whiskerOfCompIdIsoSelf_hom_right, whiskerLeft_rightUnitor_inv_assoc, Adjunction.comp_left_triangle_aux, CategoryTheory.Pseudofunctor.mapComp_id_right_hom_app_assoc, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom, CategoryTheory.Oplax.LaxTrans.naturality_id_assoc, CategoryTheory.StrictlyUnitaryLaxFunctorCore.mapβ_rightUnitor, Adj.leftUnitor_inv_Οr, rightUnitor_inv_naturality_assoc, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_assoc, Pith.rightUnitor_inv_iso_hom, CategoryTheory.Oplax.StrongTrans.id_naturality_hom, CategoryTheory.OplaxFunctor.mapβ_rightUnitor_app, CategoryTheory.StrictlyUnitaryPseudofunctorCore.mapβ_right_unitor, CategoryTheory.Pseudofunctor.mapComp_id_right_hom_app, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id, LeftExtension.whiskerOfCompIdIsoSelf_inv_right, rightUnitor_comp_assoc, Adj.leftUnitor_hom_Οr, CategoryTheory.Oplax.StrongTrans.categoryStruct_id_naturality, Comonad.comul_counit, Adjunction.comp_right_triangle_aux, conjugateEquiv_symm_apply', whiskerLeft_rightUnitor, CategoryTheory.Pseudofunctor.mapβ_right_unitor_app_assoc, CategoryTheory.Pseudofunctor.mapβ_right_unitor_app, Prod.sectR_mapId_hom, CategoryTheory.FreeBicategory.mk_right_unitor_hom, CategoryTheory.Lax.OplaxTrans.vComp_naturality_id, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id, prod_rightUnitor_hom_snd, conjugateEquiv_symm_apply, Adjunction.right_triangle, triangle_assoc_comp_left_inv, CategoryTheory.BicategoricalCoherence.right_iso, Equivalence.right_triangle_hom, rightUnitor_hom_congr, Adj.Bicategory.leftUnitor_inv_Οr, rightUnitor_comp_inv_assoc, Bicategory.Opposite.bicategory_rightUnitor_hom_unop2, triangle_assoc, CategoryTheory.OplaxFunctor.mapβ_rightUnitor_app_assoc, Bicategory.Opposite.bicategory_rightUnitor_inv_unop2, CategoryTheory.LaxFunctor.mapβ_rightUnitor_hom, Equivalence.left_triangle_hom, CategoryTheory.LaxFunctor.mapβ_rightUnitor, triangle_assoc_comp_right_assoc, rightUnitorNatIso_hom_app, triangle_assoc_comp_left_inv_assoc
|
rightUnitorNatIso π | CompOp | 2 mathmath: rightUnitorNatIso_inv_app, rightUnitorNatIso_hom_app
|
termΞ±_ π | CompOp | β |
termΟ_ π | CompOp | β |
toCategoryStruct π | CompOp | 1285 mathmath: iterated_mateEquiv_conjugateEquiv, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id, CategoryTheory.Join.pseudofunctorLeft_mapId_inv_toNatTrans_app, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_assoc, CategoryTheory.Pseudofunctor.DescentData.isEquivalence_toDescentData_of_sieve_le, prod_whiskerLeft_snd, Bicategory.Opposite.op2_associator, CategoryTheory.StrictPseudofunctorPreCore.map_id, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_mapβ_toNatTrans_app, CategoryTheory.Pseudofunctor.DescentData.ofObj_hom, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom, RightExtension.w_assoc, CategoryTheory.Pseudofunctor.DescentData.subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv, CategoryTheory.Oplax.StrongTrans.Modification.vcomp_app, AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_adj, CategoryTheory.Pseudofunctor.mapβ_associator_assoc, CategoryTheory.LaxFunctor.mapβ_associator_assoc, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map, Adj.rightUnitor_hom_Οl, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_naturality_assoc, Comonad.comul_assoc_flip, Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil, CategoryTheory.Cat.whiskerRight_toNatTrans, CategoryTheory.OplaxFunctor.id_mapComp, InducedBicategory.bicategory_whiskerLeft_hom, Adj.comp_r, Bicategory.Opposite.op2_unop2, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_mapβ, CategoryTheory.Join.pseudofunctorRight_mapComp_inv_toNatTrans_app, eqToHomTransIso_refl_left, CategoryTheory.StrictlyUnitaryLaxFunctor.id_mapβ, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_app_assoc, Bicategory.Opposite.op2_associator_inv, CategoryTheory.Pseudofunctor.mapβ_associator_app_assoc, Pith.inclusion_mapComp, Pith.pseudofunctorToPith_mapId_hom_iso, leftAdjointSquare.comp_hvcomp, CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_inv_app_hom, CategoryTheory.Pseudofunctor.isEquivalence_toDescentData, conjugateEquiv_whiskerRight, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerRight_naturality, LeftLift.whiskering_map, leftUnitor_inv_naturality_assoc, rightAdjointSquare.comp_vhcomp, CategoryTheory.Cat.Hom.id_map, CategoryTheory.Lax.StrongTrans.vComp_naturality_hom, whiskerLeft_inv_hom, CategoryTheory.StrictlyUnitaryLaxFunctor.mapIdIso_hom, CategoryTheory.FreeBicategory.lift_mapId, CategoryTheory.StrictlyUnitaryLaxFunctorCore.mapβ_leftUnitor, Adj.associator_inv_Οr, Prod.sectL_mapId_inv, whiskerRight_comp_assoc, Prod.snd_map, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom, CategoryTheory.Cat.Hom.toNatIso_associator, InducedBicategory.bicategory_associator_inv_hom, LeftExtension.w_assoc, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality, CategoryTheory.OplaxFunctor.mapβ_associator, inv_hom_whiskerRight_whiskerRight_assoc, Adj.rIso_inv, mateEquiv_comp_id_right, CategoryTheory.Pseudofunctor.StrongTrans.homCategory_comp_as_app, inv_hom_whiskerRight_assoc, whisker_exchange, inv_hom_whiskerRight, CategoryTheory.LaxFunctor.mapβ_leftUnitor_assoc, CategoryTheory.Cat.associator_hom_app, CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_obj, pentagon_inv, Bicategory.Opposite.op2_whiskerLeft, isLeftAdjoint_TFAE, Adjunction.homEquivβ_symm_apply, InducedBicategory.Hom.category_id_hom, CategoryTheory.LaxFunctor.comp_mapId, CategoryTheory.Pseudofunctor.mapβ_left_unitor_assoc, Pith.comp_of, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id_app, CategoryTheory.OplaxFunctor.mapβ_associator_app, CategoryTheory.Oplax.LaxTrans.vComp_naturality_id, CategoryTheory.StrictPseudofunctorCore.mapβ_left_unitor, Lan.existsUnique, CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_id_fiber, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_whiskerRight_as_app, CategoryTheory.Oplax.OplaxTrans.Modification.vcomp_app, eqToHomTransIso_refl_refl, CategoryTheory.FreeBicategory.mk_left_unitor_inv, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality_assoc, RightLift.w_assoc, mateEquiv_vcomp, CategoryTheory.Pseudofunctor.StrongTrans.comp_app, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj, conjugateEquiv_adjunction_id_symm, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_assoc, Adj.comp_Οl_assoc, CategoryTheory.StrictPseudofunctor.mk'_obj, CategoryTheory.Oplax.OplaxTrans.StrongCore.naturality_hom, Adj.forgetβ_mapId, CategoryTheory.Adjunction.ofCat_counit, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id, CategoryTheory.Iso.unop2_op2, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp_assoc, CategoryTheory.Oplax.OplaxTrans.homCategory_id_as_app, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app, CategoryTheory.BicategoricalCoherence.left'_iso, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app, CategoryTheory.StrictlyUnitaryLaxFunctorCore.mapβ_associator, Pseudofunctor.ofLaxFunctorToLocallyGroupoid_mapCompIso_inv, LeftExtension.ofCompId_right, CategoryTheory.StrictlyUnitaryLaxFunctorCore.mapβ_id, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp_app, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_comp_naturality_hom, CategoryTheory.OplaxFunctor.mapComp_naturality_right_assoc, CategoryTheory.Oplax.LaxTrans.naturality_naturality_assoc, InducedBicategory.categoryStruct_comp_hom, CategoryTheory.StrictPseudofunctor.id_mapComp_hom, InducedBicategory.bicategory_leftUnitor_inv_hom, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_app_assoc, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctor_map_hom, CategoryTheory.Pseudofunctor.StrongTrans.leftUnitor_inv_as_app, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_whiskerLeft_as_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv, LanLift.CommuteWith.instHasLeftKanLiftComp, pentagon_hom_hom_inv_hom_hom_assoc, CategoryTheory.Functor.toPseudoFunctor'_obj, CategoryTheory.Oplax.OplaxTrans.categoryStruct_id_naturality, Adj.Bicategory.rightUnitor_inv_Οr, LeftLift.w_assoc, whiskerRightIso_hom, associatorNatIsoLeft_inv_app, CategoryTheory.StrictlyUnitaryPseudofunctor.mk'_map, CategoryTheory.Pseudofunctor.mapComp_id_left_inv_app, pentagon_inv_hom_hom_hom_hom, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_app_assoc, rightUnitor_inv_naturality, CategoryTheory.OplaxFunctor.mapComp_assoc_left_app_assoc, CategoryTheory.Pseudofunctor.CoGrothendieck.instIsEquivalenceΞ±CategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, Adjunction.homEquivβ_apply, CategoryTheory.StrictPseudofunctorCore.mapβ_associator, Prod.swap_mapβ, CategoryTheory.Pseudofunctor.DescentData.isoMk_inv_hom, Mathlib.Tactic.Bicategory.naturality_rightUnitor, Pith.whiskerRight_iso_inv, rightUnitor_inv_congr, CategoryTheory.Pseudofunctor.mapβ_left_unitor, CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_base, unitors_inv_equal, Adj.forgetβ_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map, Pith.leftUnitor_inv_iso_hom, leftZigzagIso_symm, CategoryTheory.StrictPseudofunctor.mk''_mapId, associator_inv_naturality_middle, associator_naturality_right_assoc, CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_fiber, CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerLeft_naturality_assoc, hom_inv_whiskerRight_whiskerRight_assoc, CategoryTheory.StrictlyUnitaryLaxFunctor.mapId_isIso, prod_id_fst, triangle_assoc_comp_left, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom, associator_inv_naturality_right, LanLift.CommuteWith.lanLiftCompIso_hom, Pseudofunctor.ofOplaxFunctorToLocallyGroupoid_mapCompIso_hom, CategoryTheory.StrictlyUnitaryPseudofunctor.id_mapComp_hom, whiskerLeft_iff, CategoryTheory.FreeBicategory.mk_right_unitor_inv, AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_l, whiskerLeft_comp, CategoryTheory.Pseudofunctor.ObjectProperty.ΞΉ_app_toFunctor, conjugateEquiv_symm_id, CategoryTheory.Oplax.StrongTrans.Modification.whiskerLeft_naturality, CategoryTheory.LaxFunctor.mapComp_naturality_left_app_assoc, conjugateEquiv_apply, prod_whiskerRight_fst, CategoryTheory.Pseudofunctor.DescentData.comp_hom, whiskerRight_comp_symm, Adj.Bicategory.rightUnitor_inv_Οl, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv, Pith.compβ_iso_hom_assoc, CategoryTheory.Cat.leftUnitor_hom_app, associator_eqToHom_hom_assoc, whiskerRight_id, CategoryTheory.OplaxFunctor.mapβ_leftUnitor_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality, CategoryTheory.Oplax.LaxTrans.naturality_comp_assoc, CategoryTheory.Oplax.OplaxTrans.categoryStruct_comp_app, CategoryTheory.LaxFunctor.id_mapId, CategoryTheory.StrictPseudofunctor.id_obj, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_id, CategoryTheory.Oplax.StrongTrans.homCategory_id_as_app, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_naturality, InducedBicategory.eqToHom_hom, CategoryTheory.Pseudofunctor.Grothendieck.ext_iff, lanLiftUnit_desc_assoc, whiskerLeft_hom_inv, CategoryTheory.Lax.LaxTrans.id_app, CategoryTheory.StrictlyUnitaryLaxFunctor.id_obj, mateEquiv_id_comp_right, leftUnitor_comp_inv, CategoryTheory.Pseudofunctor.mapComp_id_left, CategoryTheory.Iso.unop2_inv, postcomp_obj, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality_app, CategoryTheory.StrictlyUnitaryPseudofunctorCore.mapβ_whisker_right, CategoryTheory.StrictPseudofunctor.comp_mapComp_hom, leftZigzagIso_hom, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_mapComp, CategoryTheory.Functor.toOplaxFunctor'_obj, Bicategory.Opposite.bicategory_associator_hom_unop2, CategoryTheory.OplaxFunctor.PseudoCore.mapCompIso_hom, CategoryTheory.StrictPseudofunctor.comp_mapId_hom, Bicategory.Opposite.unop2_id_bop, CategoryTheory.LaxFunctor.mapComp_assoc_right_app, LeftExtension.ofCompId_left_as, CategoryTheory.Oplax.OplaxTrans.associator_hom_as_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id, CategoryTheory.Pseudofunctor.toOplax_mapComp, Bicategory.Opposite.unopFunctor_map, CategoryTheory.BicategoricalCoherence.tensorRight_iso, inv_hom_whiskerRight_whiskerRight, Prod.sectR_mapComp_inv, Prod.fst_mapComp_hom, whiskerLeft_whiskerLeft_hom_inv_assoc, id_whiskerLeft_symm, CategoryTheory.Pseudofunctor.isStackFor_ofArrows_iff, CategoryTheory.LaxFunctor.mapβ_leftUnitor_hom_app, Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_of, LeftLift.IsKan.fac_assoc, postcomposing_obj, pentagon_inv_hom_hom_hom_inv, Adj.rightUnitor_inv_Οl, Adj.Homβ.conjugateEquiv_symm_Οr, CategoryTheory.LaxFunctor.PseudoCore.mapCompIso_inv, CategoryTheory.Join.pseudofunctorLeft_mapId_hom_toNatTrans_app, CategoryTheory.Pseudofunctor.mapComp_id_right_inv_app_assoc, CategoryTheory.StrictlyUnitaryLaxFunctor.comp_mapId, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp_val_app, CategoryTheory.Pseudofunctor.mapβ_associator_app, CategoryTheory.Cat.rightUnitor_hom_toNatTrans, Prod.snd_mapβ, CategoryTheory.Lax.OplaxTrans.naturality_comp, leftUnitor_inv_whiskerRight_assoc, whiskerRight_comp_symm_assoc, CategoryTheory.Pseudofunctor.DescentData.iso_hom, CategoryTheory.Oplax.StrongTrans.Modification.whiskerRight_naturality, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app_assoc, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_naturality_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.mk'_mapId, CategoryTheory.whiskerLeft_def, CategoryTheory.StrictlyUnitaryPseudofunctor.id_mapId_inv, Adj.rightUnitor_hom_Οr, Pith.pseudofunctorToPith_mapId_inv_iso_inv, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality, CategoryTheory.Pseudofunctor.mapComp_id_right, Adjunction.comp_counit, LeftExtension.whiskering_map, comp_whiskerRight, CategoryTheory.BicategoricalCoherence.left_iso, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_naturality, Bicategory.Opposite.bicategory_leftUnitor_hom_unop2, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id_app, comp_whiskerLeft_symm, Bicategory.Opposite.op2_whiskerRight, inv_whiskerRight, CategoryTheory.StrictlyUnitaryPseudofunctor.id_mapComp_inv, Pith.idβ_iso_inv, mateEquiv_symm_apply', CategoryTheory.Oplax.LaxTrans.naturality_naturality, CategoryTheory.Pseudofunctor.mapComp'_comp_id, CategoryTheory.Oplax.StrongTrans.naturality_comp, CategoryTheory.OplaxFunctor.mapβ_leftUnitor_assoc, CategoryTheory.Functor.toPseudoFunctor'_map, conjugateEquiv_id_comp_right_apply, CategoryTheory.Oplax.OplaxTrans.associator_inv_as_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp_app, CategoryTheory.Pseudofunctor.presheafHom_obj, Adjunction.homEquivβ_apply, CategoryTheory.Oplax.StrongTrans.naturality_id_assoc, CategoryTheory.StrictlyUnitaryLaxFunctorCore.mapComp_naturality_right, Adj.forgetβ_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app, CategoryTheory.Oplax.LaxTrans.naturality_id, CategoryTheory.whiskerRight_def, CategoryTheory.StrictlyUnitaryPseudofunctorCore.mapβ_left_unitor, CategoryTheory.Pseudofunctor.toLax_mapComp, CategoryTheory.Pseudofunctor.isoMapOfCommSq_horiz_id, CategoryTheory.Oplax.OplaxTrans.naturality_comp, CategoryTheory.Join.pseudofunctorLeft_mapComp_hom_toNatTrans_app, CategoryTheory.Lax.LaxTrans.naturality_comp, CategoryTheory.Pseudofunctor.DescentData.iso_inv, InducedBicategory.bicategory_whiskerRight_hom, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_naturality_assoc, CategoryTheory.Oplax.StrongTrans.id_naturality_inv, CategoryTheory.OplaxFunctor.mapComp_assoc_left_app, CategoryTheory.Lax.OplaxTrans.vComp_naturality_comp, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_assoc, CategoryTheory.Oplax.LaxTrans.id_app, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_leftUnitor_inv_as_app, CategoryTheory.Pseudofunctor.mapβ_right_unitor_assoc, Prod.sectL_mapComp_hom, associator_inv_naturality_left, CategoryTheory.Pseudofunctor.CoGrothendieck.instFullΞ±CategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality_app, leftUnitor_inv_naturality, whiskerLeft_whiskerLeft_inv_hom, CategoryTheory.Pseudofunctor.DescentData.nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq, unitors_equal, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerLeft_naturality_assoc, CategoryTheory.Cat.associator_inv_app, associator_naturality_right, whiskerRightIso_inv, precomposing_map_app, Prod.sectL_obj, CategoryTheory.Cat.Hom.comp_toFunctor, CategoryTheory.Cat.rightUnitor_hom_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_app_assoc, CategoryTheory.Oplax.LaxTrans.id_naturality, CategoryTheory.Pseudofunctor.ObjectProperty.ΞΉ_naturality, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_id, CategoryTheory.Pseudofunctor.mapComp_id_right_hom, conjugateEquiv_symm_of_iso, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp, CategoryTheory.Oplax.StrongTrans.Modification.naturality_assoc, CategoryTheory.LaxFunctor.mapComp_naturality_right_app_assoc, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_associator_hom_as_app, CategoryTheory.Lax.LaxTrans.vComp_naturality_naturality, prod_whiskerRight_snd, CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_mapβ, Adj.Bicategory.rightUnitor_hom_Οr, CategoryTheory.StrictPseudofunctor.comp_mapId_inv, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_obj, Adj.id_Οl, Adj.comp_Οl, CategoryTheory.Pseudofunctor.ObjectProperty.mapId_inv_app, CategoryTheory.PrelaxFunctor.mkOfHomFunctors_toPrelaxFunctorStruct, Comonad.comul_assoc_flip_assoc, CategoryTheory.OplaxFunctor.mapβ_associator_app_assoc, CategoryTheory.StrictPseudofunctor.mk'_mapComp, CategoryTheory.Pseudofunctor.mapComp_id_left_hom_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp, CategoryTheory.LaxFunctor.mapβ_associator_app_assoc, conjugateEquiv_comp_id_right_apply, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_mapβ_toNatTrans, CategoryTheory.Lax.LaxTrans.id_naturality, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_comp_assoc, whiskerLeft_rightUnitor_assoc, leftUnitor_inv_whiskerRight, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality_assoc, CategoryTheory.StrictlyUnitaryPseudofunctorCore.mapβ_associator, CategoryTheory.pseudofunctorOfIsLocallyDiscrete_obj, CategoryTheory.Functor.toOplaxFunctor_obj, instIsIsoHomLeftZigzagHom, Prod.fst_mapβ, Equivalence.right_triangle, CategoryTheory.Functor.toPseudoFunctor_mapComp, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_obj, CategoryTheory.Oplax.OplaxTrans.categoryStruct_id_app, InducedBicategory.forget_map, CategoryTheory.Pseudofunctor.DescentData.instIsIsoΞ±CategoryObjLocallyDiscreteOppositeCatMkOpHom, associator_eqToHom_inv, Equivalence.left_triangle, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_app, CategoryTheory.StrictlyUnitaryLaxFunctorCore.map_id, CategoryTheory.LaxFunctor.mapβ_leftUnitor_hom_app_assoc, CategoryTheory.OplaxFunctor.mapId'_eq_mapId, CategoryTheory.PrelaxFunctor.mapβ_eqToHom, Mathlib.Tactic.Bicategory.naturality_associator, Lan.CommuteWith.lanCompIso_inv, LanLift.existsUnique, CategoryTheory.Oplax.OplaxTrans.categoryStruct_comp_naturality, CategoryTheory.Iso.op2_hom_unop2, Bicategory.Opposite.bicategory_leftUnitor_inv_unop2, Prod.sectR_mapId_inv, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_naturality, CategoryTheory.Adjunction.toCat_counit_toNatTrans, CategoryTheory.PrelaxFunctor.mapβ_hom_inv, CategoryTheory.StrictlyUnitaryLaxFunctor.id_mapComp, CategoryTheory.OplaxFunctor.mapComp_assoc_right_app, CategoryTheory.Pseudofunctor.CoGrothendieck.ΞΉ_map_base, CategoryTheory.Pseudofunctor.StrongTrans.Modification.naturality, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp_app, CommRingCat.moduleCatRestrictScalarsPseudofunctor_map, InducedBicategory.bicategory_comp_hom, pentagon_inv_inv_hom_hom_inv, CategoryTheory.Pseudofunctor.StrongTrans.homCategory_id_as_app, CategoryTheory.Pseudofunctor.isPrestackFor_ofArrows_iff, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_assoc, CategoryTheory.FreeBicategory.mk_left_unitor_hom, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_app_assoc, Adjunction.ofCat_id, CategoryTheory.Join.pseudofunctorLeft_mapComp_inv_toNatTrans_app, CategoryTheory.Pseudofunctor.CoGrothendieck.map_obj_fiber, Adjunction.ofCat_comp, Pseudofunctor.ofLaxFunctorToLocallyGroupoid_mapIdIso_inv, CategoryTheory.oplaxFunctorOfIsLocallyDiscrete_map, CategoryTheory.Pseudofunctor.whiskerLeftIso_mapId, Lan.CommuteWith.lanCompIsoWhisker_hom_right, Prod.swap_map, CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_hom_app, Pith.rightUnitor_hom_iso, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_id_assoc, Comonad.counit_comul_assoc, CategoryTheory.OplaxFunctor.mapComp_assoc_left, Bicategory.Opposite.op2_rightUnitor_inv, CategoryTheory.LaxFunctor.mapβ_rightUnitor_hom_app, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp_assoc, CategoryTheory.Pseudofunctor.id_mapId, CategoryTheory.Pseudofunctor.DescentData.Hom.comm_assoc, CategoryTheory.BicategoricalCoherence.right'_iso, CategoryTheory.Lax.LaxTrans.naturality_comp_assoc, pentagon_assoc, CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj, Adj.id_Οr, CategoryTheory.Oplax.StrongTrans.Modification.id_app, prod_rightUnitor_inv_fst, CategoryTheory.LaxFunctor.mapComp'_eq_mapComp, CategoryTheory.Pseudofunctor.mapComp_id_left_inv_app_assoc, CategoryTheory.Oplax.LaxTrans.naturality_comp, Adj.Bicategory.leftUnitor_hom_Οl, CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_mapβ, CategoryTheory.Functor.toPseudoFunctor_map, whiskerLeft_isIso, CategoryTheory.Oplax.StrongTrans.isoMk_hom_as_app, conjugateIsoEquiv_apply_inv, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id_app, CategoryTheory.PrelaxFunctor.mapβ_inv_hom_isIso, CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_id_fiber, eqToHomTransIso_refl_right, CategoryTheory.Pseudofunctor.ObjectProperty.map_map_hom, CategoryTheory.Pseudofunctor.mapComp_id_left_inv_assoc, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality_app, pentagon_inv_inv_hom_inv_inv, CategoryTheory.PrelaxFunctor.mapβ_inv_hom_isIso_assoc, whiskerRight_iff, CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.congr, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app_assoc, CategoryTheory.Lax.LaxTrans.naturality_id_assoc, CategoryTheory.LaxFunctor.mapComp_naturality_right_assoc, CategoryTheory.FreeBicategory.preinclusion_mapβ, Pith.pseudofunctorToPith_mapComp_inv_iso_inv, prod_whiskerLeft_fst, CategoryTheory.Oplax.OplaxTrans.rightUnitor_hom_as_app, CategoryTheory.OplaxFunctor.mapβ_associator_assoc, precomp_obj, rightAdjointSquare.comp_hvcomp, CategoryTheory.Pseudofunctor.mapβ_whisker_left, CategoryTheory.Pseudofunctor.StrongTrans.isoMk_hom_as_app, adjointifyCounit_left_triangle, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_Οl, CategoryTheory.rightUnitor_def, CategoryTheory.Lax.StrongTrans.toLax_naturality, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id, CategoryTheory.Pseudofunctor.toOplax_mapId, prod_associator_inv_fst, whiskerLeft_rightUnitor_inv, CategoryTheory.PrelaxFunctor.mapβ_hom_inv_assoc, Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons, CategoryTheory.StrictlyUnitaryLaxFunctor.mapId_eq_eqToHom, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id, CategoryTheory.OplaxFunctor.mapComp_naturality_left_app, InducedBicategory.bicategory_Hom, CategoryTheory.StrictlyUnitaryLaxFunctor.map_id, CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerLeft_naturality, CategoryTheory.BicategoricalCoherence.tensorRight'_iso, CategoryTheory.oplaxFunctorOfIsLocallyDiscrete_obj, prod_Hom, Pith.whiskerRight_iso_hom, comp_whiskerRight_assoc, CategoryTheory.tensorHom_def, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv, hom_inv_whiskerRight_whiskerRight, Pith.rightUnitor_inv_iso_inv, LeftExtension.whiskerIdCancel_right, prod_rightUnitor_inv_snd, Pith.associator_hom_iso, Strict.id_comp, CategoryTheory.Cat.Hom.comp_map, CategoryTheory.Pseudofunctor.mapComp_id_right_hom_assoc, CategoryTheory.Lax.LaxTrans.naturality_id, CategoryTheory.Pseudofunctor.DescentData.ofObj_obj, CategoryTheory.Lax.StrongTrans.naturality_comp_assoc, associator_naturality_left_assoc, CategoryTheory.StrictPseudofunctorCore.mapβ_right_unitor, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_rightUnitor_inv_as_app, prod_leftUnitor_inv_fst, triangle_assoc_comp_right_inv_assoc, CategoryTheory.LaxFunctor.mapβ_rightUnitor_hom_app_assoc, hom_inv_whiskerRight, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_app, prod_rightUnitor_hom_fst, Adjunction.left_triangle, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id_val_app, CategoryTheory.Pseudofunctor.CoGrothendieck.ext_iff, CategoryTheory.Lax.OplaxTrans.naturality_naturality, Prod.fst_mapId_hom, triangle_assoc_comp_right_inv, associator_naturality_middle, prod_id_snd, CategoryTheory.Pseudofunctor.DescentData.hom_comp_assoc, CategoryTheory.Pseudofunctor.Grothendieck.map_obj_fiber, CategoryTheory.Oplax.LaxTrans.vComp_naturality_comp, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp_assoc, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp, prod_leftUnitor_inv_snd, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_app_assoc, CategoryTheory.StrictPseudofunctor.comp_map, Adj.Bicategory.rightUnitor_hom_Οl, LeftExtension.IsKan.fac_assoc, leftUnitorNatIso_hom_app, CategoryTheory.Pseudofunctor.CoGrothendieck.ΞΉ_obj_fiber, CategoryTheory.Iso.unop2_op_inv, Strict.assoc, CategoryTheory.PrelaxFunctor.mapβ_inv, CategoryTheory.StrictPseudofunctorPreCore.map_comp, Adj.Bicategory.leftUnitor_inv_Οl, CategoryTheory.StrictPseudofunctor.mk''_map, CategoryTheory.Oplax.StrongTrans.naturality_naturality_assoc, CategoryTheory.Pseudofunctor.isStackFor_iff, Bicategory.Opposite.opFunctor_obj, Prod.sectL_mapId_hom, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_id_naturality_hom, InducedBicategory.bicategory_rightUnitor_hom_hom, CategoryTheory.Pseudofunctor.isoMapOfCommSq_vert_id, LeftExtension.IsKan.uniqueUpToIso_hom_right, CommRingCat.moduleCatExtendScalarsPseudofunctor_map, Pith.whiskerLeft_iso_hom, CategoryTheory.Pseudofunctor.bijective_toDescentData_map_iff, mateEquiv_symm_apply, CategoryTheory.Pseudofunctor.mapβ_whisker_left_assoc, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_Οr, Strict.rightUnitor_eqToIso, Bicategory.Opposite.bicategory_whiskerRight_unop2, leftUnitor_whiskerRight, Bicategory.Opposite.homCategory_comp_unop2, CategoryTheory.Join.pseudofunctorRight_mapId_hom_toNatTrans_app, CategoryTheory.Pseudofunctor.CoGrothendieck.ΞΉ_map_fiber, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp_assoc, CategoryTheory.StrictPseudofunctor.toFunctor_obj, CategoryTheory.Oplax.StrongTrans.naturality_id, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_assoc, associator_eqToHom_inv_assoc, CategoryTheory.StrictPseudofunctor.map_comp, CategoryTheory.associator_def, CategoryTheory.Functor.toOplaxFunctor'_map, HasLeftKanLift.hasInitial, prod_leftUnitor_hom_snd, Lan.CommuteWith.instHasLeftKanExtensionComp, CategoryTheory.Pseudofunctor.mapComp_id_left_hom_assoc, CategoryTheory.Pseudofunctor.mapComp_id_right_inv_assoc, CategoryTheory.OplaxFunctor.mapComp_assoc_right_app_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.mapId_eq_eqToIso, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.id_obj, whiskerLeft_inv_hom_whiskerRight_assoc, CategoryTheory.Pseudofunctor.StrongTrans.isoMk_inv_as_app, whisker_exchange_assoc, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_rightUnitor_hom_as_app, InducedBicategory.bicategory_rightUnitor_inv_hom, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv, pentagon, CategoryTheory.Oplax.OplaxTrans.homCategory_comp_as_app, Prod.snd_obj, rightUnitor_naturality_assoc, CategoryTheory.Lax.OplaxTrans.vComp_naturality_naturality, CategoryTheory.OplaxFunctor.mapβ_rightUnitor_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom, CategoryTheory.StrictlyUnitaryPseudofunctorCore.mapβ_id, CategoryTheory.LocallyDiscrete.mkPseudofunctor_map, CategoryTheory.Lax.LaxTrans.vComp_naturality_id, CategoryTheory.Oplax.OplaxTrans.Modification.naturality_assoc, CategoryTheory.Lax.OplaxTrans.id_naturality, Lan.CommuteWith.lanCompIsoWhisker_inv_right, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObj_obj, CategoryTheory.PrelaxFunctor.mapFunctor_map, whiskerRight_congr, CategoryTheory.Oplax.StrongTrans.categoryStruct_comp_naturality, Bicategory.Opposite.op2_rightUnitor, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_assoc, LeftLift.whisker_unit, CategoryTheory.Oplax.OplaxTrans.naturality_id_assoc, prod_homCategory_id_fst, CategoryTheory.OplaxFunctor.mapβ_leftUnitor, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id_assoc, conjugateEquiv_symm_comp, pentagon_hom_hom_inv_inv_hom_assoc, CategoryTheory.StrictPseudofunctor.mk'_map, mateEquiv_hcomp, CategoryTheory.StrictlyUnitaryLaxFunctor.mk'_obj, CategoryTheory.Lax.LaxTrans.naturality_naturality, Adj.leftUnitor_inv_Οl, CommRingCat.moduleCatExtendScalarsPseudofunctor_obj, Bicategory.Opposite.op2_rightUnitor_hom, whiskerLeft_eqToHom, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_comp, Pith.idβ_iso_hom, associator_hom_congr, Mathlib.Tactic.Bicategory.naturality_leftUnitor, Bicategory.Opposite.unopFunctor_obj, pentagon_inv_inv_hom_inv_inv_assoc, CategoryTheory.Functor.toOplaxFunctor_mapComp, CategoryTheory.LaxFunctor.mapβ_rightUnitor_hom_assoc, Comonad.comul_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom, comp_whiskerLeft, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_app, CategoryTheory.OplaxFunctor.mapComp_naturality_left, CategoryTheory.Lax.StrongTrans.naturality_id, LeftLift.whiskerHom_right, prod_associator_hom_fst, LeftExtension.ofCompId_hom, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_leftUnitor_hom_as_app, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv, prod_homCategory_comp_fst, CategoryTheory.Lax.StrongTrans.categoryStruct_id_naturality, CategoryTheory.StrictlyUnitaryLaxFunctor.id_map, CategoryTheory.Pseudofunctor.mapComp_id_left_inv, CategoryTheory.WithInitial.pseudofunctor_mapId, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_Οr, CategoryTheory.Join.pseudofunctorRight_mapId_inv_toNatTrans_app, CategoryTheory.StrictlyUnitaryPseudofunctorCore.mapβ_whisker_left, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_iso, Comonad.counit_def, RingCat.moduleCatRestrictScalarsPseudofunctor_map, CategoryTheory.LaxFunctor.mapβ_associator, associator_inv_naturality_left_assoc, CategoryTheory.OplaxFunctor.mapComp_id_right_assoc, whiskerLeftIso_inv, CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_mapId, CategoryTheory.Oplax.StrongTrans.naturality_comp_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_mapComp_hom, CategoryTheory.tensorObj_def, CategoryTheory.Iso.unop2_hom, CategoryTheory.OplaxFunctor.mapComp_assoc_right, mateEquiv_eq_iff, LeftLift.ofIdComp_right, CategoryTheory.OplaxFunctor.mapComp_assoc_left_assoc, InducedBicategory.forget_mapId_inv, CategoryTheory.Pseudofunctor.ObjectProperty.IsClosedUnderMapObj.map_obj, postcomposing_map_app, Bicategory.Opposite.op2_comp, pentagon_inv_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_assoc, CategoryTheory.Pseudofunctor.StrongTrans.Modification.id_app, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_id_assoc, whiskerRight_comp, rightUnitorNatIso_inv_app, CategoryTheory.Pseudofunctor.StrongTrans.associator_inv_as_app, Bicategory.Opposite.op2_leftUnitor_hom, Comonad.comul_counit_assoc, congr_whiskerLeft, CategoryTheory.Pseudofunctor.toLax_mapId, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv, CategoryTheory.Cat.comp_eq_comp, CategoryTheory.Oplax.OplaxTrans.isoMk_hom_as_app, CategoryTheory.Cat.leftUnitor_hom_toNatTrans, pentagon_inv_hom_hom_hom_hom_assoc, whiskerLeft_inv_hom_whiskerRight, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app_assoc, Adj.comp_Οr_assoc, whisker_assoc_assoc, associator_eqToHom_hom, whisker_assoc_symm, CategoryTheory.Lax.StrongTrans.naturality_naturality_assoc, Prod.sectL_mapComp_inv, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_comp, AlgebraicGeometry.Scheme.Modules.pseudofunctor_obj_obj, id_whiskerLeft_assoc, LeftLift.IsKan.fac, Pith.id_of, Lan.CommuteWith.commute, InducedBicategory.forget_mapComp_inv, Bicategory.Opposite.op2_id, CategoryTheory.Pseudofunctor.IsStack.essSurj_of_sieve, toNatTrans_mateEquiv, CategoryTheory.Iso.unop2_op_hom, CategoryTheory.OplaxFunctor.mapβ_rightUnitor, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_app_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_app, CategoryTheory.StrictlyUnitaryLaxFunctorCore.mapComp_naturality_left, CategoryTheory.Cat.associator_inv_toNatTrans, CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_mapβ, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp, Mathlib.Tactic.Bicategory.naturality_id, CategoryTheory.Cat.leftUnitor_inv_toNatTrans, CategoryTheory.Pseudofunctor.mapβ_left_unitor_app, CategoryTheory.Pseudofunctor.mapId'_eq_mapId, associator_inv_naturality_right_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp, CategoryTheory.StrictPseudofunctor.toFunctor_map, Prod.snd_mapId_hom, hom_inv_whiskerRight_assoc, triangle, CategoryTheory.Pseudofunctor.StrongTrans.leftUnitor_hom_as_app, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_mapId_hom, CategoryTheory.Pseudofunctor.ObjectProperty.mapId_hom_app, CategoryTheory.LaxFunctor.mapβ_leftUnitor_hom_assoc, Prod.sectR_mapβ, CategoryTheory.StrictPseudofunctorPreCore.mapβ_whisker_right, Pseudofunctor.ofOplaxFunctorToLocallyGroupoid_mapIdIso_inv, CategoryTheory.PrelaxFunctor.id_toPrelaxFunctorStruct, CategoryTheory.FreeBicategory.normalize_naturality, Adj.rIso_hom, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom, CategoryTheory.StrictPseudofunctor.id_mapβ, Prod.sectL_map, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_app, conjugateIsoEquiv_apply_hom, id_whiskerRight, conjugateIsoEquiv_symm_apply_hom, CategoryTheory.Iso.op2_unop_inv_unop2, Pith.homβ_ext_iff, CategoryTheory.Lax.StrongTrans.naturality_id_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id_assoc, iterated_mateEquiv_conjugateEquiv_symm, Adj.rightUnitor_inv_Οr, CategoryTheory.Oplax.OplaxTrans.naturality_id, rightUnitor_comp, whiskerRight_id_symm, whiskerLeft_whiskerLeft_hom_inv, CategoryTheory.StrictlyUnitaryPseudofunctor.mk'_obj, CategoryTheory.OplaxFunctor.mapComp_id_right, triangle_assoc_comp_right, CategoryTheory.Pseudofunctor.toDescentData_obj, CategoryTheory.Cat.Hom.toNatIso_leftUnitor, comp_whiskerLeft_assoc, InducedBicategory.forget_mapComp_hom, CategoryTheory.Pseudofunctor.mapComp_id_right_inv, CategoryTheory.StrictlyUnitaryPseudofunctor.id_mapβ, LeftLift.whisker_lift, whiskerLeft_inv_hom_assoc, associatorNatIsoMiddle_hom_app, instHasInitialLeftExtensionOfHasLeftKanExtension, CategoryTheory.Pseudofunctor.mapβ_whisker_right_app_assoc, mateEquiv_square, CategoryTheory.Pseudofunctor.StrongTrans.Modification.naturality_assoc, LeftExtension.IsKan.uniqueUpToIso_inv_right, CategoryTheory.Lax.LaxTrans.naturality_naturality_assoc, Adj.forgetβ_toPrelaxFunctor_toPrelaxFunctorStruct_mapβ, rightUnitor_naturality, CategoryTheory.StrictlyUnitaryPseudofunctor.id_map, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_val_app, whiskerLeft_comp_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_iso, Pith.whiskerLeft_iso_inv, rightZigzagIso_symm, CategoryTheory.Join.pseudofunctorRight_mapComp_hom_toNatTrans_app, Pseudofunctor.ofLaxFunctorToLocallyGroupoid_mapIdIso_hom, CategoryTheory.LaxFunctor.mapβ_rightUnitor_assoc, CategoryTheory.Lax.StrongTrans.naturality_comp, whiskerLeftIso_hom, CategoryTheory.Lax.OplaxTrans.naturality_id_assoc, Mathlib.Tactic.Bicategory.structuralIso_inv, CategoryTheory.Functor.toOplaxFunctor_map, CategoryTheory.Pseudofunctor.mapβ_whisker_right, whiskerRight_id_assoc, Prod.sectR_obj, CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_apply, whisker_assoc_symm_assoc, CategoryTheory.Cat.Hom.toNatIso_rightUnitor, conjugateEquiv_apply', mateEquiv_conjugateEquiv_vcomp, CategoryTheory.OplaxFunctor.mapComp_assoc_right_assoc, Adj.Bicategory.leftUnitor_hom_Οr, CategoryTheory.Cat.Hom.id_obj, CategoryTheory.Pseudofunctor.StrongTrans.rightUnitor_inv_as_app, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app_assoc, CategoryTheory.Iso.op2_unop_hom_unop2, CategoryTheory.FreeBicategory.mk_associator_hom, Lan.CommuteWith.lanCompIso_hom, CategoryTheory.LaxFunctor.mapβ_leftUnitor, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_id_naturality_inv, CategoryTheory.LaxFunctor.mapComp_assoc_left_app, conjugateEquiv_adjunction_id, CategoryTheory.Cat.rightUnitor_inv_app, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app_assoc, CategoryTheory.Pseudofunctor.Grothendieck.Hom.ext_iff, Prod.snd_mapId_inv, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_as_app, InducedBicategory.bicategory_homCategory_comp_hom, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_as_app, CategoryTheory.Lax.StrongTrans.naturality_naturality, precomposing_obj, CategoryTheory.Cat.rightUnitor_inv_toNatTrans, pentagon_hom_inv_inv_inv_hom_assoc, CategoryTheory.Functor.toPseudoFunctor_mapId, CategoryTheory.Oplax.OplaxTrans.naturality_naturality, conjugateEquiv_of_iso, CategoryTheory.Pseudofunctor.isPrestackFor_iff, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_assoc, CategoryTheory.bicategoricalComp_refl, LeftLift.ofIdComp_hom, rightZigzagIso_inv, prod_comp_fst, CategoryTheory.Pseudofunctor.StrongTrans.associator_hom_as_app, CategoryTheory.Pseudofunctor.mapβ_right_unitor, CategoryTheory.Lax.LaxTrans.StrongCore.naturality_hom, CategoryTheory.tensorUnit_def, Pith.associator_inv_iso_inv, rightUnitor_comp_inv, CategoryTheory.Pseudofunctor.IsStackFor.isEquivalence, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_app, CategoryTheory.Adjunction.toCat_unit_toNatTrans, CategoryTheory.BicategoricalCoherence.whiskerRight_iso, whiskerLeft_hom_inv_assoc, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_comp_naturality_inv, LeftLift.whiskerOfIdCompIsoSelf_hom_right, CategoryTheory.Pseudofunctor.CoGrothendieck.instEssSurjΞ±CategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, Adj.id_l, Mathlib.Tactic.Bicategory.evalWhiskerRight_nil, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_app_assoc, CategoryTheory.Pseudofunctor.mapComp'_eq_mapComp, CategoryTheory.Cat.Hom.comp_obj, RingCat.moduleCatRestrictScalarsPseudofunctor_obj, CategoryTheory.pseudofunctorOfIsLocallyDiscrete_map, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp_app, HasLeftKanExtension.hasInitial, CategoryTheory.Pseudofunctor.Grothendieck.Hom.congr, CategoryTheory.PrelaxFunctor.mapβ_comp, Bicategory.Opposite.unop2_comp, CategoryTheory.OplaxFunctor.mapComp_naturality_left_assoc, CategoryTheory.StrictlyUnitaryLaxFunctor.mk'_mapβ, CategoryTheory.PrelaxFunctor.mapFunctor_obj, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_map, CategoryTheory.Pseudofunctor.Grothendieck.map_map_fiber, Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_mapβ_iso_hom, CategoryTheory.Pseudofunctor.StrongTrans.rightUnitor_hom_as_app, CategoryTheory.Pseudofunctor.mapβ_whisker_left_app_assoc, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_Ξ±, lanUnit_desc, CategoryTheory.StrictPseudofunctor.comp_mapComp_inv, whiskerLeft_id, pentagon_hom_inv_inv_inv_inv_assoc, CategoryTheory.Lax.StrongTrans.vComp_naturality_inv, Mathlib.Tactic.Bicategory.eval_of, CategoryTheory.LaxFunctor.mapComp_assoc_right_assoc, CategoryTheory.Oplax.StrongTrans.vcomp_naturality_hom, CategoryTheory.Pseudofunctor.CoGrothendieck.ΞΉ_obj_base, CategoryTheory.Lax.StrongTrans.id_naturality_inv, CategoryTheory.Pseudofunctor.mapComp_id_right_inv_app, CategoryTheory.Oplax.OplaxTrans.naturality_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp_id_left_hom_app, InducedBicategory.forget_obj, Adj.Bicategory.associator_inv_Οl, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_app_assoc, CategoryTheory.StrictPseudofunctor.id_map, CategoryTheory.Pseudofunctor.toDescentData_map_hom, CategoryTheory.Pseudofunctor.mapβ_associator, conjugateEquiv_associator_hom, Prod.swap_obj, CategoryTheory.PrelaxFunctor.mapβ_hom_inv_isIso, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_assoc, Pith.inclusion_mapId, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerRight_naturality_assoc, CategoryTheory.Pseudofunctor.ObjectProperty.IsClosedUnderIsomorphisms.isClosedUnderIsomorphisms, Strict.comp_id, CategoryTheory.StrictPseudofunctor.id_mapId_hom, Bicategory.Opposite.op2_leftUnitor_inv, InducedBicategory.Hom.category_comp_hom, Prod.fst_map, Adj.id_r, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_app_assoc, Adj.Homβ.conjugateEquiv_Οl, Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_mapβ_iso_inv, Pseudofunctor.ofOplaxFunctorToLocallyGroupoid_mapCompIso_inv, eqToHom_whiskerRight, Adj.associator_inv_Οl, prod_comp_snd, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq_assoc, CategoryTheory.Oplax.OplaxTrans.rightUnitor_inv_as_app, CategoryTheory.LaxFunctor.mapβ_rightUnitor_app_assoc, leftAdjointSquare.comp_vhcomp, Pith.compβ_iso_hom, lanLiftUnit_desc, leftUnitor_naturality_assoc, conjugateEquiv_id, CategoryTheory.Lax.StrongTrans.id_naturality_hom, CategoryTheory.StrictlyUnitaryLaxFunctor.mk'_map, whisker_assoc, CategoryTheory.Lax.OplaxTrans.naturality_id, Adj.comp_Οr, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_mapβ_toNatTrans_app, CategoryTheory.OplaxFunctor.PseudoCore.mapIdIso_hom, conjugateEquiv_symm_iso, InducedBicategory.isoMk_inv_hom, Prod.sectR_mapComp_hom, CategoryTheory.StrictPseudofunctor.mapComp_eq_eqToIso, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_map, CategoryTheory.PrelaxFunctor.mapβ_comp_assoc, CategoryTheory.LaxFunctor.mapComp_naturality_right, Bicategory.Opposite.unop2_op2, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_as_app, CategoryTheory.StrictPseudofunctorPreCore.mapβ_whisker_left, associatorNatIsoRight_hom_app, Adj.lIso_inv, instIsIsoHomRightZigzagHom, CategoryTheory.WithTerminal.pseudofunctor_mapId, associator_inv_congr, inv_whiskerLeft, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_id_app, CategoryTheory.Pseudofunctor.IsStackFor.essSurj, CategoryTheory.Pseudofunctor.id_mapComp, CategoryTheory.StrictPseudofunctor.mk'_mapβ, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_Ξ±, CategoryTheory.Functor.toPseudoFunctor'_mapId, CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, CategoryTheory.Iso.op2_inv_unop2, Bicategory.Opposite.op2_leftUnitor, CategoryTheory.PrelaxFunctor.mapβ_isIso, mateEquiv_leftUnitor_hom_rightUnitor_inv, LeftExtension.whisker_unit, conjugateEquiv_mateEquiv_vcomp, CategoryTheory.LaxFunctor.mapβ_rightUnitor_app, CategoryTheory.Pseudofunctor.mapComp'_id_comp, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_assoc, CategoryTheory.StrictPseudofunctor.comp_mapβ, prod_homCategory_id_snd, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app, Adj.Bicategory.associator_hom_Οr, InducedBicategory.forget_mapβ, Bicategory.Opposite.bicategory_homCategory_id_unop2, associatorNatIsoLeft_hom_app, LeftLift.whiskerIdCancel_right, CategoryTheory.PrelaxFunctor.comp_toPrelaxFunctorStruct, CategoryTheory.PrelaxFunctor.mapβ_inv_hom_assoc, CategoryTheory.Oplax.StrongTrans.isoMk_inv_as_app, Prod.fst_mapComp_inv, CategoryTheory.Oplax.StrongTrans.Modification.naturality, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom, CategoryTheory.StrictlyUnitaryPseudofunctorCore.mapβ_comp, CategoryTheory.WithTerminal.pseudofunctor_mapComp, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_Ξ±, CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj, Adj.associator_hom_Οr, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom, Bicategory.Opposite.unop2_id, LeftExtension.whiskerOfCompIdIsoSelf_hom_right, prod_leftUnitor_hom_fst, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_Οl, whiskerLeft_rightUnitor_inv_assoc, CategoryTheory.Oplax.OplaxTrans.naturality_comp_assoc, Adjunction.comp_left_triangle_aux, whiskerLeft_hom_inv_whiskerRight, CategoryTheory.Functor.toPseudoFunctor'_mapComp, CategoryTheory.Pseudofunctor.DescentData.exists_equivalence_of_sieve_eq, LeftLift.IsKan.uniqueUpToIso_hom_right, CategoryTheory.StrictlyUnitaryPseudofunctor.map_id, Bicategory.Opposite.bicategory_homCategory_comp_unop2, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id_app, CategoryTheory.LocallyDiscrete.mkPseudofunctor_obj, CategoryTheory.Pseudofunctor.mapComp_id_right_hom_app_assoc, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom, CategoryTheory.Lax.LaxTrans.vComp_naturality_comp, CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_inv_app_hom, id_whiskerLeft, LeftExtension.whisker_extension, Pith.associator_inv_iso_hom, whiskerLeft_hom_inv_whiskerRight_assoc, CategoryTheory.Pseudofunctor.mapComp_id_left_hom, prod_associator_inv_snd, CategoryTheory.OplaxFunctor.id_mapId, CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom_assoc, CategoryTheory.Oplax.LaxTrans.naturality_id_assoc, CategoryTheory.Pseudofunctor.mapβ_whisker_left_app, CategoryTheory.StrictlyUnitaryLaxFunctorCore.mapβ_rightUnitor, CategoryTheory.Pseudofunctor.DescentData.isEquivalence_toDescentData_iff_of_sieve_eq, CategoryTheory.Pseudofunctor.CoGrothendieck.comp_const, CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, LanLift.CommuteWith.commute, CategoryTheory.StrictlyUnitaryLaxFunctor.ext_iff, Prod.snd_mapComp_hom, leftUnitor_hom_congr, CategoryTheory.Oplax.StrongTrans.Modification.whiskerLeft_naturality_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.id_mapId_hom, Adj.leftUnitor_inv_Οr, whiskerRight_isIso, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_app, CategoryTheory.PrelaxFunctor.mapβ_id, rightUnitor_inv_naturality_assoc, CategoryTheory.Pseudofunctor.CoGrothendieck.compIso_inv_app, CategoryTheory.Oplax.OplaxTrans.isoMk_inv_as_app, CategoryTheory.StrictlyUnitaryLaxFunctor.comp_map, CategoryTheory.StrictPseudofunctor.mk''_mapComp, CategoryTheory.OplaxFunctor.mapβ_leftUnitor_app_assoc, CategoryTheory.Functor.toOplaxFunctor_mapId, CategoryTheory.BicategoricalCoherence.assoc_iso, Comonad.comul_assoc_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_hom_app_hom, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_assoc, Pith.leftUnitor_hom_iso, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app, instHasInitialLeftLiftOfHasLeftKanLift, CategoryTheory.StrictlyUnitaryPseudofunctorCore.map_id, Mathlib.Tactic.BicategoryCoherence.assoc_liftHomβ, lanUnit_desc_assoc, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_assoc, CategoryTheory.Oplax.LaxTrans.vComp_naturality_naturality, associator_naturality_left, whiskerLeft_whiskerLeft_inv_hom_assoc, Pith.rightUnitor_inv_iso_hom, Pith.compβ_iso_inv_assoc, InducedBicategory.bicategory_id_hom, CategoryTheory.StrictlyUnitaryPseudofunctor.mk'_mapβ, prod_homCategory_comp_snd, CategoryTheory.Oplax.StrongTrans.id_naturality_hom, leftUnitor_naturality, InducedBicategory.bicategory_homCategory_id_hom, CategoryTheory.StrictlyUnitaryLaxFunctor.mk'_mapId, Adj.Bicategory.associator_inv_Οr, CategoryTheory.LaxFunctor.mapComp_assoc_left, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_Οl, Comonad.counit_comul, CategoryTheory.Adjunction.ofCat_unit, Pith.pseudofunctorToPith_mapId_inv_iso_hom, CategoryTheory.OplaxFunctor.mapβ_rightUnitor_app, CategoryTheory.StrictlyUnitaryPseudofunctorCore.mapβ_right_unitor, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_app, CategoryTheory.LaxFunctor.mapComp_naturality_right_app, CategoryTheory.LaxFunctor.mapComp_assoc_right, LanLift.CommuteWith.lanLiftCompIsoWhisker_inv_right, mateEquiv_apply, Adj.associator_hom_Οl, LeftExtension.whiskerHom_right, CategoryTheory.StrictlyUnitaryLaxFunctor.comp_mapComp, InducedBicategory.bicategory_associator_hom_hom, CategoryTheory.Oplax.StrongTrans.naturality_naturality, CategoryTheory.Cat.id_eq_id, pentagon_hom_hom_inv_inv_hom, CategoryTheory.PrelaxFunctor.mapβIso_hom, Pseudofunctor.ofOplaxFunctorToLocallyGroupoid_mapIdIso_hom, CategoryTheory.Oplax.OplaxTrans.leftUnitor_hom_as_app, CategoryTheory.PrelaxFunctor.mapβIso_inv, CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom, CategoryTheory.Pseudofunctor.mapComp_id_right_hom_app, Pith.inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_assoc, Bicategory.Opposite.bicategory_associator_inv_unop2, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_assoc, CategoryTheory.Lax.OplaxTrans.naturality_comp_assoc, CategoryTheory.Pseudofunctor.DescentData.id_hom, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id, CategoryTheory.LaxFunctor.mapComp_naturality_left_app, pentagon_inv_inv_hom_hom_inv_assoc, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp, CategoryTheory.OplaxFunctor.mapComp_id_left_assoc, CategoryTheory.StrictPseudofunctor.mk'_mapId, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality, Pseudofunctor.ofLaxFunctorToLocallyGroupoid_mapCompIso_hom, CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_hom_app_hom, Prod.swap_mapComp_hom, CategoryTheory.Pseudofunctor.StrongTrans.Modification.vcomp_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_app, CategoryTheory.Pseudofunctor.DescentData.isoMk_hom_hom, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_assoc, LeftLift.ofIdComp_left_as, CategoryTheory.StrictPseudofunctor.id_mapId_inv, LeftExtension.whiskerOfCompIdIsoSelf_inv_right, CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq, CategoryTheory.StrictlyUnitaryLaxFunctor.mapIdIso_inv, Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_as, CategoryTheory.FreeBicategory.mk_associator_inv, Adj.comp_l, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_comp_assoc, rightUnitor_comp_assoc, Mathlib.Tactic.Bicategory.evalComp_nil_cons, Adj.leftUnitor_hom_Οr, CategoryTheory.Pseudofunctor.DescentData.hom_self, Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of, CategoryTheory.Pseudofunctor.DescentData.comp_hom_assoc, LeftExtension.IsKan.fac, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_mapId, CategoryTheory.Oplax.StrongTrans.categoryStruct_id_naturality, CategoryTheory.Pseudofunctor.ObjectProperty.map_obj_obj, LeftLift.IsKan.uniqueUpToIso_inv_right, CategoryTheory.FreeBicategory.lift_mapComp, Comonad.comul_counit, leftZigzagIso_inv, CategoryTheory.Functor.toOplaxFunctor'_mapComp, Adjunction.comp_right_triangle_aux, CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_comp_fiber, Adj.lIso_hom, CategoryTheory.Cat.whiskerLeft_toNatTrans, Prod.sectL_mapβ, CategoryTheory.Oplax.StrongTrans.toOplax_naturality, CategoryTheory.OplaxFunctor.mapComp_naturality_right_app_assoc, Adjunction.homEquivβ_symm_apply, CategoryTheory.Oplax.StrongTrans.Modification.whiskerRight_naturality_assoc, toNatTrans_conjugateEquiv, CategoryTheory.Lax.StrongTrans.categoryStruct_comp_naturality, Adjunction.comp_unit, CategoryTheory.FreeBicategory.lift_toPrelaxFunctor_toPrelaxFunctorStruct_mapβ, CategoryTheory.Pseudofunctor.comp_mapComp, Prod.swap_mapComp_inv, CategoryTheory.PrelaxFunctor.mapβIso_eqToIso, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp, Bicategory.Opposite.opFunctor_map, CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_mapComp, LeftLift.whiskering_obj, Prod.snd_mapComp_inv, Adj.Bicategory.associator_hom_Οl, CategoryTheory.StrictPseudofunctor.mk''_obj, Pith.compβ_iso_inv, CategoryTheory.Pseudofunctor.mapβ_whisker_right_app, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerLeft_naturality, conjugateEquiv_symm_apply', AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_r, CategoryTheory.Pseudofunctor.CoGrothendieck.instFaithfulΞ±CategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_iso, InducedBicategory.isoMk_hom_hom, Pith.inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj, whiskerLeft_rightUnitor, CategoryTheory.WithInitial.pseudofunctor_mapComp, CategoryTheory.leftUnitor_def, CategoryTheory.FreeBicategory.preinclusion_obj, CategoryTheory.Pseudofunctor.mapβ_left_unitor_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_assoc, CategoryTheory.Pseudofunctor.mapβ_right_unitor_app_assoc, pentagon_hom_inv_inv_inv_inv, CategoryTheory.Pseudofunctor.mapβ_right_unitor_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_naturality_app, CategoryTheory.FreeBicategory.lift_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map, CategoryTheory.LaxFunctor.comp_mapComp, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, CategoryTheory.PrelaxFunctor.mapβ_hom_inv_isIso_assoc, Pith.inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_mapβ, CategoryTheory.PrelaxFunctor.mapβ_inv_hom, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_Οr, conjugateEquiv_iso, Prod.sectR_mapId_hom, CategoryTheory.OplaxFunctor.mapComp_naturality_right, Strict.leftUnitor_eqToIso, CategoryTheory.OplaxFunctor.mapComp_naturality_left_app_assoc, CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_symm_apply, Prod.swap_mapId_hom, CategoryTheory.Cat.whiskerRight_app, conjugateEquiv_whiskerLeft, CategoryTheory.StrictlyUnitaryLaxFunctor.id_mapId, CategoryTheory.LaxFunctor.mapβ_associator_app, CategoryTheory.FreeBicategory.mk_right_unitor_hom, LeftExtension.whiskering_obj, CategoryTheory.StrictPseudofunctor.comp_obj, Bicategory.Opposite.homCategory_id_unop2, CategoryTheory.StrictPseudofunctor.id_mapComp_inv, InducedBicategory.mkHom_eqToHom, comp_whiskerLeft_symm_assoc, CommRingCat.moduleCatRestrictScalarsPseudofunctor_obj, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_app_assoc, Bicategory.Opposite.op2_id_unbop, leftUnitor_comp, CategoryTheory.BicategoricalCoherence.assoc'_iso, LeftExtension.w, CategoryTheory.Lax.OplaxTrans.vComp_naturality_id, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id, CategoryTheory.Cat.associator_hom_toNatTrans, Mathlib.Tactic.Bicategory.evalComp_nil_nil, CategoryTheory.LaxFunctor.mapComp_naturality_left, CategoryTheory.LaxFunctor.mapComp_assoc_left_assoc, LeftLift.whiskerOfIdCompIsoSelf_inv_right, associatorNatIsoMiddle_inv_app, CategoryTheory.Pseudofunctor.mapβ_whisker_right_assoc, CategoryTheory.Cat.Hom.id_toFunctor, InducedBicategory.forget_mapId_hom, InducedBicategory.categoryStruct_id_hom, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_assoc, Pith.pseudofunctorToPith_mapComp_inv_iso_hom, prod_rightUnitor_hom_snd, precomp_map, pentagon_hom_hom_inv_hom_hom, conjugateEquiv_symm_apply, prod_associator_hom_snd, Adjunction.right_triangle, triangle_assoc_comp_left_inv, CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerRight_naturality, CategoryTheory.Pseudofunctor.ObjectProperty.mapComp_inv_app, CategoryTheory.Oplax.OplaxTrans.Modification.naturality, CategoryTheory.BicategoricalCoherence.right_iso, Equivalence.right_triangle_hom, Prod.fst_obj, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_inv, CategoryTheory.LaxFunctor.mapComp_assoc_right_app_assoc, associatorNatIsoRight_inv_app, CategoryTheory.BicategoricalCoherence.whiskerLeft_iso, leftUnitor_comp_inv_assoc, leftUnitor_whiskerRight_assoc, leftUnitor_inv_congr, conjugateIsoEquiv_symm_apply_inv, Adj.forgetβ_mapComp, rightUnitor_hom_congr, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_mapComp_inv, CategoryTheory.Pseudofunctor.comp_mapId, Prod.swap_mapId_inv, CategoryTheory.OplaxFunctor.mapComp_naturality_right_app, Prod.sectR_map, CategoryTheory.StrictPseudofunctor.mk''_mapβ, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_mapId_inv, Bicategory.Opposite.op2_associator_hom, pentagon_hom_inv_inv_inv_hom, Adj.Bicategory.leftUnitor_inv_Οr, CategoryTheory.LaxFunctor.mapComp_assoc_left_app_assoc, CategoryTheory.Lax.OplaxTrans.id_app, CategoryTheory.Oplax.StrongTrans.homCategory_comp_as_app, rightZigzagIso_hom, CategoryTheory.LaxFunctor.id_mapComp, CategoryTheory.Cat.leftUnitor_inv_app, CategoryTheory.Functor.toPseudoFunctor_obj, associator_inv_naturality_middle_assoc, CategoryTheory.LaxFunctor.mapβ_leftUnitor_app, CategoryTheory.BicategoricalCoherence.refl_iso, rightUnitor_comp_inv_assoc, CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_Οl, CategoryTheory.Lax.OplaxTrans.naturality_naturality_assoc, InducedBicategory.bicategory_leftUnitor_hom_hom, CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_comp_fiber, CategoryTheory.StrictlyUnitaryLaxFunctor.comp_mapβ, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_app, Bicategory.Opposite.bicategory_rightUnitor_hom_unop2, CategoryTheory.Pseudofunctor.CoGrothendieck.compIso_hom_app, CategoryTheory.Pseudofunctor.DescentData.hom_comp, Strict.associator_eqToIso, CategoryTheory.Pseudofunctor.IsPrestackFor.nonempty_fullyFaithful, AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_Οr, CategoryTheory.Cat.whiskerLeft_app, CategoryTheory.OplaxFunctor.mapComp'_eq_mapComp, isRightAdjoint_TFAE, RightLift.w, CategoryTheory.Pseudofunctor.ObjectProperty.mapβ_app_hom, triangle_assoc, leftUnitorNatIso_inv_app, CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.ext_iff, CategoryTheory.OplaxFunctor.mapβ_rightUnitor_app_assoc, CategoryTheory.Oplax.StrongTrans.vcomp_naturality_inv, Bicategory.Opposite.bicategory_whiskerLeft_unop2, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv, CategoryTheory.Oplax.OplaxTrans.whiskerRight_as_app, associator_naturality_middle_assoc, Bicategory.Opposite.bicategory_rightUnitor_inv_unop2, CategoryTheory.Pseudofunctor.whiskerRightIso_mapId, CategoryTheory.Pseudofunctor.Grothendieck.map_map_base, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_associator_inv_as_app, CategoryTheory.Oplax.OplaxTrans.leftUnitor_inv_as_app, CategoryTheory.FreeBicategory.lift_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj, CategoryTheory.Functor.toOplaxFunctor'_mapId, CategoryTheory.LaxFunctor.mapβ_leftUnitor_hom, RightExtension.w, Prod.fst_mapId_inv, CategoryTheory.LaxFunctor.mapβ_rightUnitor_hom, Adj.leftUnitor_hom_Οl, LanLift.CommuteWith.lanLiftCompIso_inv, CategoryTheory.Oplax.OplaxTrans.Modification.id_app, CategoryTheory.StrictlyUnitaryLaxFunctor.comp_obj, Pith.pseudofunctorToPith_mapComp_hom_iso, mateEquiv_apply', Equivalence.left_triangle_hom, conjugateEquiv_comp, CategoryTheory.OplaxFunctor.mapComp_id_left, CategoryTheory.LaxFunctor.mapβ_leftUnitor_app_assoc, CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor, postcomp_map, CategoryTheory.LaxFunctor.mapβ_rightUnitor, LanLift.CommuteWith.lanLiftCompIsoWhisker_hom_right, triangle_assoc_comp_right_assoc, CategoryTheory.LaxFunctor.mapId'_eq_mapId, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_app_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.comp_mapβ, rightUnitorNatIso_hom_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_app, pentagon_inv_hom_hom_hom_inv_assoc, CategoryTheory.LaxFunctor.PseudoCore.mapIdIso_inv, leftUnitor_comp_assoc, LeftLift.w, CategoryTheory.LaxFunctor.mapComp_naturality_left_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_app, CategoryTheory.Pseudofunctor.DescentData.Hom.comm, CategoryTheory.StrictlyUnitaryLaxFunctorCore.mapβ_comp, CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map, triangle_assoc_comp_left_inv_assoc, CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_map, CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerRight_naturality_assoc
|
whiskerLeft π | CompOp | 365 mathmath: CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_assoc, prod_whiskerLeft_snd, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom, RightExtension.w_assoc, CategoryTheory.LaxFunctor.mapComp'_whiskerRight_comp_mapComp', CategoryTheory.Pseudofunctor.mapβ_associator_assoc, CategoryTheory.LaxFunctor.mapβ_associator_assoc, CategoryTheory.LaxFunctor.whiskerLeft_mapComp'_comp_mapComp'_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_naturality_assoc, Comonad.comul_assoc_flip, InducedBicategory.bicategory_whiskerLeft_hom, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_comp_mapComp'βββ_hom_assoc, conjugateEquiv_whiskerRight, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerRight_naturality, LeftLift.whiskering_map, leftUnitor_inv_naturality_assoc, CategoryTheory.Lax.StrongTrans.vComp_naturality_hom, whiskerLeft_inv_hom, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_comp_mapComp'_hom_whiskerRight_assoc, LeftExtension.w_assoc, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality, CategoryTheory.OplaxFunctor.mapβ_associator, mateEquiv_comp_id_right, whisker_exchange, pentagon_inv, Bicategory.Opposite.op2_whiskerLeft, Adjunction.homEquivβ_symm_apply, CategoryTheory.Oplax.LaxTrans.vComp_naturality_id, Lan.existsUnique, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp'_hom_comp_whiskerLeft_mapComp'_hom, conjugateEquiv_adjunction_id_symm, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_assoc, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp_assoc, CategoryTheory.StrictlyUnitaryLaxFunctorCore.mapβ_associator, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_comp_naturality_hom, CategoryTheory.OplaxFunctor.mapComp_naturality_right_assoc, CategoryTheory.Oplax.LaxTrans.naturality_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_comp_whiskerLeft_mapComp'_hom, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id_assoc, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_whiskerLeft_as_app, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv, pentagon_hom_hom_inv_hom_hom_assoc, pentagon_inv_hom_hom_hom_hom, Adjunction.homEquivβ_apply, associator_inv_naturality_middle, associator_naturality_right_assoc, CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerLeft_naturality_assoc, triangle_assoc_comp_left, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom, associator_inv_naturality_right, whiskerLeft_iff, whiskerLeft_comp, CategoryTheory.Pseudofunctor.mapComp'βββ_inv, CategoryTheory.Oplax.StrongTrans.Modification.whiskerLeft_naturality, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv, associator_eqToHom_hom_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality, CategoryTheory.Oplax.LaxTrans.naturality_comp_assoc, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_id, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_naturality, whiskerLeft_hom_inv, mateEquiv_id_comp_right, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id, whiskerLeft_whiskerLeft_hom_inv_assoc, id_whiskerLeft_symm, pentagon_inv_hom_hom_hom_inv, CategoryTheory.Lax.OplaxTrans.naturality_comp, CategoryTheory.Oplax.StrongTrans.Modification.whiskerRight_naturality, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_naturality_assoc, CategoryTheory.whiskerLeft_def, CategoryTheory.Pseudofunctor.mapComp'βββ_hom, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_naturality, comp_whiskerLeft_symm, Bicategory.Opposite.op2_whiskerRight, mateEquiv_symm_apply', CategoryTheory.Oplax.LaxTrans.naturality_naturality, CategoryTheory.Oplax.StrongTrans.naturality_comp, Adjunction.homEquivβ_apply, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_assoc, CategoryTheory.Oplax.StrongTrans.naturality_id_assoc, CategoryTheory.StrictlyUnitaryLaxFunctorCore.mapComp_naturality_right, CategoryTheory.Oplax.LaxTrans.naturality_id, CategoryTheory.Oplax.OplaxTrans.naturality_comp, CategoryTheory.Lax.LaxTrans.naturality_comp, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_naturality_assoc, CategoryTheory.Lax.OplaxTrans.vComp_naturality_comp, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_comp_whiskerLeft_mapComp'_hom_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_assoc, CategoryTheory.Pseudofunctor.mapβ_right_unitor_assoc, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_comp_mapComp'_inv, leftUnitor_inv_naturality, whiskerLeft_whiskerLeft_inv_hom, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerLeft_naturality_assoc, associator_naturality_right, Mathlib.Tactic.Bicategory.structuralIsoOfExpr_whiskerLeft, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_id, CategoryTheory.Pseudofunctor.mapComp_id_right_hom, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp, CategoryTheory.Oplax.StrongTrans.Modification.naturality_assoc, CategoryTheory.LaxFunctor.mapComp_naturality_right_app_assoc, CategoryTheory.Lax.LaxTrans.vComp_naturality_naturality, Comonad.comul_assoc_flip_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_comp_assoc, whiskerLeft_rightUnitor_assoc, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality_assoc, CategoryTheory.StrictlyUnitaryPseudofunctorCore.mapβ_associator, associator_eqToHom_inv, CategoryTheory.Pseudofunctor.mapComp'βββ_hom, CategoryTheory.Oplax.OplaxTrans.categoryStruct_comp_naturality, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_naturality, CategoryTheory.Pseudofunctor.StrongTrans.Modification.naturality, pentagon_inv_inv_hom_hom_inv, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_assoc, Adj.Bicategory.whiskerLeft_Οl, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_id_assoc, CategoryTheory.OplaxFunctor.mapComp_assoc_left, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp_assoc, CategoryTheory.Lax.LaxTrans.naturality_comp_assoc, pentagon_assoc, CategoryTheory.Oplax.LaxTrans.naturality_comp, whiskerLeft_isIso, pentagon_inv_inv_hom_inv_inv, Adj.whiskerRight_Οr, CategoryTheory.Lax.LaxTrans.naturality_id_assoc, CategoryTheory.LaxFunctor.mapComp_naturality_right_assoc, CategoryTheory.OplaxFunctor.mapComp'_comp_mapComp'_whiskerRight, prod_whiskerLeft_fst, CategoryTheory.OplaxFunctor.mapβ_associator_assoc, CategoryTheory.Pseudofunctor.mapβ_whisker_left, CategoryTheory.LaxFunctor.mapComp'_whiskerRight_comp_mapComp'_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id, whiskerLeft_rightUnitor_inv, CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerLeft_naturality, CategoryTheory.Pseudofunctor.mapComp'βββ_inv, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv, CategoryTheory.Pseudofunctor.mapComp_id_right_hom_assoc, CategoryTheory.Lax.LaxTrans.naturality_id, CategoryTheory.Lax.StrongTrans.naturality_comp_assoc, triangle_assoc_comp_right_inv_assoc, CategoryTheory.Lax.OplaxTrans.naturality_naturality, CategoryTheory.LaxFunctor.whiskerLeft_mapComp'_comp_mapComp', triangle_assoc_comp_right_inv, associator_naturality_middle, CategoryTheory.Oplax.LaxTrans.vComp_naturality_comp, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp_assoc, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp, LeftExtension.IsKan.fac_assoc, CategoryTheory.Oplax.StrongTrans.naturality_naturality_assoc, Pith.whiskerLeft_iso_hom, CategoryTheory.Pseudofunctor.mapβ_whisker_left_assoc, Bicategory.Opposite.bicategory_whiskerRight_unop2, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp_assoc, CategoryTheory.Oplax.StrongTrans.naturality_id, associator_eqToHom_inv_assoc, CategoryTheory.Pseudofunctor.mapComp_id_right_inv_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_assoc, whiskerLeft_inv_hom_whiskerRight_assoc, whisker_exchange_assoc, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv, pentagon, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_assoc, CategoryTheory.Lax.OplaxTrans.vComp_naturality_naturality, CategoryTheory.OplaxFunctor.mapβ_rightUnitor_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom, CategoryTheory.Lax.LaxTrans.vComp_naturality_id, CategoryTheory.FreeBicategory.mk_whisker_left, CategoryTheory.Oplax.OplaxTrans.Modification.naturality_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_assoc, LeftLift.whisker_unit, CategoryTheory.Oplax.OplaxTrans.naturality_id_assoc, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id_assoc, pentagon_hom_hom_inv_inv_hom_assoc, CategoryTheory.Lax.LaxTrans.naturality_naturality, whiskerLeft_eqToHom, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_comp, Adj.whiskerLeft_Οr, pentagon_inv_inv_hom_inv_inv_assoc, CategoryTheory.LaxFunctor.mapβ_rightUnitor_hom_assoc, Comonad.comul_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom, comp_whiskerLeft, CategoryTheory.Lax.StrongTrans.naturality_id, LeftLift.whiskerHom_right, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'βββ_inv, CategoryTheory.StrictlyUnitaryPseudofunctorCore.mapβ_whisker_left, CategoryTheory.LaxFunctor.mapβ_associator, CategoryTheory.OplaxFunctor.mapComp_id_right_assoc, whiskerLeftIso_inv, CategoryTheory.Oplax.StrongTrans.naturality_comp_assoc, CategoryTheory.OplaxFunctor.mapComp_assoc_right, CategoryTheory.OplaxFunctor.mapComp_assoc_left_assoc, postcomposing_map_app, pentagon_inv_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_assoc, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_id_assoc, Comonad.comul_counit_assoc, congr_whiskerLeft, pentagon_inv_hom_hom_hom_hom_assoc, whiskerLeft_inv_hom_whiskerRight, whisker_assoc_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_comp_mapComp'βββ_hom, associator_eqToHom_hom, whisker_assoc_symm, CategoryTheory.Lax.StrongTrans.naturality_naturality_assoc, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_comp, id_whiskerLeft_assoc, CategoryTheory.OplaxFunctor.mapβ_rightUnitor, associator_inv_naturality_right_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp, triangle, CategoryTheory.FreeBicategory.normalize_naturality, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom, CategoryTheory.Pseudofunctor.mapComp'_inv_comp_mapComp'_hom, CategoryTheory.Lax.StrongTrans.naturality_id_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id_assoc, CategoryTheory.Oplax.OplaxTrans.naturality_id, rightUnitor_comp, whiskerLeft_whiskerLeft_hom_inv, CategoryTheory.OplaxFunctor.mapComp_id_right, triangle_assoc_comp_right, comp_whiskerLeft_assoc, CategoryTheory.Pseudofunctor.mapComp_id_right_inv, whiskerLeft_inv_hom_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_comp_mapComp'βββ_hom_assoc, CategoryTheory.Pseudofunctor.StrongTrans.Modification.naturality_assoc, CategoryTheory.Lax.LaxTrans.naturality_naturality_assoc, whiskerLeft_comp_assoc, Pith.whiskerLeft_iso_inv, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'βββ_inv_assoc, CategoryTheory.LaxFunctor.mapβ_rightUnitor_assoc, CategoryTheory.Lax.StrongTrans.naturality_comp, whiskerLeftIso_hom, CategoryTheory.Lax.OplaxTrans.naturality_id_assoc, whisker_assoc_symm_assoc, conjugateEquiv_apply', CategoryTheory.OplaxFunctor.mapComp_assoc_right_assoc, conjugateEquiv_adjunction_id, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_as_app, CategoryTheory.Lax.StrongTrans.naturality_naturality, pentagon_hom_inv_inv_inv_hom_assoc, CategoryTheory.Oplax.OplaxTrans.naturality_naturality, CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_assoc, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'_inv, CategoryTheory.Pseudofunctor.mapβ_right_unitor, rightUnitor_comp_inv, whiskerLeft_hom_inv_assoc, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_comp_naturality_inv, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'βββ_inv_assoc, CategoryTheory.Pseudofunctor.mapβ_whisker_left_app_assoc, lanUnit_desc, whiskerLeft_id, pentagon_hom_inv_inv_inv_inv_assoc, CategoryTheory.Lax.StrongTrans.vComp_naturality_inv, CategoryTheory.LaxFunctor.mapComp_assoc_right_assoc, CategoryTheory.Oplax.StrongTrans.vcomp_naturality_hom, CategoryTheory.Oplax.OplaxTrans.naturality_naturality_assoc, Adj.whiskerLeft_Οl, CategoryTheory.Pseudofunctor.mapβ_associator, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_assoc, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerRight_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_assoc, CategoryTheory.OplaxFunctor.mapComp'_comp_whiskerLeft_mapComp', leftUnitor_naturality_assoc, whisker_assoc, CategoryTheory.Lax.OplaxTrans.naturality_id, CategoryTheory.LaxFunctor.mapComp_naturality_right, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_as_app, CategoryTheory.StrictPseudofunctorPreCore.mapβ_whisker_left, inv_whiskerLeft, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_assoc, CategoryTheory.Oplax.StrongTrans.Modification.naturality, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom, whiskerLeft_rightUnitor_inv_assoc, CategoryTheory.Oplax.OplaxTrans.naturality_comp_assoc, whiskerLeft_hom_inv_whiskerRight, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_comp_mapComp'βββ_hom, CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom, CategoryTheory.Lax.LaxTrans.vComp_naturality_comp, id_whiskerLeft, whiskerLeft_hom_inv_whiskerRight_assoc, CategoryTheory.Oplax.LaxTrans.naturality_id_assoc, CategoryTheory.Pseudofunctor.mapβ_whisker_left_app, leftUnitor_hom_congr, CategoryTheory.Oplax.StrongTrans.Modification.whiskerLeft_naturality_assoc, Comonad.comul_assoc_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_assoc, lanUnit_desc_assoc, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_assoc, CategoryTheory.Oplax.LaxTrans.vComp_naturality_naturality, whiskerLeft_whiskerLeft_inv_hom_assoc, leftUnitor_naturality, CategoryTheory.LaxFunctor.mapComp_assoc_left, CategoryTheory.LaxFunctor.mapComp_naturality_right_app, CategoryTheory.LaxFunctor.mapComp_assoc_right, Adj.Bicategory.whiskerRight_Οr, CategoryTheory.Oplax.StrongTrans.naturality_naturality, pentagon_hom_hom_inv_inv_hom, CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_assoc, CategoryTheory.Lax.OplaxTrans.naturality_comp_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id, pentagon_inv_inv_hom_hom_inv_assoc, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_assoc, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_comp_assoc, rightUnitor_comp_assoc, LeftExtension.IsKan.fac, Comonad.comul_counit, CategoryTheory.Cat.whiskerLeft_toNatTrans, CategoryTheory.OplaxFunctor.mapComp_naturality_right_app_assoc, Adjunction.homEquivβ_symm_apply, CategoryTheory.Oplax.StrongTrans.Modification.whiskerRight_naturality_assoc, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerLeft_naturality, conjugateEquiv_symm_apply', whiskerLeft_rightUnitor, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_assoc, pentagon_hom_inv_inv_inv_inv, CategoryTheory.OplaxFunctor.mapComp_naturality_right, conjugateEquiv_whiskerLeft, CategoryTheory.OplaxFunctor.mapComp'_comp_mapComp'_whiskerRight_assoc, comp_whiskerLeft_symm_assoc, LeftExtension.w, CategoryTheory.Lax.OplaxTrans.vComp_naturality_id, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id, CategoryTheory.LaxFunctor.mapComp_assoc_left_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_assoc, precomp_map, pentagon_hom_hom_inv_hom_hom, triangle_assoc_comp_left_inv, CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerRight_naturality, CategoryTheory.Oplax.OplaxTrans.Modification.naturality, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_inv, leftUnitor_inv_congr, CategoryTheory.OplaxFunctor.mapComp_naturality_right_app, CategoryTheory.OplaxFunctor.mapComp'_comp_whiskerLeft_mapComp'_assoc, pentagon_hom_inv_inv_inv_hom, associator_inv_naturality_middle_assoc, rightUnitor_comp_inv_assoc, CategoryTheory.Lax.OplaxTrans.naturality_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'βββ_inv, CategoryTheory.Pseudofunctor.mapComp'_hom_comp_mapComp'_hom_whiskerRight, CategoryTheory.Cat.whiskerLeft_app, triangle_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_comp_mapComp'_hom_whiskerRight, CategoryTheory.Oplax.StrongTrans.vcomp_naturality_inv, Bicategory.Opposite.bicategory_whiskerLeft_unop2, associator_naturality_middle_assoc, RightExtension.w, CategoryTheory.LaxFunctor.mapβ_rightUnitor_hom, Mathlib.Tactic.Bicategory.evalWhiskerLeft_id, mateEquiv_apply', CategoryTheory.LaxFunctor.mapβ_rightUnitor, triangle_assoc_comp_right_assoc, pentagon_inv_hom_hom_hom_inv_assoc, triangle_assoc_comp_left_inv_assoc, CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerRight_naturality_assoc
|
whiskerLeftIso π | CompOp | 22 mathmath: Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil, Mathlib.Tactic.Bicategory.naturality_rightUnitor, CategoryTheory.BicategoricalCoherence.tensorRight_iso, CategoryTheory.Pseudofunctor.mapComp_id_right, CategoryTheory.Pseudofunctor.mapComp'_comp_id, CategoryTheory.Pseudofunctor.isoMapOfCommSq_horiz_id, Mathlib.Tactic.Bicategory.structuralIsoOfExpr_whiskerLeft, Mathlib.Tactic.Bicategory.naturality_associator, CategoryTheory.Pseudofunctor.whiskerLeftIso_mapId, Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons, CategoryTheory.BicategoricalCoherence.tensorRight'_iso, CategoryTheory.Pseudofunctor.isoMapOfCommSq_vert_id, CategoryTheory.Oplax.StrongTrans.categoryStruct_comp_naturality, Mathlib.Tactic.Bicategory.naturality_leftUnitor, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_iso, whiskerLeftIso_inv, Mathlib.Tactic.Bicategory.naturality_id, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_iso, whiskerLeftIso_hom, CategoryTheory.Lax.StrongTrans.categoryStruct_comp_naturality, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_iso, CategoryTheory.BicategoricalCoherence.whiskerLeft_iso
|
whiskerRight π | CompOp | 362 mathmath: CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom, CategoryTheory.LaxFunctor.mapComp'_whiskerRight_comp_mapComp', CategoryTheory.FreeBicategory.mk_whisker_right, CategoryTheory.Pseudofunctor.mapβ_associator_assoc, CategoryTheory.LaxFunctor.mapβ_associator_assoc, CategoryTheory.LaxFunctor.whiskerLeft_mapComp'_comp_mapComp'_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_naturality_assoc, Comonad.comul_assoc_flip, Mathlib.Tactic.Bicategory.evalWhiskerRight_id, CategoryTheory.Cat.whiskerRight_toNatTrans, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_comp_mapComp'βββ_hom_assoc, conjugateEquiv_whiskerRight, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerRight_naturality, CategoryTheory.Lax.StrongTrans.vComp_naturality_hom, whiskerRight_comp_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_comp_mapComp'_hom_whiskerRight_assoc, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality, CategoryTheory.OplaxFunctor.mapβ_associator, inv_hom_whiskerRight_whiskerRight_assoc, inv_hom_whiskerRight_assoc, whisker_exchange, inv_hom_whiskerRight, CategoryTheory.LaxFunctor.mapβ_leftUnitor_assoc, pentagon_inv, Bicategory.Opposite.op2_whiskerLeft, Adjunction.homEquivβ_symm_apply, CategoryTheory.Pseudofunctor.mapβ_left_unitor_assoc, CategoryTheory.Oplax.LaxTrans.vComp_naturality_id, CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_whiskerRight_as_app, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality_assoc, RightLift.w_assoc, CategoryTheory.Pseudofunctor.mapComp'_hom_comp_whiskerLeft_mapComp'_hom, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_assoc, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp_assoc, CategoryTheory.StrictlyUnitaryLaxFunctorCore.mapβ_associator, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_comp_naturality_hom, CategoryTheory.Oplax.LaxTrans.naturality_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_comp_whiskerLeft_mapComp'_hom, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv, pentagon_hom_hom_inv_hom_hom_assoc, LeftLift.w_assoc, whiskerRightIso_hom, pentagon_inv_hom_hom_hom_hom, rightUnitor_inv_naturality, Adjunction.homEquivβ_apply, Pith.whiskerRight_iso_inv, rightUnitor_inv_congr, CategoryTheory.Pseudofunctor.mapβ_left_unitor, associator_inv_naturality_middle, CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerLeft_naturality_assoc, hom_inv_whiskerRight_whiskerRight_assoc, triangle_assoc_comp_left, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom, CategoryTheory.Pseudofunctor.mapComp'βββ_inv, CategoryTheory.Oplax.StrongTrans.Modification.whiskerLeft_naturality, CategoryTheory.LaxFunctor.mapComp_naturality_left_app_assoc, prod_whiskerRight_fst, whiskerRight_comp_symm, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv, associator_eqToHom_hom_assoc, whiskerRight_id, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_naturality, CategoryTheory.Oplax.LaxTrans.naturality_comp_assoc, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_id, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_naturality, lanLiftUnit_desc_assoc, Adj.Bicategory.whiskerRight_Οl, leftUnitor_comp_inv, CategoryTheory.StrictlyUnitaryPseudofunctorCore.mapβ_whisker_right, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id, inv_hom_whiskerRight_whiskerRight, LeftLift.IsKan.fac_assoc, pentagon_inv_hom_hom_hom_inv, CategoryTheory.Lax.OplaxTrans.naturality_comp, leftUnitor_inv_whiskerRight_assoc, whiskerRight_comp_symm_assoc, CategoryTheory.Oplax.StrongTrans.Modification.whiskerRight_naturality, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_hom, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality, LeftExtension.whiskering_map, comp_whiskerRight, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_naturality, Bicategory.Opposite.op2_whiskerRight, inv_whiskerRight, mateEquiv_symm_apply', CategoryTheory.Oplax.LaxTrans.naturality_naturality, CategoryTheory.Oplax.StrongTrans.naturality_comp, CategoryTheory.OplaxFunctor.mapβ_leftUnitor_assoc, Adjunction.homEquivβ_apply, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_assoc, CategoryTheory.Oplax.StrongTrans.naturality_id_assoc, CategoryTheory.Oplax.LaxTrans.naturality_id, CategoryTheory.whiskerRight_def, CategoryTheory.Oplax.OplaxTrans.naturality_comp, CategoryTheory.Lax.LaxTrans.naturality_comp, InducedBicategory.bicategory_whiskerRight_hom, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_naturality_assoc, CategoryTheory.Lax.OplaxTrans.vComp_naturality_comp, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_comp_whiskerLeft_mapComp'_hom_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_assoc, associator_inv_naturality_left, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_comp_mapComp'_inv, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerLeft_naturality_assoc, whiskerRightIso_inv, precomposing_map_app, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_id, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp, CategoryTheory.Oplax.StrongTrans.Modification.naturality_assoc, CategoryTheory.Lax.LaxTrans.vComp_naturality_naturality, prod_whiskerRight_snd, Comonad.comul_assoc_flip_assoc, Adj.Bicategory.whiskerLeft_Οr, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_comp_assoc, leftUnitor_inv_whiskerRight, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality_assoc, CategoryTheory.StrictlyUnitaryPseudofunctorCore.mapβ_associator, associator_eqToHom_inv, CategoryTheory.Pseudofunctor.mapComp'βββ_hom, LanLift.existsUnique, CategoryTheory.Oplax.OplaxTrans.categoryStruct_comp_naturality, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_naturality, CategoryTheory.Pseudofunctor.StrongTrans.Modification.naturality, pentagon_inv_inv_hom_hom_inv, CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_assoc, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_id_assoc, Comonad.counit_comul_assoc, CategoryTheory.OplaxFunctor.mapComp_assoc_left, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp_assoc, CategoryTheory.Lax.LaxTrans.naturality_comp_assoc, pentagon_assoc, CategoryTheory.Oplax.LaxTrans.naturality_comp, CategoryTheory.Pseudofunctor.mapComp_id_left_inv_assoc, pentagon_inv_inv_hom_inv_inv, whiskerRight_iff, Adj.whiskerRight_Οr, CategoryTheory.Lax.LaxTrans.naturality_id_assoc, CategoryTheory.OplaxFunctor.mapComp'_comp_mapComp'_whiskerRight, CategoryTheory.OplaxFunctor.mapβ_associator_assoc, CategoryTheory.LaxFunctor.mapComp'_whiskerRight_comp_mapComp'_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id, CategoryTheory.OplaxFunctor.mapComp_naturality_left_app, CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerLeft_naturality, Pith.whiskerRight_iso_hom, comp_whiskerRight_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_inv, hom_inv_whiskerRight_whiskerRight, CategoryTheory.Lax.LaxTrans.naturality_id, CategoryTheory.Lax.StrongTrans.naturality_comp_assoc, associator_naturality_left_assoc, triangle_assoc_comp_right_inv_assoc, hom_inv_whiskerRight, CategoryTheory.Lax.OplaxTrans.naturality_naturality, CategoryTheory.LaxFunctor.whiskerLeft_mapComp'_comp_mapComp', triangle_assoc_comp_right_inv, associator_naturality_middle, CategoryTheory.Oplax.LaxTrans.vComp_naturality_comp, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp_assoc, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp, CategoryTheory.Oplax.StrongTrans.naturality_naturality_assoc, Bicategory.Opposite.bicategory_whiskerRight_unop2, leftUnitor_whiskerRight, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp_assoc, CategoryTheory.Oplax.StrongTrans.naturality_id, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_assoc, associator_eqToHom_inv_assoc, CategoryTheory.Pseudofunctor.mapComp_id_left_hom_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_assoc, whiskerLeft_inv_hom_whiskerRight_assoc, whisker_exchange_assoc, pentagon, rightUnitor_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_assoc, CategoryTheory.Lax.OplaxTrans.vComp_naturality_naturality, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom, CategoryTheory.Lax.LaxTrans.vComp_naturality_id, CategoryTheory.Oplax.OplaxTrans.Modification.naturality_assoc, whiskerRight_congr, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_assoc, CategoryTheory.Oplax.OplaxTrans.naturality_id_assoc, CategoryTheory.OplaxFunctor.mapβ_leftUnitor, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id_assoc, pentagon_hom_hom_inv_inv_hom_assoc, CategoryTheory.Lax.LaxTrans.naturality_naturality, CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_comp, Adj.whiskerLeft_Οr, pentagon_inv_inv_hom_inv_inv_assoc, Comonad.comul_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom, CategoryTheory.OplaxFunctor.mapComp_naturality_left, CategoryTheory.Lax.StrongTrans.naturality_id, CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'βββ_inv, CategoryTheory.Pseudofunctor.mapComp_id_left_inv, CategoryTheory.LaxFunctor.mapβ_associator, associator_inv_naturality_left_assoc, CategoryTheory.Oplax.StrongTrans.naturality_comp_assoc, CategoryTheory.OplaxFunctor.mapComp_assoc_right, CategoryTheory.OplaxFunctor.mapComp_assoc_left_assoc, pentagon_inv_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_assoc, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_id_assoc, whiskerRight_comp, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv, pentagon_inv_hom_hom_hom_hom_assoc, whiskerLeft_inv_hom_whiskerRight, whisker_assoc_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_comp_mapComp'βββ_hom, associator_eqToHom_hom, whisker_assoc_symm, CategoryTheory.Lax.StrongTrans.naturality_naturality_assoc, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_comp, LeftLift.IsKan.fac, CategoryTheory.StrictlyUnitaryLaxFunctorCore.mapComp_naturality_left, Adj.whiskerRight_Οl, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp, hom_inv_whiskerRight_assoc, triangle, CategoryTheory.LaxFunctor.mapβ_leftUnitor_hom_assoc, CategoryTheory.StrictPseudofunctorPreCore.mapβ_whisker_right, id_whiskerRight, CategoryTheory.Pseudofunctor.mapComp'_inv_comp_mapComp'_hom, CategoryTheory.Lax.StrongTrans.naturality_id_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id_assoc, CategoryTheory.Oplax.OplaxTrans.naturality_id, whiskerRight_id_symm, triangle_assoc_comp_right, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_comp_mapComp'βββ_hom_assoc, CategoryTheory.Pseudofunctor.mapβ_whisker_right_app_assoc, CategoryTheory.Pseudofunctor.StrongTrans.Modification.naturality_assoc, CategoryTheory.Lax.LaxTrans.naturality_naturality_assoc, rightUnitor_naturality, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'βββ_inv_assoc, CategoryTheory.Lax.StrongTrans.naturality_comp, CategoryTheory.Lax.OplaxTrans.naturality_id_assoc, CategoryTheory.Pseudofunctor.mapβ_whisker_right, whiskerRight_id_assoc, whisker_assoc_symm_assoc, conjugateEquiv_apply', CategoryTheory.OplaxFunctor.mapComp_assoc_right_assoc, CategoryTheory.LaxFunctor.mapβ_leftUnitor, CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_as_app, CategoryTheory.Lax.StrongTrans.naturality_naturality, pentagon_hom_inv_inv_inv_hom_assoc, CategoryTheory.Oplax.OplaxTrans.naturality_naturality, CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'_inv, CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_comp_naturality_inv, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'βββ_inv_assoc, Mathlib.Tactic.Bicategory.evalWhiskerRight_nil, CategoryTheory.OplaxFunctor.mapComp_naturality_left_assoc, pentagon_hom_inv_inv_inv_inv_assoc, CategoryTheory.Lax.StrongTrans.vComp_naturality_inv, CategoryTheory.LaxFunctor.mapComp_assoc_right_assoc, CategoryTheory.Oplax.StrongTrans.vcomp_naturality_hom, CategoryTheory.Oplax.OplaxTrans.naturality_naturality_assoc, CategoryTheory.Pseudofunctor.mapβ_associator, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_assoc, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerRight_naturality_assoc, eqToHom_whiskerRight, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_assoc, CategoryTheory.OplaxFunctor.mapComp'_comp_whiskerLeft_mapComp', lanLiftUnit_desc, whisker_assoc, CategoryTheory.Lax.OplaxTrans.naturality_id, LeftExtension.whisker_unit, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_assoc, CategoryTheory.Oplax.StrongTrans.Modification.naturality, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom, CategoryTheory.Oplax.OplaxTrans.naturality_comp_assoc, whiskerLeft_hom_inv_whiskerRight, CategoryTheory.Pseudofunctor.mapComp'βββ_inv_comp_mapComp'βββ_hom, CategoryTheory.Lax.LaxTrans.vComp_naturality_comp, whiskerLeft_hom_inv_whiskerRight_assoc, CategoryTheory.Pseudofunctor.mapComp_id_left_hom, CategoryTheory.Oplax.LaxTrans.naturality_id_assoc, CategoryTheory.Oplax.StrongTrans.Modification.whiskerLeft_naturality_assoc, whiskerRight_isIso, rightUnitor_inv_naturality_assoc, Comonad.comul_assoc_assoc, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_assoc, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_assoc, CategoryTheory.Oplax.LaxTrans.vComp_naturality_naturality, associator_naturality_left, CategoryTheory.LaxFunctor.mapComp_assoc_left, Comonad.counit_comul, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_assoc, CategoryTheory.LaxFunctor.mapComp_assoc_right, LeftExtension.whiskerHom_right, CategoryTheory.Oplax.StrongTrans.naturality_naturality, pentagon_hom_hom_inv_inv_hom, CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_assoc, CategoryTheory.Lax.OplaxTrans.naturality_comp_assoc, CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id, CategoryTheory.LaxFunctor.mapComp_naturality_left_app, pentagon_inv_inv_hom_hom_inv_assoc, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp, CategoryTheory.OplaxFunctor.mapComp_id_left_assoc, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_assoc, CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_comp_assoc, Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of, Adjunction.homEquivβ_symm_apply, CategoryTheory.Oplax.StrongTrans.Modification.whiskerRight_naturality_assoc, CategoryTheory.Pseudofunctor.mapβ_whisker_right_app, CategoryTheory.Oplax.OplaxTrans.Modification.whiskerLeft_naturality, conjugateEquiv_symm_apply', CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_assoc, pentagon_hom_inv_inv_inv_inv, CategoryTheory.OplaxFunctor.mapComp_naturality_left_app_assoc, CategoryTheory.Cat.whiskerRight_app, conjugateEquiv_whiskerLeft, CategoryTheory.OplaxFunctor.mapComp'_comp_mapComp'_whiskerRight_assoc, Mathlib.Tactic.Bicategory.structuralIsoOfExpr_whiskerRight, leftUnitor_comp, CategoryTheory.Lax.OplaxTrans.vComp_naturality_id, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id, CategoryTheory.LaxFunctor.mapComp_naturality_left, CategoryTheory.LaxFunctor.mapComp_assoc_left_assoc, CategoryTheory.Pseudofunctor.mapβ_whisker_right_assoc, CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_assoc, pentagon_hom_hom_inv_hom_hom, triangle_assoc_comp_left_inv, CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerRight_naturality, CategoryTheory.Oplax.OplaxTrans.Modification.naturality, CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_inv, leftUnitor_comp_inv_assoc, leftUnitor_whiskerRight_assoc, rightUnitor_hom_congr, CategoryTheory.OplaxFunctor.mapComp'_comp_whiskerLeft_mapComp'_assoc, pentagon_hom_inv_inv_inv_hom, associator_inv_naturality_middle_assoc, CategoryTheory.Lax.OplaxTrans.naturality_naturality_assoc, CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'βββ_inv, CategoryTheory.Pseudofunctor.mapComp'_hom_comp_mapComp'_hom_whiskerRight, RightLift.w, triangle_assoc, CategoryTheory.Pseudofunctor.mapComp'βββ_hom_comp_mapComp'_hom_whiskerRight, CategoryTheory.Oplax.StrongTrans.vcomp_naturality_inv, Bicategory.Opposite.bicategory_whiskerLeft_unop2, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv, CategoryTheory.Oplax.OplaxTrans.whiskerRight_as_app, associator_naturality_middle_assoc, CategoryTheory.LaxFunctor.mapβ_leftUnitor_hom, mateEquiv_apply', CategoryTheory.OplaxFunctor.mapComp_id_left, postcomp_map, triangle_assoc_comp_right_assoc, pentagon_inv_hom_hom_hom_inv_assoc, leftUnitor_comp_assoc, LeftLift.w, CategoryTheory.LaxFunctor.mapComp_naturality_left_assoc, triangle_assoc_comp_left_inv_assoc, CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerRight_naturality_assoc
|
whiskerRightIso π | CompOp | 15 mathmath: whiskerRightIso_hom, CategoryTheory.Pseudofunctor.mapComp_id_left, Mathlib.Tactic.Bicategory.naturality_whiskerRight, CategoryTheory.Pseudofunctor.isoMapOfCommSq_horiz_id, whiskerRightIso_inv, CategoryTheory.Pseudofunctor.isoMapOfCommSq_vert_id, CategoryTheory.Oplax.StrongTrans.categoryStruct_comp_naturality, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_iso, CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_iso, CategoryTheory.BicategoricalCoherence.whiskerRight_iso, CategoryTheory.Pseudofunctor.mapComp'_id_comp, CategoryTheory.Lax.StrongTrans.categoryStruct_comp_naturality, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_iso, Mathlib.Tactic.Bicategory.structuralIsoOfExpr_whiskerRight, CategoryTheory.Pseudofunctor.whiskerRightIso_mapId
|
Β«term_β·_Β» π | CompOp | β |
Β«term_β_Β» π | CompOp | β |
Β«termΞ»_Β» π | CompOp | β |