module mset [g] open multi as m abstract sig Idx { f : one g } // fact { some Idx } // binary relation representation fun get[] : Idx -> one g { f } /** multiple ways to `initialize` a mset * 1. by stating the multiplicity of each element * 2. is isomorphic to another mset * 3. is lifted from an ordinary set. */ // multiplicity Of element pred moe[e: g, n: Int] { #(f:>e) = n } // is isomorphic to another family pred isomorphicTo[ family: univ -> one univ ] { let I = family.idx | some r: I->Idx | bijection[r, I, Idx] && r.f = family } // lift from an ordinary set pred liftedFrom[ s: univ ] { Idx.f = s && #Idx = #s } // this family is a multi-join result from fam and span] pred composedFrom[fami: univ -> one univ, span: univ -> univ -> g ] { let I = fami.idx, sLeg = span.sleg, tLeg = span.tleg, Hd = span.head | some p1: Idx->I, p2: Idx-> Hd | pullback[I, Hd, fami, sLeg, Idx, p1, p2] && f = p2.tLeg }