Definition all_companions_double_cat_on_disp_cat (H : all_companions_double_cat C) : all_companions_double_cat double_cat_on_disp_cat. Proof. intros x y f. pose (c := H (pr1 x) (pr1 y) (pr1 f)). simple refine (_ ,, _). - exact (pr1 c). - use make_double_cat_are_companions. + exact (pr12 c). + exact (pr122 c). + abstract (refine (transportf_disp_mor2_twosided_disp_cat_on_disp_cat _ _ _ _ _ _ @ _) ; refine (_ @ pr1 (pr222 c)) ; use transportf_disp_mor2_eq ; apply maponpaths_2 ; refine (transportf_disp_mor2_twosided_disp_cat_on_disp_cat _ _ _ _ _ _ @ _) ; use transportf_disp_mor2_eq ; apply idpath). + abstract (refine (transportf_disp_mor2_twosided_disp_cat_on_disp_cat _ _ _ _ _ _ @ _) ; refine (_ @ pr2 (pr222 c)) ; use transportf_disp_mor2_eq ; refine (transportf_disp_mor2_twosided_disp_cat_on_disp_cat _ _ _ _ _ _ @ _) ; use transportf_disp_mor2_eq ; apply idpath). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. 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.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.TwoSidedDispCatOnDispCat. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. 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.