Definition cod_fib_terminal_unit : functor_identity _ ⟹ cod_fib_terminal_to_base ∙ cod_fib_terminal_from_base. Proof. use make_nat_trans. - simple refine (λ x, make_cod_fib_mor _ _). + apply identity. + abstract (cbn ; apply TerminalArrowEq). - abstract (intros x y f ; use eq_mor_cod_fib ; rewrite !comp_in_cod_fib ; cbn ; rewrite id_left, id_right ; apply idpath). 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.