Definition is_opcartesian_total_setcategory_of_set_functor : is_opcartesian_sopfib (pr1_total_category_of_set_functor G) f. Proof. intros e₃ g h p. use iscontraprop1. - exact (is_opcartesian_total_setcategory_of_set_functor_factor_unique g h). - simple refine (_ ,, (_ ,, _)). + exact (is_opcartesian_total_setcategory_of_set_functor_factor g h p). + abstract (cbn ; apply idpath). + exact (is_opcartesian_total_setcategory_of_set_functor_factor_comm g h p). 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.Setcategories. Require Import UniMath.CategoryTheory.DisplayedCats.StreetOpFibration. Require Import UniMath.CategoryTheory.Categories.CategoryOfSetCategories. Require Import UniMath.CategoryTheory.GrothendieckConstruction.TotalCategory. Require Import UniMath.CategoryTheory.GrothendieckConstruction.Projection.