Library UniMath.CategoryTheory.CategoriesWithBinOps

Precategories such that spaces of morphisms have a binary operation

Definition of precategories such that homs are binops.
Gives the binop of the homs from x to y.
  Definition to_binop {BC : precategoryWithBinOps} (x y : BC) : binop (BCx, y) := (pr2 BC) x y.

  Lemma to_binop_eq {BC : precategoryWithBinOps} {x y : BC} {f1 f2 g1 g2 : x --> y}
        (e1 : f1 = f2) (e2 : g1 = g2) : to_binop _ _ f1 g1 = to_binop _ _ f2 g2.
  Proof.
    induction e1, e2. apply idpath.
  Qed.

End def_precategory_with_binops.

Definition oppositePrecategoryWithBinOps (M : precategoryWithBinOps) : precategoryWithBinOps
  := make_precategoryWithBinOps
       (opp_precat M)
       (λ A B f g, @to_binop M (rm_opp_ob B) (rm_opp_ob A) (rm_opp_mor f) (rm_opp_mor g)).

Definition induced_precategoryWithBinOps (M : precategoryWithBinOps) {X:Type} (j : X ob M)
  : precategoryWithBinOps.
Proof.
   (induced_precategory M j). intros a b. exact (@to_binop M (j a) (j b)).
Defined.