Definition iso_cleaving_functor_alg : iso_cleaving disp_cat_functor_alg. Proof. intros c c' i d. cbn in *. use tpair. - exact (compose (compose (functor_on_z_iso F i) d) (z_iso_inv_from_z_iso i)). - cbn. unfold z_iso_disp. cbn. use tpair. + abstract ( etrans; [eapply pathsinv0; apply id_right |]; repeat rewrite <- assoc; do 2 apply maponpaths; apply pathsinv0; apply z_iso_after_z_iso_inv ). + use tpair. * unfold functor_alg_mor. cbn. repeat rewrite assoc. unfold functor_alg_mor. cbn. rewrite <- functor_comp. rewrite z_iso_after_z_iso_inv. rewrite functor_id. rewrite id_left. apply idpath. * split; apply homset_property. Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Limits. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.SIP. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Reindexing. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Sigma. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits.