Library Exercise_4_2_1_13

Require Import Utf8.
Require Import ProofIrrelevance.
Require Import PreOrderCategory CategoryIsomorphisms.

Set Implicit Arguments.

Generalizable All Variables.



We have seen that a preorder can be considered as a category P. Recall from Definition that a partial order is a preorder with an additional property. Phrase the defining property for preorders in terms of isomorphisms in the category P.

  Local Open Scope category_scope.

  Class IsoImpliesId obj (C : @Category obj) :=
    { iso_implies_id :> x y : C,
                          (x y)%category
                          → x = y }.

  Context `(PreOrder X R).

  Local Infix "≤" := R.

  Global Instance PartialOrderCategory_is_PartialOrder
         `(IsoImpliesId _ (PreOrderCategory (R := R) _))
  : PartialOrder _ R.
    intros x x0; split;
    try solve [ intros; subst; intuition ].
    intros [f g].
    eapply iso_implies_id.
      abstract (
          apply ProofIrrelevance.proof_irrelevance

  Global Instance PartialOrder_is_PartialOrderCategory `(H0 : PartialOrder X eq R)
  : IsoImpliesId (PreOrderCategory (R := R) _).
    intros x y i.
    apply (H0 x y);
      destruct i as [ ? [ ] ];
      compute in *;
End Exercise_4_2_1_13.