Modularity features for structures necessary for nice diagrams & diagram operators

[ComFreek]

• [ ] Allow extending structure domains

  theory Magma = ...
  theory Monoid = include ?Magma ...
  
  theory MagmaHom = {
   structure dom : ?Magma
   ...
  }
  theory MonoidHom = {
   include ?MagmaHom
   structure dom : ?Monoid
   ...
  }

• [ ] Allow assigning the whole codomain to structure symbol in domain:

  theory Magma = ...
  view IdentityMagmaHom : ?MagmaHom -> ?Magma = {
  dom = this // invent syntax for this
  }

  • via API: construct mapping dom = OMIDENT(?Magma) (since dom is a morphism ?Monoid -> ?MonoidHom anyway)
  • via surface syntax: try dom = ?S