Definition disp_functor_eq_step_3 : pr1 FF ╝ pr1 GG ≃ ∑ (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). Proof. use weqbandf. - exact (weqonsecfibers _ _ (λ x, weqtoforallpaths _ _ _) ∘ weqtoforallpaths _ _ _)%weq. - intro p. induction FF as [ [ FFo FFm ] FFp ]. induction GG as [ [ GGo GGm ] GGp ]. cbn in p. induction p ; cbn. refine (weqonsecfibers _ _ (λ x, _) ∘ weqtoforallpaths _ _ _)%weq. refine (weqonsecfibers _ _ (λ y, _) ∘ weqtoforallpaths _ _ _)%weq. refine (weqonsecfibers _ _ (λ xx, _) ∘ weqtoforallpaths _ _ _)%weq. refine (weqonsecfibers _ _ (λ yy, _) ∘ weqtoforallpaths _ _ _)%weq. refine (weqonsecfibers _ _ (λ f, _) ∘ weqtoforallpaths _ _ _)%weq. refine (weqonsecfibers _ _ (λ ff, _) ∘ weqtoforallpaths _ _ _)%weq. use weqimplimpl. + intro pp. rewrite id_right_disp. rewrite id_left_disp. rewrite pp. unfold transportb. rewrite transport_f_f. apply maponpaths_2. apply homset_property. + intro pp. rewrite id_right_disp, id_left_disp in pp. unfold transportb in pp. rewrite transport_f_f in pp. refine (!_ @ maponpaths (λ z, transportf _ (id_right _) z) pp @ _). * rewrite transport_f_f. apply transportf_set. apply homset_property. * rewrite transport_f_f. apply transportf_set. apply homset_property. + apply D₂. + 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.