How can I glue/identify inclusions in two structures in MMT?

I'd like to formalize formal languages and their semantics in MMT and define a general notion of semantics equivalence of two semantics wrt. one syntax. Precisely, encoding the latter turns out to be an identification/glueing that I have no idea on how to do in MMT. Let me elaborate on my concrete formalization setup next.

Below is a simplified formalization showing my approach. Based on a theory Meta aggregating both the logical framework LF and some logic, I start in Syntax defining a general notion of expressions and typings. Then, in Semantics I define on top a semantics, here for simplicity, only a deductive semantics, i.e. a derivability relation.

theory Meta : http://cds.omdoc.org/urtheories?LF=  
  // some logic giving us a type `prop` of propositions,
  // a notion of derivability ⊦, biimplication ⇔ etc. ❙
  include ?Logic ❙
❙

theory Syntax : ?Meta =
  // type for expressions ❙
  expr: type ❙

  // a typing relation
  typing_rel: expr ⟶ expr ⟶ prop ❙

  // ... ❙
❚

theory Semantics : ?Meta=
  include ?Syntax ❙

  // a deductive semantics: "derivable e" says e is a theorem ❙
  derivable: expr ⟶ prop ❙
❚

Given this, I want to define the equivalence of two such semantics wrt. to one syntax. Encoding the first part is easy, see below; but I am having trouble encoding the latter requirement.

theory SemanticsEquivalence : ?Meta =
  structure syn : ?Syntax ❚

  // how can I force sem1|?Syntax = sem2|?Syntax = syn ❙
  structure sem1 : ?Semantics = ❚
  structure sem2 : ?Semantics = ❚

  is_equivalent: {e: syn/expr} ⊦ (sem1/derivable e) ⇔ (sem2/derivable e) ❙
❚

How do I glue/identify the inclusions of Syntax in both sem1 and sem2?

Solution

Use defined inclusions within the structures:

theory SemanticsEquivalence : ?Meta =
  structure syn : ?Syntax = ❚
    
  structure sem1 : ?Semantics =
    include ?Syntax ❘ = ?SemanticsEquivalence?syn ❙
  ❚
  structure sem2 : ?Semantics =
    include ?Syntax ❘ = ?SemanticsEquivalence?syn ❙
  ❚

  is_equivalent: {e: syn/expr} ⊦ (sem1/derivable e) ⇔ (sem2/derivable e) ❙
❚

Explanation

The theory of why this works is much deeper than the code above might suggest. It requires understanding the three aspects elaborated on below. I aggregated this information from the official MMT docs on implicit morphisms, structures, and includes and from personal communication with @Dennis Müller.

1. Structures induce theory morphisms

   For example, structure syn : ?Syntax = ❚ within the theory SemanticsEquivalence has two effects: first, it copies every declaration Syntax?d to a declaration SemanticsEquivalence?syn/d where syn/d is just a "complex" name for the copy. Second, the structure also induces a theory morphism Syntax -> SemanticsEquivalence that maps every declaration Syntax?d to the copy SemanticsEquivalence?syn/d.

   This behavior of structures might look a bit simplistic here, but that's only because the structure syn has an empty body. If you had instead

   theory SemanticsEquivalence : ?Meta =
     otherExpr: type ❙
     structure syn : ?Syntax =
       expr = otherExpr ❙
     ❚
   ❚
   

   then the induced theory morphism would contain the mappings Syntax?expr := SemanticsEquivalence?otherExpr, Syntax?typing_rel := SemanticsEquivalence?syn/typing_rel, i.e. only Syntax?typing_rel got copied.

2. Inclusions induce theory morphisms, too

   For example, with theory Semantics = include ?Syntax ❙ ... ❚ the inclusion of Syntax within Semantics has similar effects as structures with empty body: every declaration Syntax?d is accessible within Semantics under the same URI (thus in some sense a copy), and there is an induced morphism — an implicit one even — Syntax -> Semantics that maps every declaration identity-like: Syntax?d := Syntax?d.

3. Inclusions, as declarations, may also have a definition

   Let us consider this by means of an example. Consider we had a morphism m: Syntax -> Semantics' where theory Semantics' = include ?Syntax ❘ = m ❙ ... ❚. Now, the inclusion of Syntax no longer induces the trivial identity-like morphism, but instead takes m. For instance, if the ... part mentions a declaration Syntax?d, actually m(Syntax?d) is taken.

   Let us mix this insight with the previous ones. Consider the following code:

   theory SemanticsEquivalence : ?Meta =
     structure syn : ?Syntax = ❚
   
     structure sem1 : ?Semantics =
       include ?Syntax ❘ = ?SemanticsEquivalence?syn
     ❚
   
     // other structure... ❙
   ❚
   

   By the first insight, syn induces a morphism Syntax -> SemanticsEquivalence, which is accessible via ?SemanticsEquivalence?syn. Moreover, by the first and second insights, we know that the inclusion of Syntax within the structure is a special kind of morphism, namely Syntax -> SemanticsEquivalence — note the codomain! Finally, by the third insight, we can define that inclusion with a fitting morphism, namely with ?SemanticsEquivalence?syn. And this achieves precisely the gluing we wanted.