Definition orthogonal_via_pb_to_orthogonal_nat_trans (HB_2_1 : is_univalent_2_1 B) : orthogonal_functor f g ⟹ pr1 (pb_ump_mor (@iso_comma_has_pb_ump (univ_hom HB_2_1 b₁ c₁) (univ_hom HB_2_1 b₂ c₂) (univ_hom HB_2_1 b₁ c₂) (post_comp b₁ g) (pre_comp c₂ f)) (orthogonal_via_pb_cone HB_2_1)). Proof. use make_nat_trans. - intro h. simple refine ((id2 _ ,, id2 _) ,, _). abstract (cbn ; rewrite id2_rwhisker, lwhisker_id2, id2_left, id2_right ; apply idpath). - abstract (intros h₁ h₂ γ ; use subtypePath ; [ intro ; apply cellset_property | ] ; cbn ; rewrite !id2_left, !id2_right ; apply idpath). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.FullyFaithful. Require Import UniMath.CategoryTheory.IsoCommaCategory. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Morphisms.Properties.ClosedUnderInvertibles. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.PullbackFunctions. Import PullbackFunctions.Notations. Require Import UniMath.Bicategories.Limits.PullbackEquivalences. Require Import UniMath.Bicategories.Limits.Examples.BicatOfUnivCatsLimits.