Library Exercise_4_5_1_28

Require Import Utf8.
Require Import Category Coproduct 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_28_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_28_only (x y : X') : (x y)%objectx = y.
    intros [? []]; compute; intros.
    subst; reflexivity.
End Exercise_4_5_1_28.