Proposition mono_cod_fiber_functor_on_mor {C : category} (HC : Pullbacks C) {x y : C} (f : x --> y) {zg₁ zg₂ : C /m y} (gp : zg₁ --> zg₂) : #(mono_cod_pb HC f) gp = (#(cod_pb HC f) (#(mono_cod_to_cod_fib _) gp) ,, tt). Proof. use subtypePath. { intro. apply isapropunit. } use subtypePath. { intro. apply homset_property. } rewrite cod_fiber_functor_on_mor. use (MorphismsIntoPullbackEqual (isPullback_Pullback (HC y (pr11 zg₂) x (pr21 zg₂) f))) ; cbn. - rewrite !PullbackArrow_PullbackPr1. etrans. { apply (PullbackArrow_PullbackPr1 (HC y (pr11 zg₂) x (pr21 zg₂) f)). } rewrite transportf_mono_cod_disp. cbn. apply idpath. - rewrite !PullbackArrow_PullbackPr2. etrans. { apply (PullbackArrow_PullbackPr2 (HC y (pr11 zg₂) x (pr21 zg₂) f)). } apply id_right. 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.