Definition cod_fib_terminal_from_base_data : functor_data C (C/T). Proof. use make_functor_data. - exact (λ x, make_cod_fib_ob (TerminalArrow T x)). - simple refine (λ _ _ f, make_cod_fib_mor _ _). + exact f. + abstract (cbn ; apply TerminalArrowEq). 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.