Library Exercise_4_5_1_14

Require Import Utf8.
Require Import Category Product DiscreteCategory.
Require Import Common Notations.

Set Implicit Arguments.

Generalizable All Variables.



Let X be a set, and consider it as a discrete category. Given two objects x y : Ob X, under what conditions will there exist a product x × y?

  Variable X : Type.

  Let X' := DiscreteCategory X.

  Definition Exercise_4_5_1_14_ex (x : X') : (x × x)%object.
    subst_body; compute in ×.
    eexists (@eq_refl _ x) (@eq_refl _ x) (fun _ _ mm);
      abstract (
          apply ProofIrrelevance.proof_irrelevance
  Lemma Exercise_4_5_1_14_only (x y : X') : (x × y)%objectx = y.
    intros [? []]; compute; intros.
    subst; assumption.
End Exercise_4_5_1_14.