Definition make_orthogonal_essentially_surjective : essentially_surjective (orthogonal_functor f g). Proof. intros h. pose (ℓ := H₃ (pr11 h) (pr21 h) (z_iso_to_inv2cell (pr2 h))). apply hinhpr. simple refine (_ ,, _). - exact (pr1 ℓ). - use make_z_iso'. + simple refine ((_ ,, _) ,, _) ; cbn. * exact (pr12 ℓ). * exact (pr122 ℓ). * exact (pr222 ℓ). + use is_z_iso_iso_comma. * use is_inv2cell_to_is_z_iso. apply property_from_invertible_2cell. * use is_inv2cell_to_is_z_iso. apply property_from_invertible_2cell. 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.