Definition disp_cat_eq_step_6_right : (∑ (F : disp_functor (functor_identity C) D₁ D₂), (∏ (x : C), isweq (F x)) × disp_functor_ff F) → disp_cat_eq_functor. Proof. intro FF. induction FF as [ FF [ HF₁ HF₂ ]]. simple refine (_ ,, _ ,, _ ,, _). - intro x. use make_weq. + exact (FF x). + exact (HF₁ x). - intros x y xx yy f. use make_weq. + exact (λ ff, ♯FF ff). + apply HF₂. - intros x xx ; cbn. exact (disp_functor_id FF xx). - intros x y z f g xx yy zz ff gg ; cbn. exact (disp_functor_comp FF ff gg). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. 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. Require Import UniMath.CategoryTheory.DisplayedCats.Equivalences. Require Import UniMath.CategoryTheory.DisplayedCats.DisplayedFunctorEq. Require Import UniMath.CategoryTheory.DisplayedCats.EquivalenceOverId.