Lemma maponpaths_idtoiso (a b : C) (e : a = b) : idtoiso (maponpaths (functor_on_objects F) e) = functor_on_z_iso F (idtoiso e). Proof. induction e. apply z_iso_eq. apply (! functor_id _ _ ). 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.