@Filip #42 that is a really interesting experiment! I am no expert of coq, so what I say may be completely meaningless. But, could you use some of the typeclasses from the standard library for preorders, posets and ordered sets? I think the definiti…
The web, where the objects are the web pages and the relation is given by ‘links to’, seems to me a preorder as we cannot avoid cycles, thus invalidating antisymmetry. If we try to generate a partial order from it, do you know if we get just a set w…
Chapter 1, page 7: In Definition 1.8, right before the exercise, the notation used is \(a_1, a_2\) but becomes \(a, b\) by the end of the sentence
Chapter 1, page 9: Remark 1.16, the surjective function is showing a double headed arrow for the fi…