Definition comp_diag_dr_corner {B : verity_double_bicat} {x y z : B} {v₁ : x -|-> y} {v₂ : y -|-> z} {h₁ : x --> y} {h₂ : y --> z} (s₁ : square_double_bicat h₁ (id_h y) v₁ (id_v y)) (s₂ : square_double_bicat h₂ (id_h z) v₂ (id_v z)) : square_double_bicat (h₁ · h₂) (id_h z) (v₁ · v₂) (id_v z) := lunitor _ ▹s (lunitor _ ▿s ((s₁ ⋆h id_v_square_bicat h₂) ⋆v (id_h_square_bicat v₂ ⋆h s₂))).
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.VerityDoubleBicat.