def1.v

Definition Domain (A : Type) := A → Prop.

Axiom Domain_irrelevance :
  ∀ {A : Type} (P : Domain A) (x : A) (H1 H2 : P x), H1 = H2.

Program Definition Par : Category := {|
  obj     := Type;
  hom     := fun A B => { D : Domain A & ∀ x : A, D x → B };
  homset  := fun P Q => {|
    equiv := fun '(Df; f) '(Dg; g) =>
      ∀ x (df : Df x) (dg : Dg x), f x df = g x dg
  |};
  id      := λ _, (λ _, True; λ x _, x);
  compose := fun _ _ _ '(Df; f) '(Dg; g) => _
|}.
Next Obligation.
  equivalence; subst.
  - now pose proof (Domain_irrelevance _ _ df dg); subst.
  - (* stuck, missing D for the transitive term *)

def2.v

Import EqNotations.

Program Definition Par : Category := {|
  obj     := Type;
  hom     := fun A B => { D : Ensemble A & ∀ x : A, D x → B };
  homset  := fun _ _ => {|
    equiv := fun '(Df; f) '(Dg; g) =>
      { S : Same_set _ Df Dg
      | ∀ x (df : Df x),
          f x df = g x (rew (Extensionality_Ensembles _ _ _ S) in df) }
  |};
  id      := λ _, (λ _, True; λ x _, x);
  compose := fun _ _ _ '(Df; f) '(Dg; g) => _
|}.

def3.v

Import EqNotations.

Program Definition Par : Category := {|
  obj     := obj[Sets];
  hom     := fun A B => ∃ D : obj[Sets], D ~> A × B;
  homset  := fun _ _ => {|
    equiv := fun '(Df; f) '(Dg; g) => ∀ iso : Df ≅ Dg, f ≈ g ∘ iso
  |};
  id      := λ A, (A; {| morphism := λ x : A, _ |});
  compose := fun _ _ _ '(Df; f) '(Dg; g) => _
|}.