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
}