# 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.