Lemma idtoiso_functor_precompose {C₁ C₂ : category} (F : C₁ ⟶ C₂) {y : C₂} {x₁ x₂ : C₁} (p : x₁ = x₂) (f : F x₁ --> y) : idtoiso (maponpaths (λ z, F z) (!p)) · f = transportf (λ z, F z --> y) p f. Proof. induction p. cbn. apply id_left. 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.