Definition disp_functor_eq_step_4 : (∑ (p : ∏ (x : C₁) (xx : D₁ x), FF x xx = GG x xx), ∏ (x y : C₁) (xx : D₁ x) (yy : D₁ y) (f : x --> y) (ff : xx -->[ f ] yy), ♯FF ff ;; idtoiso_disp (idpath _) (p y yy) = transportb _ (id_right _ @ !(id_left _)) (idtoiso_disp (idpath _) (p x xx) ;; ♯GG ff)) ≃ (∑ (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. use weqbandf. - exact (weqonsecfibers _ _ (λ x, weqonsecfibers _ _ (λ y, make_weq _ (HD₂ _ _ (idpath _) _ _)))). - intro p. use weqimplimpl. + intros pp x y xx yy f ff. cbn -[idtoiso_disp]. exact (pp x y xx yy f ff). + intros pp x y xx yy f ff. cbn -[idtoiso_disp]. exact (pp x y xx yy f ff). + repeat (use impred ; intro). apply D₂. + repeat (use impred ; intro). apply D₂. 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.