Definition make_global_element_functor_precat (F : functor C D) (ge : ∏ c : C, global_element TD (F c)) (ge_compat : ∏ (c c' : C) (f: c --> c'), ge c · #F f = ge c') : global_element Terminal_functor_precat F. Proof. use make_nat_trans. - exact ge. - abstract (intros c c' f; cbn; rewrite ge_compat; apply id_left). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Monics.