RFC: BundledSet

Stream: general

[Yury G. Kudryashov]

In #6442, I define BundledSet as I suggested in #2202 and migrate docs#Flag and docs#Subsemigroup to BundledSets. Before migrating more files (and adding missing features), I would like to get some feedback: if this is not going to be merged, then I would prefer not to waste my time on the refactor.

[Yury G. Kudryashov]

The main change is that instead of a bunch of custom structures I define

structure BundledSet (α : Type _) (p : Set α → Prop) where
  carrier : Set α
  prop : p carrier

This way we can generalize lots of boilerplate code to BundledSet.

[Yury G. Kudryashov]

I already generalized the construction of a CompleteLattice suitable for algebraic subobjects and *.closure. Other generalizations I have in mind:

• *.eqLocus;
• optional: *.ker
• prod, pi
• map/comap with a GaloisConnection;
  • if we migrate bundled homs to a common data type, then we can also have map_id, map_map etc.

[Kevin Buzzard]

I think it's worth experimenting with this, for sure

[Oliver Nash]

Should the type of p above be p : Set α → Prop rather than p : α → Prop?

[Yury G. Kudryashov]

Oliver Nash said:

Should the type of p above be p : Set α → Prop rather than p : α → Prop?

Yes, it was a typo.

[Jireh Loreaux]

@Yury G. Kudryashov can you document any potential downsides you see for #6442? And how dependent / independent are these changes from #2202, as I believe that RFC still has some pending issues that would probably want resolving?

[Yury G. Kudryashov]

Potential downsides

• If we use generic BundledSet.closure etc, then one can see something like BundledSet M IsSubsemigroup in the info view. I guess, this can be fixed by some meta programming.
• As in #2202, you have to write {carrier := s, prop := { mul_mem := _, one_mem := _}} instead of carrier := s, mul_mem' := _, one_mem' := _.