Lemma eq_in_sub_precategory2 (C : precategory)(C':sub_precategories C) (a b : sub_ob C') (f g : a --> b) (pf : sub_precategory_predicate_morphisms C' _ _ f) (pg : sub_precategory_predicate_morphisms C' _ _ g): f = g -> (tpair (λ f, sub_precategory_predicate_morphisms _ _ _ f) f pf) = (tpair (λ f, sub_precategory_predicate_morphisms _ _ _ f) g pg).
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos.