Proposition isTerminal_mono_codomain_fib {x : C} (yf : C /m x) (H : is_z_isomorphism (pr21 yf)) : isTerminal (C /m x) yf. Proof. pose (f := (_ ,, H) : z_iso _ _). intro zg. use iscontraprop1. - abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use eq_mor_mono_cod_fib ; use (cancel_z_iso _ _ f) ; exact (pr2 φ₁ @ !(pr2 φ₂))). - use make_mono_cod_fib_mor. + exact (mono_cod_mor zg · inv_from_z_iso f). + abstract (rewrite assoc' ; refine (_ @ id_right _) ; apply maponpaths ; exact (z_iso_after_z_iso_inv f)). Defined.
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.Adjunctions.Core. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Preservation. 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.Examples.MonoCodomain. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseTerminal. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseProducts. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodLimits. Require Import UniMath.CategoryTheory.DisplayedCats.MonoCodomain.FiberMonoCod. Require Import UniMath.CategoryTheory.DisplayedCats.MonoCodomain.Inclusion.