Library PreOrderCategory

Require Import Utf8.
Require Export Setoid.
Require Export Classes.RelationClasses Morphisms.
Require Import FunctionalExtensionality ProofIrrelevance.
Require Export Category.
Require Import ComputableCategory.

Set Implicit Arguments.

Generalizable All Variables.

PreOrders as Categories

A preorder (X, ≤) consists of a set X and a binary relation that is reflexive and transitive. We can make from (X, ≤) : Ob PrO a category X' : Ob Cat as follows. Define Ob X' = X and for every two objects x y : X define
[Hom_X'(x, y) = if x y then {"x y"} else ∅]
In Coq, we can simply take the set of proofs of x y.
  Section single_preorder.
    Context `(PreOrder X R).

    Local Infix "≤" := R.

    Definition PreOrderCategory : @Category X.
      refine {|
          Morphism := R;
          Identity := reflexivity;
          Compose := (fun x y z A B transitivity B A)
      abstract (intros; apply ProofIrrelevance.proof_irrelevance).
  End single_preorder.

  Section all_preorders.
    Record > PreOrderedSet :=
        PreOrderedSetType :> Type;
        PreOrderedSetRelation :> Relation_Definitions.relation PreOrderedSetType;
        PreOrderedSetPreOrder :> PreOrder PreOrderedSetRelation

    Definition CategoryOfPreOrders
      := @ComputableCategory PreOrderedSet _ (fun XPreOrderCategory X).
  End all_preorders.
End preorder_category.