Definition disp_functor_eq_weq : FF = GG ≃ disp_nat_z_iso FF GG (nat_z_iso_id F) := (disp_functor_eq_step_5 ∘ disp_functor_eq_step_4 ∘ disp_functor_eq_step_3 ∘ disp_functor_eq_step_2 ∘ disp_functor_eq_step_1)%weq.
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.