Definition cartesian_terminal_via_adj_to_cartesian_terminal_preserves {x y : B} (f : x --> y) : preserves_terminal (pre_comp b f). Proof. use preserves_terminal_if_preserves_chosen. - apply cartesian_terminal_via_adj_to_cartesian_terminal_obj. - use (iso_to_Terminal (cartesian_terminal_via_adj_to_cartesian_terminal_obj x)). use inv2cell_to_z_iso. refine (comp_of_invertible_2cell (rwhisker_of_invertible_2cell _ _) (rassociator_invertible_2cell _ _ _)). apply (is_bifinal_invertible_2cell_property (pr2 T)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.UnivalenceOp. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Limits.Final. Require Import UniMath.Bicategories.Limits.Products. Section FromAdj. End FromAdj. Section FromAdj. End FromAdj.