arend-lib issues

Prove that strongly dense maps are closed under pullbacks along open maps

This is [Topology.Locale/pullback_sdense](https://github.com/JetBrains/arend-lib/blob/4ea97da483c5bb2e6a22c8d09c03becf17756c7e/src/Topology/Locale.ard#L1182). A proof of this lemma can be found in A constructive “Closed subgroup theorem” for localic groups and groupoids, Peter T. Johnstone, 1989, Lemma 1.9.

valis

help wanted

Prove that open maps of locales are closed under pullbacks

This is [Topology.Locale/pullback_open](https://github.com/JetBrains/arend-lib/blob/4ea97da483c5bb2e6a22c8d09c03becf17756c7e/src/Topology/Locale.ard#L1178). A proof of this theorem can be found in Handbook of Categorical Algebra: Volume 3, Francis Borceux, 1994 (Chapter 1), Theorem 1.6.4.

valis

help wanted

Show that the pullback of regular monomorphisms is their meet in the preorder of regular subojects

This is [Category.Subobj/pullback_regularSubobj-isMeet](https://github.com/JetBrains/arend-lib/blob/4ea97da483c5bb2e6a22c8d09c03becf17756c7e/src/Category/Subobj.ard#L42).

valis

help wanted

Prove that regular monomorphisms are stable under pullbacks

This is [Category.Limit/regularMono_pullback](https://github.com/JetBrains/arend-lib/blob/4ea97da483c5bb2e6a22c8d09c03becf17756c7e/src/Category/Limit.ard#L591). This should be straightforward.

valis

help wanted

Show that the forgetful functor from rings to sets creates limits

This is [Algebra.Ring.Category/CRingBicat.createsLimits](https://github.com/JetBrains/arend-lib/blob/4ea97da483c5bb2e6a22c8d09c03becf17756c7e/src/Algebra/Ring/Category.ard#L210). It is probably better to show that the forgetful functor from any algebraic category to sets creates limits and then transfer this result to rings.

valis

help wanted

Extend `run` meta to support trailing lambdas

1

A common pattern in Arend proofs (apart from `==< equalities >==`) is a sequential invocation of functions and metas. A `run` meta makes these chains comprehensible as can be seen...

TurtlePU

Generalize the definition of Subset

`Subset`s are currently only defined for `Monoid`s: https://github.com/JetBrains/arend-lib/blob/6be71a0b2477906448d873f07277ec3289b31796/src/Algebra/Ring/Localization.ard#L23-L32 while they can be defined for `BaseSet`s. It goes without saying that this is useful in general.

tonyxty