Using the the dependently-typed programming language Agda,
we formalise orders, with attention to the theory of Galois Connections,
and showcase it by formalising a few results of the category of algebraic
contexts with relational homomorphisms presented by Jipsen (2012) and Moshier (2013).
We aim to exhibit an internal theory of Galois Connections and Closure operators
where the ambient space need not have a notion of meets (intersections), which
are the usual medium in presenting antisymmetry of partial orders.
Instead we consider `symmetric quotients' as being the relational counterpart of
propositional calculus' primitive connective: equivalence. We argue that it as a more
natural primitive than meet --- especially its connection with certain proof heuristics
regarding posets. Moreover, not only do we constrain ourselves to an unconventional
set of primitive operators, but in fact we discard the familiar setting of relations
and sets in favour of the more general setting of ordered categories with converse
(OCCs) --- in fact, a large portion does not require identities and so semigroupoids
may be used instead. / Thesis / Master of Science (MSc)
| Identifer | oai:union.ndltd.org:mcmaster.ca/oai:macsphere.mcmaster.ca:11375/17276 |
| Date | 06 1900 |
| Creators | Al-hassy, Musa |
| Contributors | Kahl, Wolfram, Computing and Software |
| Source Sets | McMaster University |
| Language | English |
| Detected Language | English |
| Type | Thesis |
Page generated in 0.0159 seconds