Lemma functor_comp_id (A B : precategory) (G : functor A B) (a a' : A) (f : a --> a') (g : a' --> a) : f · g = identity _ -> #G f · #G g = identity _ . Proof. intro e. intermediate_path (#G (identity a )). - rewrite <- e. apply (! functor_comp _ _ _). - apply functor_id_id. apply idpath. Qed.
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.