Definition functor_to_cat_of_elems_data : functor_data C' cat_of_elems. Proof. use make_functor_data. - exact (λ c, G₂ c ,, γ c (pr2 (G₁ c))). - refine (λ c₁ c₂ f, # G₂ f ,, _). abstract (cbn ; refine (!(eqtohomot (nat_trans_ax γ _ _ f) (pr2 (G₁ c₁))) @ _) ; cbn ; apply maponpaths ; exact (pr2 (# G₁ f))). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.