Proposition is_initial_mor_to_strict_initial {C : category} (I : strict_initial_object C) (x : C) (f : x --> I) : isInitial _ x. Proof. use (iso_to_Initial I). pose (f_iso := f ,, is_strict_initial_strict_initial I x f : z_iso x I). exact (z_iso_inv f_iso). 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.