Lemma faithful_reflects_morphism_equality {C D : precategory} (F : functor C D) (FF : faithful F) {a b : ob C} (f g : C ⟦a, b⟧) : # F f = # F g → f = g. Proof. intros feq. apply (Injectivity (# F)). - apply isweqonpathsincl, FF. - exact feq. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Univalence.