Library ChainCategory


Require Import Utf8.
Require Import ProofIrrelevance.
Require Export Category.
Require Import Subcategory NatFacts.

Set Implicit Arguments.

Generalizable All Variables.

Chain Categories

Section ChainCat.
  Definition OmegaCategory : @Category nat.
    refine (@Build_Category _
                            le
                            le_refl
                            (fun _ _ _ H0 H1le_trans H1 H0)
                            _
                            _
                            _);
    abstract (intros; apply proof_irrelevance).
  Defined.

  Definition ChainCategory' n : @Category { m | m n }
    := Eval hnf in FullSubcategory OmegaCategory (fun mm n).
  Arguments ChainCategory' n / .
  Definition ChainCategory n := Eval simpl in ChainCategory' n.
End ChainCat.

Notation "[ n ]" := (ChainCategory n) : category_scope.
Notation "[ ∞ ]" := (OmegaCategory) : category_scope.
Notation "[ 'ω' ]" := (OmegaCategory) : category_scope.