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