Lemma functor_cancel_pw {C C' D D' : precategory} hsD hsD' (F : [C,D,hsD] ⟶ [C',D',hsD']) {a b } (f g : [C,D,hsD] ⟦ a, b ⟧) (x :C') : f = g -> ((# F f ) : nat_trans _ _ ) x = (# F g:nat_trans _ _) x . Proof. intro e. now induction e. Qed.
Require Import UniMath.Foundations.Propositions. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence.