Correcting an incorrect definition of discrete relations and discrete graphs

[EgbertRijke]

This PR corrects an incorrect definition.

[EgbertRijke]

Maybe an even more correct definition of discrete directed graph is that it is (0 -> 1)-null. This is a proposition again.

[EgbertRijke]

Maybe an even more correct definition of discrete directed graph is that it is (0 -> 1)-null. This is a proposition again.

Nevermind, if a graph is (0 -> 1)-null then the type of vertices for which there exists an outgoing edge is a set. That is too restrictive.

[EgbertRijke]

I think the definition in this pull request is the way to go.

[fredrik-bakke]

I'm confused by why discreteness can't be a property, and I'm too tired to think at the moment, but thanks for fixing the definitions. I'll complete a review when I've rested :)

[EgbertRijke]

I'm confused by why discreteness can't be a property, and I'm too tired to think at the moment, but thanks for fixing the definitions. I'll complete a review when I've rested :)

For reflexive graphs it is still a property. For directed graphs, the notion of discreteness that was implemented included some examples of directed graphs that are typically not considered to be discrete, since they are not reflexive. One example is given in the idea text. The simplest solution is to add the condition that directed graphs must be reflexive. However, this is structure.

Rest well!

[EgbertRijke]

It appears that I still had it wrong: A directed graph should be discrete if its edge relation is empty. This makes it so that the inclusion of discrete directed graphs is left adjoint to the forgetful functor (V , E) |-> V from directed graphs to types. Correcting it now.