Projective Object

Alloy Category Theory

AwodeyのP33にProjective Objectのお話が載っているのですが。

Alloyで書くとこういうことなのかな。
https://gist.github.com/967745

たけをさんから以下のような例をいただいた。

open util/relation

sig P {
      f : one X
}
sig E {
      e : one X
}
sig X {}

fun f_bar : P -> one E {
 { p: P, eob: E | p->eob.e in f }
}

-- fail
assert f_bar_exists {
 some f => some f_bar
}
check f_bar_exists

-- pass
assert f_bar_exists_if_surjective {
 surjective [e, X] => (some f => some f_bar)
}
check f_bar_exists_if_surjective

ただ、生成公理がからむ場合、Alloyでは圏の例示ができない（破たんする）ケースもあるとのこと。