Lemma maponpaths_isotoid (a b : C) (i : z_iso a b) : maponpaths (functor_on_objects F) (isotoid _ HC i) = isotoid _ HD (functor_on_z_iso F i). Proof. apply (invmaponpathsweq (make_weq (idtoiso) (HD _ _ ))). simpl. rewrite maponpaths_idtoiso. repeat 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.