Definition cod_fib_terminal_equivalence : equivalence_of_cats (C/T) C. Proof. use make_equivalence_of_cats. - use make_adjunction_data. + exact cod_fib_terminal_to_base. + exact cod_fib_terminal_from_base. + exact cod_fib_terminal_unit. + exact cod_fib_terminal_counit. - split. + intro x. use is_z_iso_fiber_from_is_z_iso_disp. use is_z_iso_disp_codomain. apply identity_is_z_iso. + intro x. apply identity_is_z_iso. Defined.
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.Equivalences.Core. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.