# Library Exercise_4_2_1_16

Require Import Utf8.
Require Import ProofIrrelevance.
Require Import Notations PreOrderCategory CategoryIsomorphisms Orders.

Set Implicit Arguments.

Generalizable All Variables.

# Exercise 4.2.1.16

## Problem

Every linear order is a partial order with a special property. Can you phrase this property in terms of hom-sets?

### Real Solution

Local Open Scope category_scope.

Context `(PreOrder X R).

Let C := PreOrderCategory (R := R) _.

Class CategoryConnected obj (C : @Category obj) :=
{ category_connected :> x y,
inhabited ((Morphism C x y) (Morphism C y x)) }.

Local Infix "≤" := R.

Global Instance LinearOrderCategory_is_LinearOrder `(CategoryConnected _ C)
: LinearOrder R.
Proof.
constructor; try solve [ firstorder ].
intros ? ? ? f g.
exact (Compose (C := C) g f).
Defined.

Global Instance LinearOrder_is_LinearOrderCategory `(H0 : LinearOrder X R)
: CategoryConnected C.
Proof.
constructor.
intros x y.
destruct ((_ : Comparable R) x y);
compute;
intuition.
Qed.
End Exercise_4_2_1_16.