Proposition from_stable_inverses : is_inverse_in_precat from_stable_mor from_stable_inv. Proof. unfold from_stable_mor, from_stable_inv. split. - use (MorphismsIntoPullbackEqual (isPullback_Pullback Hpb)). + rewrite !assoc'. rewrite (PullbackArrow_PullbackPr1 Hpb). rewrite PullbackArrow_PullbackPr1. rewrite id_left. apply idpath. + rewrite !assoc'. rewrite (PullbackArrow_PullbackPr2 Hpb). rewrite PullbackArrow_PullbackPr2. rewrite id_left. apply idpath. - use (MorphismsIntoPullbackEqual (isPullback_Pullback _)). + rewrite !assoc'. rewrite PullbackArrow_PullbackPr1. rewrite (PullbackArrow_PullbackPr1 Hpb). rewrite id_left. apply idpath. + rewrite !assoc'. rewrite PullbackArrow_PullbackPr2. rewrite (PullbackArrow_PullbackPr2 Hpb). rewrite id_left. apply idpath. 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.