Definition make_orthogonal_full : full (orthogonal_functor f g). Proof. intros l₁ l₂. intro k. apply hinhpr. simple refine (_ ,, _) ; cbn. - exact (pr1 (H₁ l₁ l₂ (pr11 k) (pr21 k) (pr2 k))). - abstract (use subtypePath ; [ intro ; apply cellset_property | ] ; cbn ; exact (pathsdirprod (pr12 (H₁ l₁ l₂ (pr11 k) (pr21 k) (pr2 k))) (pr22 (H₁ l₁ l₂ (pr11 k) (pr21 k) (pr2 k))))). 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.