Definition Under_mor_eq {X Y : Under_ob} (M : Under_mor X Y) : Under_ob_mor X · Under_mor_mor M = Under_ob_mor Y := pr2 M.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors.