Definition functor_to_cat_of_elems_pointed_nat_trans : functor_to_cat_of_elems ∙ cat_of_elems_to_pointed ⟹ G₁. Proof. use make_nat_trans. - refine (λ x, inv_from_z_iso (nat_z_iso_pointwise_z_iso γ x) ,, _) ; cbn. abstract (exact (eqtohomot (z_iso_inv_after_z_iso (nat_z_iso_pointwise_z_iso γ x)) (pr2 (G₁ x)))). - abstract (intros c₁ c₂ f ; cbn ; use subtypePath ; [ intro ; apply (pr1 (G₁ c₂)) | ] ; cbn ; use funextsec ; intro x ; exact (eqtohomot (nat_trans_ax (nat_z_iso_to_trans_inv γ) _ _ f) x)). 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.