Definition disp_functor_eq_step_5_right : disp_nat_z_iso FF GG (nat_z_iso_id F) → ∑ (p : ∏ (x : C₁) (xx : D₁ x), z_iso_disp (identity_z_iso _) (FF x xx) (GG x xx)), ∏ (x y : C₁) (xx : D₁ x) (yy : D₁ y) (f : x --> y) (ff : xx -->[ f ] yy), ♯FF ff ;; p y yy = transportb _ (id_right _ @ !(id_left _)) (p x xx ;; ♯GG ff). Proof. simple refine (λ p, (λ x xx, _ ,, _) ,, _). - exact (p x xx). - exact (pr2 p x xx). - abstract (intros x y f xx yy ff ; refine (disp_nat_trans_ax p ff @ _) ; apply maponpaths_2 ; apply homset_property). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.