Library Exercise_4_5_1_28


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

Set Implicit Arguments.

Generalizable All Variables.


Exercise 4.5.1.28

Problem

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 ×.
     x.
    eexists (@eq_refl _ x) (@eq_refl _ x) (fun _ _ mm);
      abstract (
          compute;
          intros;
          apply ProofIrrelevance.proof_irrelevance
        ).
  Defined.
  Lemma Exercise_4_5_1_28_only (x y : X') : (x y)%objectx = y.
    intros [? []]; compute; intros.
    subst; reflexivity.
  Qed.
End Exercise_4_5_1_28.