Lemma contr_cat_hom_weq : ∏ a b : ob C, (a --> b) ≃ (contr_cat_center C --> contr_cat_center C). Proof. intros a b. pose (aeqcenter := iscontr_uniqueness (contr_cat_iscontr C) a). pose (beqcenter := iscontr_uniqueness (contr_cat_iscontr C) b). use weq_iso. - intros cab. pose (tocenter := transportf (λ x, C ⟦ a, x ⟧) beqcenter cab). exact (transportf (λ x, C ⟦ x, contr_cat_center C ⟧) aeqcenter tocenter). - intros ccc. pose (froma := transportf (λ x, C ⟦ x, contr_cat_center C ⟧) (!aeqcenter) ccc). exact (transportf (λ x, C ⟦ a, x ⟧) (!beqcenter) froma). - intros x; cbn. abstract (rewrite (transport_f_f _ (aeqcenter) (! aeqcenter)); rewrite pathsinv0r; cbn; unfold idfun; rewrite (transport_f_f _ (beqcenter) (! beqcenter)); rewrite pathsinv0r; cbn; unfold idfun; reflexivity). - intros x; cbn. abstract (rewrite (transport_f_f _ (! beqcenter) (beqcenter)); rewrite pathsinv0l; cbn; unfold idfun; rewrite (transport_f_f _ (! aeqcenter) (aeqcenter)); rewrite pathsinv0l; cbn; unfold idfun; reflexivity). 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.