Definition delta_functor (I : UU) (C : category) : C ⟶ (power_category I C). Proof. apply (tpair _ (delta_functor_data I C)). abstract (split; intros x *; apply idpath). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.opp_precat.