RDF and Setoids
Libraries developed with Calculus of Inductive Constructions based proof assistants (such as Coq, Agda, ...) prefer to work with Setoids over Sets (Why? See StackExchange).
Setoids are just Sets equipped with an Equivalence Relation. They are available in the Agda Standard Library and as a Setoid Category in the Agda Categories library.
Say we want to model RDF in Agda. One could model the core of RDF as Functor from the small category G_3
of two objects A
and N
and three arrows s, p, o: A \to N
to either Set or Setoids. Which should one choose?
A Functor to Set (available as a Category in Agda) would arguably be closer to the RDF Semantics spec which is specified in terms of Sets.
But it depends on what one is modeling. If the Functor from G_3
to Set models the syntax of RDF then we seem to be missing the semantic dimension: namely what the URIs refer to. Can that be taken care of by natural transformations between the Functors?
Or is this where Setoids could come in useful? In a way the Semantics of RDF tell us that two URIs can refer to the same thing, so that they fall in an equivalence class...