Definition comp_is_cartesian_sfib : is_cartesian_sfib F (f · g). Proof. intros w h₁ h₂ p. use iscontraprop1. - exact (comp_is_cartesian_sfib_factor_unique p). - simple refine (_ ,, _ ,, _). + exact (comp_is_cartesian_sfib_factor p). + exact (comp_is_cartesian_sfib_factor_over p). + exact (comp_is_cartesian_sfib_factor_comm 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.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.