Definition contr_cat_functor_data (f : C ⟦ contr_cat_center C, contr_cat_center C ⟧ -> D ⟦ contr_cat_center D, contr_cat_center D ⟧) : functor_data C D. Proof. use make_functor_data. - apply weqcontrcontr; apply contr_cat_iscontr. - intros a b g. apply f. apply (contr_cat_hom_weq a b); assumption. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.Additive. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PreAdditive. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.Categories.HSET.Core.