Last active
December 2, 2023 04:22
-
-
Save donovancrichton/f136242484881f20191bba1bf582adc7 to your computer and use it in GitHub Desktop.
Formalising categories with setoids à la Hu & Carrette
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Category | |
%default total | |
public export | |
-- Heterogenous binary relations | |
REL : Type -> Type -> Type | |
REL a b = a -> b -> Type | |
-- Homogenous binary relations | |
public export | |
Rel : Type -> Type | |
Rel a = REL a a | |
-- relation p implies relation q | |
public export | |
→ : {a, b : Type} -> REL a b -> REL a b -> Type | |
p `→` q = {x, y : _} -> p x y -> q x y | |
-- A relation is reflexive if all objects can relate | |
-- with themselves. | |
public export | |
Reflexive : {a : Type} -> Rel a -> Type | |
Reflexive r = {x : a} -> x `r` x | |
-- A relation is symmetric if the relation still holds | |
-- if we swap the order. | |
public export | |
Sym : {a, b : Type} -> REL a b -> REL b a -> Type | |
Sym p q = p `→` flip q | |
-- symmetry of homogenous relations | |
public export | |
Symmetric : {a : Type} -> Rel a -> Type | |
Symmetric r = Sym r r | |
-- transitivity of hetrogeneous relations | |
public export | |
Trans : {a, b, c : Type} | |
-> (p : REL a b) -> (q : REL b c) -> REL a c -> Type | |
Trans p q r = {i, j, k : _} -> p i j -> q j k -> r i k | |
-- transitivity of homogenous relations | |
public export | |
Transitive : {a : Type} -> Rel a -> Type | |
Transitive r = Trans r r r | |
public export | |
interface IsEquivalence (r : Rel a) where | |
refl : Reflexive r | |
sym : Symmetric r | |
trans : Transitive r | |
public export | |
sym' : (a = b) -> (b = a) | |
sym' Refl = Refl | |
public export | |
trans' : (a = b) -> (b = c) -> (a = c) | |
trans' Refl Refl = Refl | |
public export | |
implementation [equiv] IsEquivalence Equal where | |
refl = Refl | |
sym = sym' | |
trans = trans' | |
public export | |
interface Category (obj : Type) where | |
-- behaviour | |
morphism : (x, y : obj) -> Type | |
compose : {a, b, c : obj} | |
-> morphism b c | |
-> morphism a b | |
-> morphism a c | |
eq : {a, b : obj} | |
-> morphism a b | |
-> morphism a b | |
-> Type | |
id : {a : obj} -> morphism a a | |
-- properties | |
PROP_leftid : {a,b : obj} | |
-> {f : morphism a b} | |
-> eq {a,b} (compose {a,b,c=b} (id {a=b}) f) f | |
PROP_rightid : {a,b : obj} | |
-> {f : morphism a b} | |
-> eq {a,b} (compose {a,b=a,c=b} f (id {a})) f | |
PROP_equiv : {a,b : obj} -> IsEquivalence (eq {a, b}) | |
PROP_CompRespEq : {a,b,c : obj} | |
-> {g,i : morphism b c} | |
-> {f,h : morphism a b} | |
-> eq {a,b} f h -> eq {a=b, b=c} g i | |
-> eq {a,b=c} (compose {a,b,c} g f) | |
(compose {a,b,c} i h) | |
PROP_CompAssoc : {a, b, c, d : obj} | |
-> {f : morphism a b} | |
-> {g : morphism b c} | |
-> {h : morphism c d} | |
-> eq {a, b=d} | |
(compose {a, b=c, c=d} h | |
(compose {a, b, c} g f)) | |
(compose {a, b, c=d} | |
(compose {a=b, b=c, c=d} h g) f) | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
The
{a = b}
syntax is for specifying the values of implicit arguments for when Idris gets stuck on inferring them automatically.