Lemma cats_minimal_homotopical (C : category) : homotopical_category. Proof. unfold homotopical_category. pose (C_Weq := (C ,, (fun x y f => (is_z_isomorphism f ,, isaprop_is_z_isomorphism f))) : category_with_weq ). exists C_Weq. unfold is_homotopical. unfold two_of_six. intros. assert (g_is_iso : is_z_isomorphism g). { assert (g_is_monic : isMonic g). apply (isMonic_postcomp _ g h). simpl in hg. apply (is_iso_isMonic _ _ hg). assert (g_left_inv : ((is_z_isomorphism_mor gf) · f · g) = identity _). rewrite <- assoc. apply (z_iso_after_z_iso_inv (f · g ,, gf)). pose (g_right_inv := left_inv_monic_is_right_inv _ g_is_monic _ g_left_inv). eapply make_is_z_isomorphism. split. apply g_right_inv. apply g_left_inv. } pose (f_is_iso := z_iso_two_of_three_left gf g_is_iso). split. apply f_is_iso. split. apply g_is_iso. split. apply (z_iso_two_of_three_right hg g_is_iso). rewrite <- assoc. apply is_z_isomorphism_comp. apply f_is_iso. apply hg. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos.