-- (c) MFES/CSI 2018/19 -- building a product type in Alloy

open RelCalc

sig P { fst : one A , snd : one B}

sig A,B {}

fact {

-- for P to be a product, we need the reflexion property:
    ker[fst] & ker[snd] in iden

-- but this is not enough: we need to have all pairs (a,b) in P:
     A -> B in ~fst.snd
}

run {} for exactly 3 A, exactly 2 B, exactly 6 P -- why exaclty 6?