Redesign bundled morphisms and sets

Draft proposal, see also Zulip

-- Auxiliary classes
class ComposablePred (A B C) (p : (B → C) → Prop) (q : (A → B) → Prop) (r : outParam ((A → C) → Prop)) : Prop where
  comp : ∀ f g, p f → q g → r (f ∘ g)

class WeakerPred (A B) (p q : (A → B) → Prop) : Prop where
  weaker : ∀ f, p f → q f

class IdPred (A) (p : (A → A) → Prop) : Prop where
  id : p id

class InvertiblePred (A B) (p : (A → B) → Prop) (q : outParam ((B → A) → Prop)) : Prop where
  symm : ∀ f g, p f → LeftInverse g f → RightInverse g f → q g

-- hom-specific data
structure IsMulHom [Mul A] [Mul B] (f : A → B) : Prop where
  map_mul : ∀ a b, f (a * b) = f a * f b

instance {A B C} [Mul A] [Mul B] [Mul C] : ComposablePred A B C IsMulHom IsMulHom IsMulHom := sorry
instance {A} [Mul A] : IdPred A IsMulHom

-- generic constructions
structure BundledHom (A B : Type*) (p : (A → B) → Prop) where
  toFun : A → B
  property : p toFun

attribute [coe] BundledHom.toFun

instance : CoeFun (BundledHom A B p) fun _ => A → B := ⟨BundledHom.toFun⟩

structure BundledEmbedding (A B : Type*) (p : (A → B) → Prop) extends BundledHom A B p where
  injective : Injective toFun

instance : CoeFun (BundledEmbedding A B p) fun _ => A → B := ⟨fun f => f.toBundledHom⟩

structure BundledEquiv (A B : Type*) (p : (A → B) → Prop) extends BundledHom A B p where
  invFun : B → A
  left_inv : LeftInverse invFun toFun
  right_inv : RightInverse invFun toFun

def BundledEquiv.toBundledEmbedding := sorry

instance : CoeFun (BundledEquiv A B p) fun _ => A → B := ⟨fun f => f.toBundledEmbedding⟩

def BundledEquiv.symm {A B : Type*} {p : (A → B) → Prop} {q : outParam ((B → A) → Prop)} [InvertiblePred A B p q]
    (e : BundledEquiv A B p) : BundledEquiv B A q := sorry

-- auxiliary abbreviations
abbrev MulHom A B [Mul A] [Mul B] := BundledHom A B IsMulHom
abbrev MulEquiv A B [Mul A] [Mul B] := BundledEquiv A B IsMulHom

lemma map_mul {p : (A → B) → Prop} [WeakerPred A B p IsMulHom] (f : BundledHom A B p) (a b : A) :
    f (a * b) = f a * f b := sorry

Then main "pro" of this approach is that we can use a generic construction to define, e.g., *.comp, *.id, and *.End with pow = iterate. Also, map_mul can be stated for a BundledHom because coercions of BundledEmbeddings and BundledEquivs are unfolded to BundledHoms (with two and three arrows, resp.).

There are a few things I don't know how to do with this approach yet:

• auto upgrade from MulEquiv to MonoidHom; maybe,

class HasProp {p : (A → B) → Prop} (f : BundledHom A B p) (q : (A → B) → Prop) : Prop where
  prop : q f

instead of WeakerPred?

• FunLikes that have other data fields (e.g., Finsupp).
• define a MulHom with nice where syntax instead of

def f : MulHom A B where
  toFun := f
  property := { map_mul := _ }

A similar redesign can be done with SetLike. Then we can have CanMap/CanComap classes (in Prop) that say something like p s → p (f '' s) with p in different universes.

Start with the draft proposal in the issue and review the linked Zulip discussion on bundled morphisms. Evaluate the proposed BundledHom, predicate classes, automatic upgrades, FunLike data fields, where syntax, and the related SetLike redesign; done requires an agreed design rather than an isolated edit.