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.