Definition orthogonal_to_orthogonal_via_pb (HB_2_1 : is_univalent_2_1 B) (Hf : f ⊥ g) : orthogonal_via_pb HB_2_1. Proof. use (left_adjoint_equivalence_to_pb _ _ _ (@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)) _ _). - exact univalent_cat_is_univalent_2_0. - exact (orthogonal_functor f g). - exact (@equiv_cat_to_adj_equiv (univ_hom HB_2_1 b₂ c₁) (@univalent_iso_comma (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_functor f g) Hf). - use nat_z_iso_to_invertible_2cell. use make_nat_z_iso. + use make_nat_trans. * exact (λ _, id2 _). * abstract (intros h₁ h₂ α ; cbn ; rewrite id2_left, id2_right ; apply idpath). + intro. use is_inv2cell_to_is_z_iso ; cbn. is_iso. - use nat_z_iso_to_invertible_2cell. use make_nat_z_iso. + use make_nat_trans. * exact (λ _, id2 _). * abstract (intros h₁ h₂ α ; cbn ; rewrite id2_left, id2_right ; apply idpath). + intro. use is_inv2cell_to_is_z_iso ; cbn. is_iso. - abstract (use nat_trans_eq ; [ apply homset_property | ] ; intro x ; cbn ; rewrite id2_rwhisker, lwhisker_id2 ; 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.