diag-ops [skip ci]

UniFormal · Apr 13, 2024 · 7026337 · 7026337
1 parent d4e1202
commit 7026337
Show file tree

Hide file tree

Showing 4 changed files with 190 additions and 119 deletions.
diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/Diagram.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/modules/diagrams/Diagram.scala
@@ -194,10 +194,14 @@ object DiagramConnection {
 
   object Singleton {
     def apply(domTheory: MPath, codTheory: MPath, mor: Term): DiagramConnection = {
-      DiagramConnection(
+      new DiagramConnection(
         DiagramFunctor(Diagram(List(domTheory)), Diagram(List(codTheory)), Map(domTheory -> OMMOD(codTheory))),
-        Map(domTheory -> mor)
-      )
+        Map(domTheory -> mor)) {
+        override def applyTheory(thy: MPath): Term = thy match {
+          case `domTheory` => mor
+          case _ => OMCOMP(OMIDENT(OMMOD(thy)), mor) // i.e., mor domain-restricted to thy
+        }
+      }
     }
 
     def unapply(connection: DiagramConnection): Option[(MPath, MPath, Term)] = connection match {