Formalising categories with setoids à la Hu & Carrette

Category.idr

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)

The {a = b} syntax is for specifying the values of implicit arguments for when Idris gets stuck on inferring them automatically.