Skip to content

Instantly share code, notes, and snippets.

@kencoba

kencoba/projective_object.als

Created May 12, 2011 01:15
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save kencoba/967745 to your computer and use it in GitHub Desktop.
Save kencoba/967745 to your computer and use it in GitHub Desktop.
Download ZIP
// P is projective object if there is some arrow f_bar such that e o f_bar = f.
Raw
projective_object.als
open util/relation
sig P {
f : one X,
f_bar : one E
}
sig E {
e : one X
}
sig X {}
// e:E->>X
fact {
surjective[e,X]
}
// P is projective object if there is some arrow f_bar such that e o f_bar = f.
pred projective_object {
f_bar.e = f
}
run projective_object
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment