Please use this identifier to cite or link to this item:
http://hdl.handle.net/11375/17276
Title: | A Mechanisation of Internal Galois Connections In Order Theory Formalised Without Meets |
Authors: | Al-hassy, Musa |
Advisor: | Kahl, Wolfram |
Department: | Computing and Software |
Keywords: | relation algebra, ordered category, converse, order, galois connection |
Publication Date: | Jun-2015 |
Abstract: | 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. |
URI: | http://hdl.handle.net/11375/17276 |
Appears in Collections: | Open Access Dissertations and Theses |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
thesis.pdf | Musa Al-hassy, MSc Thesis, CAS April 2015 | 570.67 kB | Adobe PDF | View/Open |
Items in MacSphere are protected by copyright, with all rights reserved, unless otherwise indicated.