Proposition comprehension_eso_inv_mor_help_sub_pr1 : comprehension_eso_inv_mor_help_sub · PullbackPr1 HΔ = γΔ. Proof. apply (PullbackArrow_PullbackPr1 HΔ). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Equivalences. Require Import UniMath.CategoryTheory.DisplayedCats.EquivalenceOverId. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseTerminal. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseProducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseEqualizers. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.FullyFaithfulDispFunctor. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.ComprehensionCat.BicatOfCompCat. Require Import UniMath.Bicategories.ComprehensionCat.CompCatNotations. Require Import UniMath.Bicategories.ComprehensionCat.DFLCompCat. Require Import UniMath.Bicategories.ComprehensionCat.DFLCompCatNotations.