Proposition terminal_mor_factorization_eq {x y : C} {f : x --> x} (p : identity _ = f) {g g' : x --> y} (q : g = g') {xx : D x} (ff : xx -->[ f ] pr1 (HD y x g (terminal_obj_in_fib T y))) (gg : xx -->[ g' ] terminal_obj_in_fib T y) : (ff ;; HD y x g (terminal_obj_in_fib T y))%mor_disp = transportb (λ z, _ -->[ z ] _) (maponpaths (λ z, z · _) (!p) @ id_left _ @ q) gg. Proof. induction p, q. refine (_ @ cartesian_factorisation_commutes (pr22 (HD y x g (terminal_obj_in_fib T y))) _ _). apply maponpaths_2. apply (TerminalArrowEq (T := lift_terminal_in_fib T g)). 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.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Total. 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.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Preservation. Section RightAdjointFromTerminal. End RightAdjointFromTerminal.