Lemma iseqrel_are_isomorphic : iseqrel are_isomorphic. Proof. repeat split. - intros x y z h1. apply hinhuniv; intros h2; generalize h1; clear h1. now apply hinhuniv; intros h1; apply hinhpr, (iso_comp h1 h2). - now intros x; apply hinhpr, identity_iso. - now intros x y; apply hinhuniv; intro h1; apply hinhpr, iso_inv_from_iso. Qed.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories.