Library Exercise_4_2_1_14


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

Set Implicit Arguments.

Generalizable All Variables.


Exercise 4.2.1.14

Problem

Suppose that C is a preorder (considered as a category). Let x y : Ob C be objects such that x y and y x. Prove that there is an isomorphism x y in C.

  Local Open Scope category_scope.

  Context `(PreOrder X R).
  Let C := PreOrderCategory (R := R) _.

  Local Infix "≤" := R.

  Lemma Exercise_4_2_1_14 : x y : C, x yy x → (x y)%category.
    intros x y f g.
     f.
     g;
      abstract (
          simpl;
          apply ProofIrrelevance.proof_irrelevance
        ).
  Defined.
End Exercise_4_2_1_14.