Definition setcategory_eq_idtoiso_comp {C : setcategory} {x x' y y' : C} (p p' : x = x') (f : x' --> y) (q q' : y = y') : idtoiso p · f · idtoiso q = idtoiso p' · f · idtoiso q'.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors.