Definition isweqhomot' {X Y} (f g : X -> Y) (H : isweq f) (homot : ∏ x, f x = g x) : isweq g. Proof. apply (isweqhomot f g homot H). Defined.
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.