Lemma transportf_functor_isotoid' {C₁ C₂ : category} (HC₁ : is_univalent C₁) (F : C₁ ⟶ C₂) {y : C₂} {x₁ x₂ : C₁} (i : z_iso x₁ x₂) (f : y --> F x₁) : transportf (λ z, y --> F z) (isotoid _ HC₁ i) f = f · #F i. Proof. rewrite <- idtoiso_functor_precompose'. rewrite maponpaths_idtoiso. rewrite idtoiso_isotoid. 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.