Definition comp_faithful {h₁ : slice_bicat b₁} {h₂ : slice_bicat b₂} {α β : comp_ob h₁ --> h₂} (p : comp_unit h₁ · # (pb_psfunctor B f) α ==> comp_unit h₁ · # (pb_psfunctor B f) β) (q₁ q₂ : α ==> β) (r₁ : comp_unit h₁ ◃ ## (pb_psfunctor B f) q₁ = p) (r₂ : comp_unit h₁ ◃ ## (pb_psfunctor B f) q₂ = p) : q₁ = q₂.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.Bicategories.Core.Bicat. Import Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Slice. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.PseudoFunctors.UniversalArrow. Require Import UniMath.Bicategories.PseudoFunctors.Examples.PullbackFunctor. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.PullbackFunctions. Import PullbackFunctions.Notations.