Definition strict_initial_z_iso {C : category} (I : strict_initial_object C) (I' : Initial C) (f : z_iso I I') : is_strict_initial I'. Proof. intros x g. pose (H := is_strict_initial_strict_initial I x (g · inv_from_z_iso f)). pose (h := (_ ,, H) : z_iso x I). use make_is_z_isomorphism. - exact (inv_from_z_iso f · inv_from_z_iso h). - split. + abstract (rewrite !assoc ; exact (z_iso_inv_after_z_iso h)). + abstract (apply InitialArrowEq). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodColimits. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Preservation.