proposition: Lemma are_z_isomorphic_monorel {c : C} {x1 y1 x2 y2 : Subobjectscategory c} (h1 : are_z_isomorphic x1 y1) (h2 : are_z_isomorphic x2 y2) : monorel c x1 x2 → monorel c y1 y2.
proof: Proof. apply hinhuniv; intros f. change (ishinh_UU (z_iso x1 y1)) in h1. change (ishinh_UU (z_iso x2 y2)) in h2. apply h1; clear h1; intro h1. apply h2; clear h2; intro h2. intros P H; apply H; clear P H. set (h1_inv := inv_from_z_iso h1). set (Hh1 := z_iso_after_z_iso_inv h1). exists (pr1 (pr1 h1_inv) · pr1 f · pr1 (pr1 (pr1 h2))). set (Htemp := maponpaths pr1 (pr2 (pr1 h2))). apply pathsinv0; simpl in *. rewrite <-!assoc, <- Htemp. intermediate_path (pr1 (pr1 h1_inv) · pr1 (pr2 x1)). { apply maponpaths, pathsinv0, (pr2 f). } etrans; [ apply maponpaths, (maponpaths pr1 (pr2 (pr1 h1))) |]; simpl. rewrite assoc. etrans; [ eapply cancel_postcomposition, (maponpaths pr1 (maponpaths pr1 Hh1)) |]. apply id_left. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.slicecat UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Subcategory.Core UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.opp_precat