Definition all_conjoints_coreflections_double_cat (C : two_cat) (HC : locally_univalent_two_cat C) : all_conjoints_double_cat (coreflections_double_cat C HC). Proof. intros x y fHf. cbn in x. pose (f := pr1 fHf). pose (Hf := pr12 fHf : left_adjoint _). refine (left_adjoint_right_adjoint Hf ,, _). exact (are_conjoints_coreflections_double_cat HC fHf). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Core.TwoCategories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Sigma. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.SquaresTwoCat. Require Import UniMath.Bicategories.Core.Bicat. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.Strictness. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Morphisms.Properties.Composition. Require Import UniMath.Bicategories.DoubleCategories.Basics.StrictDoubleCatBasics. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.UnivalentDoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.PseudoDoubleSetCats. Require Import UniMath.Bicategories.DoubleCategories.Core.CompanionsAndConjoints. Require Import UniMath.Bicategories.DoubleCategories.Examples.SquareDoubleCatTwo. Require Import UniMath.Bicategories.DoubleCategories.Examples.DoubleCatOnDispCat. Import TwoCategories.Notations.