Skip to content

Commit

Permalink
add proof that we can interpret a preorder as a category
Browse files Browse the repository at this point in the history
  • Loading branch information
@marcosh
marcosh committed Dec 6, 2018
1 parent 5d269ea commit 5af7cda
Showing 1 changed file with 31 additions and 0 deletions.
31 changes: 31 additions & 0 deletions src/PreorderAsCategory.idr
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
module PreorderAsCategory.idr

import Category

-- contrib
import Decidable.Order

interface Preorder t po => UniquePreorder t (po : t -> t -> Type) where
unique : (a, b : t) -> (f, g : po a b) -> f = g

identity : Preorder t po => (a : t) -> po a a
identity = reflexive

compose : Preorder t po => (a, b, c : t) -> po a b -> po b c -> po a c
compose = transitive

identityLeft : UniquePreorder t po => (a, b : t) -> (f : po a b) -> compose a a b (identity a) f = f
identityLeft a b f = unique a b (compose a a b (identity a) f) f

identityRight : UniquePreorder t po => (a, b : t) -> (f : po a b) -> compose a b b f (identity b) = f
identityRight a b f = unique a b (compose a b b f (identity b)) f

ass : UniquePreorder t po => (a, b, c, d : t) -> (f : po a b) -> (g : po b c) -> (h : po c d) -> transitive a b d f (transitive b c d g h) = transitive a c d (transitive a b c f g) h
ass a b c d f g h = unique a d (transitive a b d f (transitive b c d g h)) (transitive a c d (transitive a b c f g) h)

UniquePreorder t po => Category t po where
identity = identity
compose {a} {b} {c} = compose a b c
identityLeft {a} {b} {f} = identityLeft a b f
identityRight {a} {b} {f} = identityRight a b f
associativity {a} {b} {c} {d} {f} {g} {h} = ass a b c d f g h

2 comments on commit 5af7cda

@wisnesky
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If you want to hook this up to AQL I'd suggest trying to write down this category:

objects
		Employee 
		Department
generating arrows
		manager : Employee -> Employee
		worksIn   : Employee -> Department
		secretary : Department -> Employee
equations
		manager ; worksIn = worksIn
  		secretary ; worksIn = id_Department

@marcosh
Copy link
Contributor Author

@marcosh marcosh commented on 5af7cda Dec 7, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That is definitely a good idea.

Maybe the project is still in an early stage to actually work on this now, I'll open an issue here so that we don't forget about this

Please sign in to comment.