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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.slicecat. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Subcategory.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.opp_precat.