New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Correspondence graphs #1246
Correspondence graphs #1246
Conversation
: arc G → node G | ||
:= pr222 G. | ||
|
||
Definition has_nodeset (G : precgraph) : UU |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It would be nice to put these in hProp
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
However, it becomes less easy to use it I think.
: cgraph_mor G H | ||
:= p₀,, p₁,, h. | ||
|
||
Definition onnode {G H : precgraph} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Definition onnode {G H : precgraph} | |
Definition on_node {G H : precgraph} |
: cgraph_mor G H → node G → node H | ||
:= pr1. | ||
|
||
Definition onarc {G H : precgraph} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Definition onarc {G H : precgraph} | |
Definition on_arc {G H : precgraph} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
These will be presumably used quite often. I think it is better to squeeze as much as possible.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think less abbreviation and more underscores would improve readability, but I like the content.
Co-Authored-By: Langston Barrett <langston.barrett@gmail.com>
Co-Authored-By: Langston Barrett <langston.barrett@gmail.com>
Co-Authored-By: Langston Barrett <langston.barrett@gmail.com>
Co-Authored-By: Langston Barrett <langston.barrett@gmail.com>
@maggesi : apologies for the slow handling of this PR! |
Correspondence graphs
Correspondence graphs
Alternative representation of graphs as a "correspondence" relation (here called CGraphs for short)
E -> V * V
and its categorical structure.
What is missing: