Proposition from_monic_slice_to_terminal (H : isMonic (cod_mor xf)) : isMonic (TerminalArrow T xf). Proof. intros xg φ ψ p. use eq_mor_cod_fib. use H. use (cancel_z_iso _ _ (functor_on_z_iso (slice_dom _) (z_iso_Terminals T' T))). pose (maponpaths dom_mor p) as q. rewrite !comp_in_cod_fib in q. assert (TerminalArrow T xf = fm · TerminalArrow T T') as r. { apply TerminalArrowEq. } rewrite r in q ; clear r. rewrite !comp_in_cod_fib in q. rewrite !assoc'. exact q. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Limits.Terminal. 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.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.MonoCodomain. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Sigma. Require Import UniMath.CategoryTheory.DisplayedCats.MonoCodomain.FiberMonoCod. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodLimits. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodDomain. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.