Library Exercise_4_2_1_13


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

Set Implicit Arguments.

Generalizable All Variables.


Exercise 4.2.1.13

Problem

We have seen that a preorder can be considered as a category P. Recall from Definition 3.4.1.1 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.
  Proof.
    compute;
    intros x x0; split;
    try solve [ intros; subst; intuition ].
    intros [f g].
    eapply iso_implies_id.
     f.
     g;
      abstract (
          simpl;
          apply ProofIrrelevance.proof_irrelevance
        ).
  Defined.

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