Definition HomPair {C:category} (a b:C) : [C^op,SET]. Proof. unshelve refine (makeFunctor_op _ _ _ _). - intro c. exact (Hom C c a × Hom C c b) % set. - simpl. intros c d f x. exact (pr1 x ∘ f ,, pr2 x ∘ f). - abstract (simpl; intro c; apply funextsec; intro x; apply dirprodeq; apply id_left) using _B_. - abstract (simpl; intros c d e f g; apply funextsec; intro x; apply dirprodeq; apply pathsinv0, assoc) using _C_. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import Require Import Require Import UniMath.MoreFoundations.Tactics.