Proposition is_left_adjoint_slice_dom_unique : isaprop (∑ (f' : yf --> pr_cod_fib BP x z), g = # (slice_dom x) f' · BinProductPr2 C (BP x z)). Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath ; [ intro ; apply homset_property | ]. use eq_mor_cod_fib. use BinProductArrowsEq. - exact (mor_eq (pr1 φ₁) @ !(mor_eq (pr1 φ₂))). - exact (!(pr2 φ₁) @ pr2 φ₂). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod. Require Import UniMath.CategoryTheory.Limits.BinProducts.