Proposition double_lunitor_nat {C : category} {D : twosided_disp_cat C C} {I : hor_id D} {Cm : hor_comp D} (l : double_cat_lunitor I Cm) {x₁ x₂ y₁ y₂ : C} {h₁ : D x₁ y₁} {h₂ : D x₂ y₂} {v₁ : x₁ --> x₂} {v₂ : y₁ --> y₂} (τ : h₁ -->[ v₁ ][ v₂ ] h₂) : transportb_disp_mor2 (id_right _ @ !(id_left _)) (id_right _ @ !(id_left _)) (double_lunitor l h₁ ;;2 τ) = double_hor_comp_mor Cm (double_id_mor I _) τ ;;2 double_lunitor l h₂. Proof. exact (pr2 l x₁ x₂ y₁ y₂ h₁ h₂ v₁ v₂ τ). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos.