Proposition stable_from_pb_preserves_bincoproduct_inverses : is_inverse_in_precat stable_from_pb_preserves_bincoproduct_mor stable_from_pb_preserves_bincoproduct_inv. Proof. unfold stable_from_pb_preserves_bincoproduct_inv. split. - refine (_ @ maponpaths dom_mor (BinCoproductArrowsEq _ _ _ pb_sum _ (hp · hp_inv) (identity _) _ _)). + rewrite comp_in_cod_fib. apply idpath. + rewrite !assoc. unfold hp, hp_inv, stable_from_pb_preserves_bincoproduct_mor_help. rewrite BinCoproductIn1Commutes. use eq_mor_cod_fib. rewrite comp_in_cod_fib. simpl. unfold stable_from_pb_preserves_bincoproduct_inv. rewrite !assoc'. rewrite BinCoproductIn1Commutes. rewrite !assoc. rewrite z_iso_after_z_iso_inv. rewrite id_left. apply maponpaths. exact (!(id_right _)). + rewrite !assoc. unfold hp, hp_inv, stable_from_pb_preserves_bincoproduct_mor_help. rewrite BinCoproductIn2Commutes. use eq_mor_cod_fib. rewrite comp_in_cod_fib. simpl. unfold stable_from_pb_preserves_bincoproduct_inv. rewrite !assoc'. rewrite BinCoproductIn2Commutes. rewrite !assoc. rewrite z_iso_after_z_iso_inv. rewrite id_left. apply maponpaths. exact (!(id_right _)). - use BinCoproductArrowsEq. + rewrite !assoc. rewrite BinCoproductIn1Commutes. unfold stable_from_pb_preserves_bincoproduct_mor. rewrite !assoc'. etrans. { apply maponpaths. refine (!_). exact (comp_in_cod_fib (BinCoproductIn1 pb_sum) stable_from_pb_preserves_bincoproduct_mor_help). } etrans. { do 2 apply maponpaths. apply BinCoproductIn1Commutes. } cbn. rewrite id_right. rewrite !assoc. etrans. { apply maponpaths_2. exact (z_iso_inv_after_z_iso φa). } apply id_left. + rewrite !assoc. rewrite BinCoproductIn2Commutes. unfold stable_from_pb_preserves_bincoproduct_mor. rewrite !assoc'. etrans. { apply maponpaths. refine (!_). exact (comp_in_cod_fib (BinCoproductIn2 pb_sum) stable_from_pb_preserves_bincoproduct_mor_help). } etrans. { do 2 apply maponpaths. apply BinCoproductIn2Commutes. } cbn. rewrite id_right. rewrite !assoc. etrans. { apply maponpaths_2. exact (z_iso_inv_after_z_iso φb). } apply id_left. Qed.
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.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Preservation. Section FromStable. End FromStable.