Definition cleaving_to_indexed_cat_data : indexed_cat_data (C^opp). Proof. use make_indexed_cat_data. - exact (λ x, univalent_fiber_category D x). - exact (λ x y f, fiber_functor_from_cleaving D HD f). - exact (λ x, fiber_functor_from_cleaving_identity HD x). - exact (λ x y z f g, fiber_functor_from_cleaving_comp HD f g). Defined.
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.OppositeCategory.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.IndexedCategories.IndexedCategory.