proposition: 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: Proof. induction p. cbn. apply id_left. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Univalence UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Univalence