I'm working on a theory in which there is a relation C defined as
Parameter Entity: Set.
Parameter C : Entity -> Entity -> Entity -> Prop.
The relation C is a relation of composition of some entities. Instead of C z x y
, I want to be able to write x o y = z
. So I have two questions:
- I think I should define a "function" (the word is perhaps not the right one) named fC that takes x and y and returns z. This way, I could use it in the Notation. But I don't know how to define this "function". Is it possible?
- I find that I can use the command
Notation
to define an operator. Something likeNotation "x o y" := fC x y.
. Is this the good way to do it?
I tried Notation "x o y" := exists u, C u x y.
but it didn't work. Is there a way to do what I want to do?