proposition: Lemma contr_cat_hom_weq : ∏ a b : ob C, (a --> b) ≃ (contr_cat_center C --> contr_cat_center C).
proof: 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.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.PartA UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.catiso UniMath.CategoryTheory.Additive UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.Categories.HSET.Core