proposition: Lemma karoubi_functor_iso_is_inverse : is_inverse_in_precat (pr1 (Core.counit_from_right_adjoint (is_right_adjoint_precomposition HD karoubi_envelope_inclusion) P) c) karoubi_functor_iso_inv.
proof: Proof. split. - refine (assoc _ _ _ @ _). apply colim_mor_eq. intro v. refine (assoc _ _ _ @ _). refine (maponpaths (λ x, x · _) (assoc _ _ _) @ _). refine (maponpaths (λ x, x · _ · _) (lan_precomposition_counit_point_colimIn HD _ P c _ _ _) @ _). refine (_ @ !id_right _). refine (!maponpaths (λ x, x · _) (functor_comp P _ _) @ _). use (maponpaths (λ x, #P x · _) _ @ colimInCommutes (lan_colim HD karoubi_envelope_inclusion (pre_comp_functor karoubi_envelope_inclusion P) c) v ((pr1 c ,, tt) ,, (make_karoubi_mor (c := make_karoubi_ob _ (identity _) _) (pr12 c) (id_left _) (pr22 c))) ((pr12 v ,, (pr2 iscontrunit _)) ,, _)); apply karoubi_mor_eq. + exact (pr222 v). + apply idpath. - refine (assoc' _ _ _ @ _). refine (maponpaths _ (lan_precomposition_counit_point_colimIn HD _ P c _ _ _) @ _). refine (!functor_comp _ _ _ @ _). refine (_ @ functor_id P _). apply maponpaths. apply karoubi_mor_eq. exact (pr22 c). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Univalence UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.LeftKanExtension UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Presheaf UniMath.CategoryTheory.Retracts UniMath.CategoryTheory.whiskering UniMath.AlgebraicTheories.FundamentalTheorem.SurjectivePrecomposition