Lemma istrans_monorel (c : C) : istrans (monorel c). Proof. intros x y z h1. apply hinhuniv; intros h2; generalize h1; clear h1. apply hinhuniv; intros h1; apply hinhpr. exists (pr1 h1 · pr1 h2). now rewrite <- assoc, <- (pr2 h2), <- (pr2 h1). 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.