Proposition lax_double_functor_to_extension_laws : lax_extension_laws lax_double_functor_to_extension_data. Proof. repeat split. - intros X Y R S p. pose (enriched_relation_square_to_le (#s F (enriched_relation_le_to_square p))) as e. unfold lax_double_functor_to_extension_data. refine (enriched_relation_le_trans e _). rewrite <- enriched_relation_comp_conj. rewrite !(lax_double_functor_id_v F). rewrite companion_enriched_relation_id. rewrite conjoint_enriched_relation_id. refine (enriched_relation_le_trans _ _). { use enriched_relation_square_to_le. apply enriched_relation_lunitor. } use enriched_relation_square_to_le. apply enriched_relation_runitor. - intros. apply (lax_double_functor_comp_h F). - intros X Y f ; cbn. refine (enriched_relation_le_trans _ _). { use enriched_relation_eq_to_le. apply maponpaths. refine (!(id_left (#F f)) @ _). apply idpath. } refine (enriched_relation_le_trans _ _). { exact (companion_enriched_relation_comp (identity (F X)) (#F f)). } refine (enriched_relation_le_trans _ _). { refine (enriched_relation_le_comp _ (enriched_relation_le_refl _)). rewrite companion_enriched_relation_id. exact (enriched_relation_square_to_le (lax_double_functor_id_h F X)). } refine (enriched_relation_le_trans _ _). { refine (enriched_relation_le_comp _ (enriched_relation_le_refl _)). exact (#s F (companion_enriched_relation_right f)). } rewrite <- enriched_relation_comp_conj. refine (enriched_relation_le_trans _ _). { use enriched_relation_eq_to_le. do 2 apply maponpaths_2. etrans. { apply maponpaths. apply (lax_double_functor_id_v F X). } rewrite companion_enriched_relation_id. apply idpath. } refine (enriched_relation_le_trans _ _). { refine (enriched_relation_le_comp _ (enriched_relation_le_refl _)). use enriched_relation_square_to_le. apply enriched_relation_lunitor. } refine (enriched_relation_le_trans _ _). { use enriched_relation_square_to_le. apply enriched_relation_lassociator. } refine (enriched_relation_le_trans _ _). { refine (enriched_relation_le_comp (enriched_relation_le_refl _) _). use enriched_relation_square_to_le. apply comp_conjoint_companion_enriched_relation. } use enriched_relation_square_to_le. apply enriched_relation_runitor. - intros X Y f ; cbn. refine (enriched_relation_le_trans _ _). { use enriched_relation_eq_to_le. apply maponpaths. refine (!(id_left (#F f)) @ _). apply idpath. } refine (enriched_relation_le_trans _ _). { exact (conjoint_enriched_relation_comp (identity (F X)) (#F f)). } refine (enriched_relation_le_trans _ _). { refine (enriched_relation_le_comp (enriched_relation_le_refl _) _). rewrite conjoint_enriched_relation_id. exact (enriched_relation_square_to_le (lax_double_functor_id_h F X)). } refine (enriched_relation_le_trans _ _). { refine (enriched_relation_le_comp (enriched_relation_le_refl _) _). exact (enriched_relation_square_to_le (#s F (conjoint_enriched_relation_left f))). } rewrite <- enriched_relation_comp_conj. refine (enriched_relation_le_trans _ _). { use enriched_relation_eq_to_le. do 2 apply maponpaths. etrans. { do 2 apply maponpaths. apply (lax_double_functor_id_v F X). } rewrite conjoint_enriched_relation_id. apply idpath. } refine (enriched_relation_le_trans _ _). { refine (enriched_relation_le_comp (enriched_relation_le_refl _) _). refine (enriched_relation_le_comp (enriched_relation_le_refl _) _). use enriched_relation_square_to_le. apply enriched_relation_runitor. } refine (enriched_relation_le_trans _ _). { use enriched_relation_square_to_le. apply enriched_relation_rassociator. } refine (enriched_relation_le_trans _ _). { refine (enriched_relation_le_comp _ (enriched_relation_le_refl _)). use enriched_relation_square_to_le. apply comp_conjoint_companion_enriched_relation. } use enriched_relation_square_to_le. apply enriched_relation_lunitor. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.EnrichedRels. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. 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.DoubleFunctor. Require Import UniMath.Bicategories.DoubleCategories.Examples.EnrichedRelDoubleCat. Require Import UniMath.CategoryTheory.EnrichedCats.BenabouCosmos. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichedRelation. Require Import UniMath.CategoryTheory.EnrichedCats.LaxExtension.