Definition translation_groupoid_precat {CC : contr_cat} (F : contr_cat_action CC hset_category) : precategory. Proof. pose (center := contr_cat_center CC). use make_precategory_one_assoc. - use make_precategory_data. + use make_precategory_ob_mor. * exact (pr1 (F center)). * intros x1 x2; exact (∑ c : CC ⟦center, center⟧, # F c x1 = x2). + intros c; exists (identity center). refine (@eqtohomot _ _ (# F (identity center)) (idfun _) _ c). apply (functor_id F center). + intros a b c f g. cbn in *. exists (pr1 f · pr1 g). refine (maponpaths (λ z, z _) (functor_comp F (pr1 f) (pr1 g)) @ _); cbn. refine (maponpaths _ (pr2 f) @ _). exact (pr2 g). - use make_dirprod. + use make_dirprod; intros ? ? ?; apply subtypePath; try (intro; apply setproperty). * apply id_left. * apply id_right. + cbn. intros a b c d f g h. apply subtypePath; [intro; apply setproperty | ]. apply assoc. 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.