Definition element_to_nattrans {C:category} (X:[C^op,HSET]) (c:C) : c ⇒ X -> Hom1 c --> X. Proof. intros x. unshelve refine (makeNattrans_op _ _). - unfold Hom1; simpl; intros b f. exact (x ⟲ f). - abstract (intros a b f; apply funextsec; intro g; apply arrow_mor_mor_assoc) 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.