Definition disp_nat_trans_to_indexed_nat_trans_data : indexed_nat_trans_data (cartesian_disp_functor_to_indexed_functor HD₁ HD₂ F) (cartesian_disp_functor_to_indexed_functor HD₁ HD₂ G). Proof. intro x. use make_nat_trans. - exact (λ xx, τ x xx). - abstract (intros xx yy ff ; cbn ; refine (maponpaths (transportf _ _) (disp_nat_trans_ax τ ff) @ _) ; unfold transportb ; rewrite transport_f_f ; apply maponpaths_2 ; apply homset_property). 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.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.IndexedCategories.IndexedCategory. Require Import UniMath.CategoryTheory.IndexedCategories.IndexedFunctor. Require Import UniMath.CategoryTheory.IndexedCategories.IndexedTransformation. Require Import UniMath.CategoryTheory.IndexedCategories.FibrationToIndexedCategory. Require Import UniMath.CategoryTheory.IndexedCategories.CartesianToIndexedFunctor.