StructuredArrow 📖 | CompOp | 321 mathmath: TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_hom_right, LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution_map, TwoSquare.instInitialStructuredArrowObjStructuredArrowDownwardsOfGuitartExact, Limits.Cone.toUnder_pt, StructuredArrow.final_pre, StructuredArrow.projectSubobject_mk, StructuredArrow.instFullUnderToUnder, StructuredArrow.map_map_right, StructuredArrow.ofCommaSndEquivalenceInverse_obj_right_left, StructuredArrow.isoMk_inv_right, TwoSquare.instIsConnectedStructuredArrowCostructuredArrowObjCostructuredArrowRightwardsOfGuitartExact, StructuredArrow.map_comp, StructuredArrow.ofCommaSndEquivalenceFunctor_map_right, Functor.toStructuredArrow_obj, StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_right_right, Limits.limit.toStructuredArrow_obj, StructuredArrow.map_obj_right, StructuredArrow.mapIso_functor_obj_left, CategoryOfElements.fromStructuredArrow_map, StructuredArrow.commaMapEquivalenceInverse_map, StructuredArrow.ofDiagEquivalence.inverse_map_right, TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_left_hom, Profinite.Extend.functorOp_map, StructuredArrow.homMk'_comp, StructuredArrow.ofCommaSndEquivalence_functor, StructuredArrow.final_map, CategoryOfElements.structuredArrowEquivalence_functor, StructuredArrow.hasLimit, TwoSquare.structuredArrowRightwardsOpEquivalence_inverse, StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_right_left_as, StructuredArrow.mapIso_inverse_obj_hom, StructuredArrow.toUnder_obj_left, StructuredArrow.IsUniversal.uniq, Functor.pointwiseRightKanExtension_lift_app, CondensedMod.isDiscrete_tfae, StructuredArrow.map₂_obj_right, StructuredArrow.commaMapEquivalenceCounitIso_hom_app_left_right, Profinite.Extend.cone_π_app, TwoSquare.EquivalenceJ.inverse_map, StructuredArrow.commaMapEquivalenceUnitIso_inv_app_right_right, Functor.RightExtension.coneAt_pt, StructuredArrow.map₂_map_right, TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_right_as, StructuredArrow.preEquivalenceInverse_obj_right_hom, TwoSquare.instIsConnectedCostructuredArrowStructuredArrowObjStructuredArrowDownwardsOfGuitartExact, StructuredArrow.proj_faithful, StructuredArrow.ofDiagEquivalence.functor_obj_right_right, Functor.RightExtension.coneAt_π_app, StructuredArrow.mapNatIso_functor_obj_right, StructuredArrow.eta_hom_right, TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_left_right, Limits.limit.toStructuredArrow_map, TwoSquare.equivalenceJ_unitIso, StructuredArrow.proj_reflectsIsomorphisms, StructuredArrow.prodInverse_map, StructuredArrow.eta_inv_right, Limits.Cone.toStructuredArrowCompProj_inv_app, StructuredArrow.instEssSurjCompPre, StructuredArrow.ofDiagEquivalence.inverse_obj_right, CategoryOfElements.to_comma_map_right, Functor.Final.instNonemptyStructuredArrow, StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_left_as, StructuredArrow.instEssSurjObjCompPostOfFull, TwoSquare.guitartExact_iff_initial, Limits.Cone.fromStructuredArrow_π_app, StructuredArrow.id_right, StructuredArrow.final_map₂_id, StructuredArrow.preEquivalenceFunctor_obj_left_as, StructuredArrow.map₂_obj_left, RepresentablyFlat.cofiltered, StructuredArrow.preEquivalence_unitIso, CategoryOfElements.structuredArrowEquivalence_counitIso, StructuredArrow.functor_map, StructuredArrow.ofCommaSndEquivalence_unitIso, StructuredArrow.map₂_map_left, StructuredArrow.ofCommaSndEquivalence_counitIso, StructuredArrow.isEquivalence_pre, StructuredArrow.prodFunctor_map, Limits.Cone.toStructuredArrowCompToUnderCompForget_hom_app, StructuredArrow.final_post, Functor.Final.out, StructuredArrow.prodEquivalence_functor, StructuredArrow.ofDiagEquivalence.inverse_obj_hom, StructuredArrow.mapNatIso_functor_obj_hom, StructuredArrow.mapIso_inverse_obj_right, StructuredArrow.ofDiagEquivalence.functor_obj_right_hom, StructuredArrow.mapNatIso_inverse_map_right, StructuredArrow.prodEquivalence_unitIso, StructuredArrow.full_map₂, isFiltered_structuredArrow_of_isFiltered_of_exists, StructuredArrow.mapNatIso_functor_map_right, StructuredArrow.ofCommaSndEquivalenceInverse_map_right_left, StructuredArrow.mapNatIso_inverse_obj_left, StructuredArrow.ofDiagEquivalence.functor_map_right_right, TwoSquare.structuredArrowRightwardsOpEquivalence_counitIso, CategoryOfElements.toStructuredArrow_obj, StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_left_as, StructuredArrow.preEquivalence_inverse, StructuredArrow.preEquivalence_functor, CostructuredArrow.toStructuredArrow'_obj, Limits.Cone.fromStructuredArrow_pt, StructuredArrow.homMk'_mk_comp, Limits.Cone.toStructuredArrow_comp_toUnder_comp_forget, StructuredArrow.ofCommaSndEquivalenceFunctor_map_left, TwoSquare.equivalenceJ_counitIso, StructuredArrow.mapNatIso_unitIso_hom_app_right, StructuredArrow.eqToHom_right, Functor.RightExtension.coneAtFunctor_obj, Functor.toStructuredArrow_map, StructuredArrow.instFaithfulObjCompPost, StructuredArrow.small_inverseImage_proj_of_locallySmall, Limits.Cone.toStructuredArrowCone_π_app, StructuredArrow.mono_iff_mono_right, Limits.Cocone.toStructuredArrow_obj, StructuredArrow.epi_homMk, StructuredArrow.isEquivalence_toUnder, StructuredArrow.ofStructuredArrowProjEquivalence.functor_map_right_right, StructuredArrow.ofCommaSndEquivalenceFunctor_obj_right, instFinalStructuredArrowCompPreOfRepresentablyFlat, LightProfinite.Extend.functor_map, Functor.RightExtension.coneAtWhiskerRightIso_inv_hom, CategoryOfElements.fromStructuredArrow_obj, StructuredArrow.ofDiagEquivalence.functor_obj_right_left_as, Limits.Cocone.equivStructuredArrow_unitIso, StructuredArrow.mkPostcomp_comp, StructuredArrow.isoMk_hom_right, TwoSquare.costructuredArrowDownwardsPrecomp_obj, StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_right_hom, StructuredArrow.toCostructuredArrow_map, StructuredArrow.hasLimitsOfShape, Functor.final_iff_isFiltered_structuredArrow, Limits.Cone.mapConeToUnder_inv_hom, StructuredArrow.toUnder_map_right, TwoSquare.equivalenceJ_inverse, StructuredArrow.isEquivalenceMap₂, Limits.Cocone.fromStructuredArrow_obj_pt, StructuredArrow.isEquivalence_post, Functor.ranObjObjIsoLimit_inv_π_assoc, CategoryOfElements.structuredArrowEquivalence_inverse, Profinite.Extend.functor_obj, CostructuredArrow.toStructuredArrow'_map, MorphismProperty.instIsClosedUnderIsomorphismsStructuredArrowStructuredArrowObjOfRespectsIso, StructuredArrow.commaMapEquivalenceInverse_obj, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₂, StructuredArrow.homMk'_id, StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_hom, StructuredArrow.preEquivalenceInverse_obj_right_right, StructuredArrow.preEquivalenceInverse_obj_right_left_as, StructuredArrow.hasLimitsOfSize, StructuredArrow.mapNatIso_inverse_obj_hom, StructuredArrow.commaMapEquivalenceFunctor_obj_left, StructuredArrow.post_map, StructuredArrow.commaMapEquivalenceFunctor_map_left, StructuredArrow.instFaithfulUnderToUnder, ObjectProperty.IsCoseparating.mono_productTo, Functor.ranObjObjIsoLimit_hom_π_assoc, isRightAdjoint_iff_hasInitial_structuredArrow, StructuredArrow.faithful_map₂, StructuredArrow.pre_map_left, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₃, StructuredArrow.map_map_left, TwoSquare.structuredArrowRightwardsOpEquivalence.functor_map_left_right, StructuredArrow.mapIso_functor_obj_right, StructuredArrow.mapIso_unitIso_inv_app_right, StructuredArrow.prodFunctor_obj, LightProfinite.Extend.functorOp_map, StructuredArrow.proj_map, Alexandrov.lowerCone_π_app, Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_inv_π, StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_right_right, StructuredArrow.mapIso_functor_map_left, TopCat.Presheaf.SheafCondition.instNonemptyStructuredArrowPairwiseOpensLeCoverPairwiseToOpensLeCover, StructuredArrow.ofStructuredArrowProjEquivalence.inverse_map_right_right, TwoSquare.structuredArrowRightwardsOpEquivalence_unitIso, StructuredArrow.comp_right, StructuredArrow.commaMapEquivalenceFunctor_map_right, StructuredArrow.essentiallySmall, Limits.Cone.toStructuredArrowCompProj_hom_app, StructuredArrow.map_obj_left, Functor.pointwiseRightKanExtensionCounit_app, StructuredArrow.ofCommaSndEquivalenceInverse_obj_hom, CostructuredArrow.toStructuredArrow_obj, CondensedSet.isDiscrete_tfae, Limits.Cocone.fromStructuredArrow_map_hom, Functor.pointwiseRightKanExtension_obj, StructuredArrow.mapNatIso_counitIso_hom_app_right, TwoSquare.costructuredArrowDownwardsPrecomp_map, LocalizerMorphism.IsRightDerivabilityStructure.Constructor.isConnected, StructuredArrow.toUnder_obj_hom, StructuredArrow.commaMapEquivalenceCounitIso_hom_app_right_right, StructuredArrow.map_mk, Limits.Cone.toStructuredArrow_obj, StructuredArrow.mono_homMk, StructuredArrow.ofCommaSndEquivalenceInverse_map_right_right, instIsCofilteredStructuredArrowCompOfRepresentablyFlat, StructuredArrow.preEquivalenceInverse_map_right_right, Functor.Final.zigzag_of_eqvGen_colimitTypeRel, TwoSquare.EquivalenceJ.functor_obj, TwoSquare.isConnected_rightwards_iff_downwards, StructuredArrow.mapIso_unitIso_hom_app_right, Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_inv_π_assoc, StructuredArrow.commaMapEquivalenceUnitIso_hom_app_right_right, Limits.Cocone.equivStructuredArrow_inverse, StructuredArrow.pre_map_right, StructuredArrow.mapIso_functor_obj_hom, StructuredArrow.mapNatIso_unitIso_inv_app_right, Functor.ranObjObjIsoLimit_hom_π, Alexandrov.projSup_obj, StructuredArrow.instFaithfulCompPre, StructuredArrow.functor_obj, Functor.pointwiseRightKanExtension_map, StructuredArrow.mono_of_mono_right, Functor.RightExtension.coneAtFunctor_map_hom, Alexandrov.lowerCone_pt, Limits.WalkingParallelPair.instIsConnectedStructuredArrowWalkingReflexivePairInclusionWalkingReflexivePair, Functor.RightExtension.coneAtWhiskerRightIso_hom_hom, StructuredArrow.mapIso_inverse_map_right, Profinite.Extend.cone_pt, TwoSquare.structuredArrowDownwards_map, Localization.structuredArrowEquiv_symm_apply, Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_hom_π, StructuredArrow.ofCommaSndEquivalenceFunctor_obj_left, StructuredArrow.ofDiagEquivalence.functor_obj_hom, CategoryOfElements.structuredArrowEquivalence_unitIso, TwoSquare.structuredArrowDownwards_obj, Limits.Cone.toUnder_π_app, StructuredArrow.prodEquivalence_inverse, StructuredArrow.ofDiagEquivalence.inverse_obj_left_as, StructuredArrow.mapNatIso_functor_obj_left, StructuredArrow.commaMapEquivalenceUnitIso_hom_app_right_left, StructuredArrow.preEquivalenceFunctor_map_right, Limits.Cone.toStructuredArrow_comp_proj, SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₁, StructuredArrow.preEquivalenceInverse_obj_hom_right, Limits.Cone.mapConeToUnder_hom_hom, LightProfinite.Extend.functor_initial, Functor.ranObjObjIsoLimit_inv_π, TwoSquare.EquivalenceJ.functor_map, StructuredArrow.mapIso_inverse_obj_left, StructuredArrow.commaMapEquivalenceUnitIso_inv_app_right_left, StructuredArrow.mapIso_functor_map_right, Functor.structuredArrowMapCone_pt, StructuredArrow.ofCommaSndEquivalence_inverse, StructuredArrow.pre_obj_hom, Limits.Cocone.toStructuredArrow_map, TwoSquare.equivalenceJ_functor, StructuredArrow.toUnder_map_left, StructuredArrow.prodInverse_obj, Limits.Cone.toStructuredArrow_map, StructuredArrow.preEquivalence_counitIso, StructuredArrow.preEquivalenceInverse_obj_left_as, LightProfinite.Extend.functor_obj, StructuredArrow.preEquivalenceFunctor_obj_right, StructuredArrow.proj_obj, StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_right_left_as, StructuredArrow.essSurj_map₂, TwoSquare.EquivalenceJ.inverse_obj, StructuredArrow.isCoseparating_proj_preimage, StructuredArrow.map_obj_hom, ObjectProperty.LimitOfShape.toStructuredArrow_obj, StructuredArrow.prodEquivalence_counitIso, StructuredArrow.mapIso_inverse_map_left, StructuredArrow.ofCommaSndEquivalenceInverse_obj_right_hom, StructuredArrow.instEssSurjUnderToUnder, LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution_obj, Limits.Cone.toStructuredArrowCompToUnderCompForget_inv_app, StructuredArrow.map_id, ObjectProperty.LimitOfShape.toStructuredArrow_map, StructuredArrow.locallySmall, Limits.WalkingParallelPair.instNonemptyStructuredArrowWalkingReflexivePairInclusionWalkingReflexivePair, StructuredArrow.instSmallOfLocallySmall, StructuredArrow.instFullCompPre, StructuredArrow.wellPowered_structuredArrow, TwoSquare.guitartExact_iff_isConnected_downwards, StructuredArrow.toCostructuredArrow'_map, StructuredArrow.post_obj, StructuredArrow.toCostructuredArrow'_obj, StructuredArrow.ofCommaSndEquivalenceInverse_obj_left_as, TwoSquare.structuredArrowRightwardsOpEquivalence_functor, Limits.Cocone.equivStructuredArrow_functor, instIsFilteredStructuredArrowProdDiagOfIsFilteredOrEmpty, StructuredArrow.mapNatIso_inverse_map_left, Limits.Cocone.fromStructuredArrow_obj_ι, Profinite.Extend.functor_initial, Limits.Cocone.equivStructuredArrow_counitIso, Limits.Cone.toStructuredArrowCone_pt, Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_hom_π_assoc, StructuredArrow.instFullObjCompPostOfFaithful, StructuredArrow.ofDiagEquivalence.functor_obj_left_as, Profinite.Extend.functor_map, StructuredArrow.toUnder_obj_right, Functor.toStructuredArrow_comp_proj, StructuredArrow.commaMapEquivalenceCounitIso_inv_app_left_right, StructuredArrow.mapNatIso_functor_map_left, StructuredArrow.map₂_obj_hom, StructuredArrow.mapNatIso_counitIso_inv_app_right, StructuredArrow.commaMapEquivalenceFunctor_obj_right, StructuredArrow.isCoseparating_inverseImage_proj, StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_right_hom, CostructuredArrow.toStructuredArrow_map, StructuredArrow.ofCommaSndEquivalenceFunctor_obj_hom, StructuredArrow.homMk'_mk_id, Alexandrov.projSup_map, StructuredArrow.pre_obj_left, StructuredArrow.epi_of_epi_right, TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_left_left_as, StructuredArrow.mkPostcomp_id, StructuredArrow.commaMapEquivalenceCounitIso_inv_app_right_right, StructuredArrow.mapIso_counitIso_hom_app_right, StructuredArrow.toCostructuredArrow_obj, StructuredArrow.final_proj_of_isFiltered, StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_hom, StructuredArrow.mapNatIso_inverse_obj_right, StructuredArrow.ofCommaSndEquivalenceInverse_obj_right_right, StructuredArrow.preEquivalenceFunctor_obj_hom, StructuredArrow.mapIso_counitIso_inv_app_right, StructuredArrow.commaMapEquivalenceFunctor_obj_hom, StructuredArrow.pre_obj_right, StructuredArrow.small_proj_preimage_of_locallySmall, Functor.structuredArrowMapCone_π_app, Localization.structuredArrowEquiv_apply
|