Definition Hom1 {C:category} (c:C) : [C^op,HSET]. Proof. unshelve refine (makeFunctor_op _ _ _ _). - intro b. exact (Hom C b c). - intros b a f g; simpl. exact (g ∘ f). - abstract (intros b; simpl; apply funextsec; intro g; apply id_left) using _L_. - abstract (intros i j k f g; simpl; apply funextsec; intro h; rewrite <- assoc; reflexivity) using _L_. 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.