AlBasmala Archive Tags RSS About

Posts tagged "category-theory":

Graphs are to categories as lists are to monoids

Article image

Numbers are the lengths of lists which are the flattenings of trees which are the spannings of graphs. Unlike the first three, graphs have two underlying types of interest –the vertices and the edges– and it is getting to grips with this complexity that we attempt to tackle by considering their ‘algebraic’ counterpart: Categories.

In our exploration of what graphs could possibly be and their relationships to lists are, we shall mechanise, or implement, our claims since there will be many details and it is easy to make mistakes –moreover as a self-learning project, I'd feel more confident to make bold claims when I have a proof assistant checking my work ;-)

Assuming slight familiarity with the Agda programming language, we motivate the need for basic concepts of category theory with the aim of discussing adjunctions with a running example of a detailed construction and proof of a free functor. Moreover, the article contains a host of exercises whose solutions can be found in the literate source file. Raw Agda code can be found here.

Since the read time for this article is more than two hours, excluding the interspersed exercises, it may help to occasionally consult a some reference sheets:

Coming from a background in order theory, I love Galois Connections and so our categorical hammer will not be terminal objects nor limits, but rather adjunctions. As such, everything is an adjunction is an apt slogan for us :-)

-- This file has been extracted from https://alhassy.github.io/PathCat/
-- Type checks with Agda version 2.6.0.

Discovering Heyting Algebra

Article image

We attempt to motivate the structure of a Heyting Algebra by considering ‘inverse problems’.

For example,

What if we decided, for security, to change our protocol from using addition to using minimum. That is, we encode our message \(m\) as \(z = x ↓ m\). Since minimum is not invertible, we decide to send our encoded messages with a ‘context’ \(c\) as a pair \((z, c)\). From this pair, a unique number \(m′\) can be extracted, which is not necessarily the original \(m\). Read on, and perhaps you'll figure out which messages can be communicated 😉

This exploration demonstrates that relative pseudo-complements

In some sense, the pseudo-complement is the “best approximate inverse” to forming meets, minima, intersections.

Along the way we develop a number of the theorems describing the relationships between different structural components of Heyting Algebras; most notably the internalisation of much of its own structure.

The article aims to be self-contained, however it may be helpful to look at this lattice cheat sheet (•̀ᴗ•́)و