-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
inst_3 : Category.{v₄, u₄} D
inst_4 : Category.{v₅, u₅} E
inst_5 : Category.{v₆, u₆} F
G : Functor.{v₁, v₄, u₁, u₄} A D
H : Functor.{v₂, v₅, u₂, u₅} B E
K : Functor.{v₃, v₆, u₃, u₆} C F
L₁ : Functor.{v₁, v₂, u₁, u₂} A B
R₁ : Functor.{v₂, v₁, u₂, u₁} B A
L₂ : Functor.{v₄, v₅, u₄, u₅} D E
R₂ : Functor.{v₅, v₄, u₅, u₄} E D
L₃ : Functor.{v₂, v₃, u₂, u₃} B C
R₃ : Functor.{v₃, v₂, u₃, u₂} C B
L₄ : Functor.{v₅, v₆, u₅, u₆} E F
R₄ : Functor.{v₆, v₅, u₆, u₅} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
adj₄ : L₄ ⊣ R₄
α : TwoSquare G L₁ L₂ H
β : TwoSquare H L₃ L₄ K
h :
  ∀ (c : C),
    app
        (natTrans
          (({
                toFun := fun (α : TwoSquare G (L₁ ⋙ L₃) (L₂ ⋙ L₄) K) ↦
                  TwoSquare.mk (R₃ ⋙ R₁) K G (R₄ ⋙ R₂)
                    (((R₃ ⋙ R₁) ⋙ G).rightUnitor.inv ≫
                      ((R₃ ⋙ R₁) ⋙ G).whiskerLeft
                          (Adjunction.mk'
                              {
                                homEquiv := fun (x : D) (x_1 : F) ↦
                                  Equiv.trans (adj₄.homEquiv (L₂.obj x) x_1) (adj₂.homEquiv x (R₄.obj x_1)),
                                unit :=
                                  adj₂.unit ≫
                                    whiskerRight
                                        (L₂.rightUnitor.inv ≫ L₂.whiskerLeft adj₄.unit ≫ (L₂.associator L₄ R₄).inv) R₂ ≫
                                      ((L₂ ⋙ L₄).associator R₄ R₂).hom,
                                counit :=
                                  ((R₄ ⋙ R₂).associator L₂ L₄).inv ≫
                                    whiskerRight
                                        ((R₄.associator R₂ L₂).hom ≫ R₄.whiskerLeft adj₂.counit ≫ R₄.rightUnitor.hom)
                                        L₄ ≫
                                      adj₄.counit,
                                homEquiv_unit := ⋯, homEquiv_counit := ⋯ :
                                CoreHomEquivUnitCounit (L₂ ⋙ L₄) (R₄ ⋙ R₂) }).unit ≫
                        ((R₃ ⋙ R₁).associator G ((L₂ ⋙ L₄) ⋙ R₄ ⋙ R₂)).hom ≫
                          (R₃ ⋙ R₁).whiskerLeft (G.associator (L₂ ⋙ L₄) (R₄ ⋙ R₂)).inv ≫
                            (R₃ ⋙ R₁).whiskerLeft (whiskerRight α.natTrans (R₄ ⋙ R₂)) ≫
                              (R₃ ⋙ R₁).whiskerLeft ((L₁ ⋙ L₃).associator K (R₄ ⋙ R₂)).hom ≫
                                ((R₃ ⋙ R₁).associator (L₁ ⋙ L₃) (K ⋙ R₄ ⋙ R₂)).inv ≫
                                  whiskerRight
                                      (Adjunction.mk'
                                          {
                                            homEquiv := fun (x : A) (x_1 : C) ↦
                                              Equiv.trans (adj₃.homEquiv (L₁.obj x) x_1) (adj₁.homEquiv x (R₃.obj x_1)),
                                            unit :=
                                              adj₁.unit ≫
                                                whiskerRight
                                                    (L₁.rightUnitor.inv ≫
                                                      L₁.whiskerLeft adj₃.unit ≫ (L₁.associator L₃ R₃).inv)
                                                    R₁ ≫
                                                  ((L₁ ⋙ L₃).associator R₃ R₁).hom,
                                            counit :=
                                              ((R₃ ⋙ R₁).associator L₁ L₃).inv ≫
                                                whiskerRight
                                                    ((R₃.associator R₁ L₁).hom ≫
                                                      R₃.whiskerLeft adj₁.counit ≫ R₃.rightUnitor.hom)
                                                    L₃ ≫
                                                  adj₃.counit,
                                            homEquiv_unit := ⋯, homEquiv_counit := ⋯ :
                                            CoreHomEquivUnitCounit (L₁ ⋙ L₃) (R₃ ⋙ R₁) }).counit
                                      (K ⋙ R₄ ⋙ R₂) ≫
                                    (K ⋙ R₄ ⋙ R₂).leftUnitor.hom),
                invFun := fun (β : TwoSquare (R₃ ⋙ R₁) K G (R₄ ⋙ R₂)) ↦
                  TwoSquare.mk G (L₁ ⋙ L₃) (L₂ ⋙ L₄) K
                    ((G ⋙ L₂ ⋙ L₄).leftUnitor.inv ≫
                      whiskerRight
                          (Adjunction.mk'
                              {
                                homEquiv := fun (x : A) (x_1 : C) ↦
                                  Equiv.trans (adj₃.homEquiv (L₁.obj x) x_1) (adj₁.homEquiv x (R₃.obj x_1)),
                                unit :=
                                  adj₁.unit ≫
                                    whiskerRight
                                        (L₁.rightUnitor.inv ≫ L₁.whiskerLeft adj₃.unit ≫ (L₁.associator L₃ R₃).inv) R₁ ≫
                                      ((L₁ ⋙ L₃).associator R₃ R₁).hom,
                                counit :=
                                  ((R₃ ⋙ R₁).associator L₁ L₃).inv ≫
                                    whiskerRight
                                        ((R₃.associator R₁ L₁).hom ≫ R₃.whiskerLeft adj₁.counit ≫ R₃.rightUnitor.hom)
                                        L₃ ≫
                                      adj₃.counit,
                                homEquiv_unit := ⋯, homEquiv_counit := ⋯ :
                                CoreHomEquivUnitCounit (L₁ ⋙ L₃) (R₃ ⋙ R₁) }).unit
                          (G ⋙ L₂ ⋙ L₄) ≫
                        (((L₁ ⋙ L₃) ⋙ R₃ ⋙ R₁).associator G (L₂ ⋙ L₄)).inv ≫
                          whiskerRight ((L₁ ⋙ L₃).associator (R₃ ⋙ R₁) G).hom (L₂ ⋙ L₄) ≫
                            whiskerRight ((L₁ ⋙ L₃).whiskerLeft β.natTrans) (L₂ ⋙ L₄) ≫
                              whiskerRight ((L₁ ⋙ L₃).associator K (R₄ ⋙ R₂)).inv (L₂ ⋙ L₄) ≫
                                (((L₁ ⋙ L₃) ⋙ K).associator (R₄ ⋙ R₂) (L₂ ⋙ L₄)).hom ≫
                                  ((L₁ ⋙ L₃) ⋙ K).whiskerLeft
                                      (Adjunction.mk'
                                          {
                                            homEquiv := fun (x : D) (x_1 : F) ↦
                                              Equiv.trans (adj₄.homEquiv (L₂.obj x) x_1) (adj₂.homEquiv x (R₄.obj x_1)),
                                            unit :=
                                              adj₂.unit ≫
                                                whiskerRight
                                                    (L₂.rightUnitor.inv ≫
                                                      L₂.whiskerLeft adj₄.unit ≫ (L₂.associator L₄ R₄).inv)
                                                    R₂ ≫
                                                  ((L₂ ⋙ L₄).associator R₄ R₂).hom,
                                            counit :=
                                              ((R₄ ⋙ R₂).associator L₂ L₄).inv ≫
                                                whiskerRight
                                                    ((R₄.associator R₂ L₂).hom ≫
                                                      R₄.whiskerLeft adj₂.counit ≫ R₄.rightUnitor.hom)
                                                    L₄ ≫
                                                  adj₄.counit,
                                            homEquiv_unit := ⋯, homEquiv_counit := ⋯ :
                                            CoreHomEquivUnitCounit (L₂ ⋙ L₄) (R₄ ⋙ R₂) }).counit ≫
                                    ((L₁ ⋙ L₃) ⋙ K).rightUnitor.hom),
                left_inv := ⋯, right_inv := ⋯ } :
              (a : TwoSquare G (L₁ ⋙ L₃) (L₂ ⋙ L₄) K) → TwoSquare (R₃ ⋙ R₁) K G (R₄ ⋙ R₂))
            (TwoSquare.mk G (L₁ ⋙ L₃) (L₂ ⋙ L₄) K
              ((G.associator L₂ L₄).inv ≫
                whiskerRight α.natTrans L₄ ≫
                  (L₁.associator H L₄).hom ≫ L₁.whiskerLeft β.natTrans ≫ (L₁.associator L₃ K).inv))))
        c =
      (TwoSquare.mk (R₃ ⋙ R₁) K G (R₄ ⋙ R₂)
              ((R₃.associator R₁ G).hom ≫
                R₃.whiskerLeft
                    (natTrans
                      (({
                            toFun := fun (α : TwoSquare G L₁ L₂ H) ↦
                              TwoSquare.mk R₁ H G R₂
                                ((R₁ ⋙ G).rightUnitor.inv ≫
                                  (R₁ ⋙ G).whiskerLeft adj₂.unit ≫
                                    (R₁.associator G (L₂ ⋙ R₂)).hom ≫
                                      R₁.whiskerLeft (G.associator L₂ R₂).inv ≫
                                        R₁.whiskerLeft (whiskerRight α.natTrans R₂) ≫
                                          R₁.whiskerLeft (L₁.associator H R₂).hom ≫
                                            (R₁.associator L₁ (H ⋙ R₂)).inv ≫
                                              whiskerRight adj₁.counit (H ⋙ R₂) ≫ (H ⋙ R₂).leftUnitor.hom),
                            invFun := fun (β : TwoSquare R₁ H G R₂) ↦
                              TwoSquare.mk G L₁ L₂ H
                                ((G ⋙ L₂).leftUnitor.inv ≫
                                  whiskerRight adj₁.unit (G ⋙ L₂) ≫
                                    ((L₁ ⋙ R₁).associator G L₂).inv ≫
                                      whiskerRight (L₁.associator R₁ G).hom L₂ ≫
                                        whiskerRight (L₁.whiskerLeft β.natTrans) L₂ ≫
                                          whiskerRight (L₁.associator H R₂).inv L₂ ≫
                                            ((L₁ ⋙ H).associator R₂ L₂).hom ≫
                                              (L₁ ⋙ H).whiskerLeft adj₂.counit ≫ (L₁ ⋙ H).rightUnitor.hom),
                            left_inv := ⋯, right_inv := ⋯ : TwoSquare G L₁ L₂ H ≃ TwoSquare R₁ H G R₂ } :
                          (a : TwoSquare G L₁ L₂ H) → TwoSquare R₁ H G R₂)
                        α)) ≫
                  (R₃.associator H R₂).inv ≫
                    whiskerRight
                        (natTrans
                          (({
                                toFun := fun (α : TwoSquare H L₃ L₄ K) ↦
                                  TwoSquare.mk R₃ K H R₄
                                    ((R₃ ⋙ H).rightUnitor.inv ≫
                                      (R₃ ⋙ H).whiskerLeft adj₄.unit ≫
                                        (R₃.associator H (L₄ ⋙ R₄)).hom ≫
                                          R₃.whiskerLeft (H.associator L₄ R₄).inv ≫
                                            R₃.whiskerLeft (whiskerRight α.natTrans R₄) ≫
                                              R₃.whiskerLeft (L₃.associator K R₄).hom ≫
                                                (R₃.associator L₃ (K ⋙ R₄)).inv ≫
                                                  whiskerRight adj₃.counit (K ⋙ R₄) ≫ (K ⋙ R₄).leftUnitor.hom),
                                invFun := fun (β : TwoSquare R₃ K H R₄) ↦
                                  TwoSquare.mk H L₃ L₄ K
                                    ((H ⋙ L₄).leftUnitor.inv ≫
                                      whiskerRight adj₃.unit (H ⋙ L₄) ≫
                                        ((L₃ ⋙ R₃).associator H L₄).inv ≫
                                          whiskerRight (L₃.associator R₃ H).hom L₄ ≫
                                            whiskerRight (L₃.whiskerLeft β.natTrans) L₄ ≫
                                              whiskerRight (L₃.associator K R₄).inv L₄ ≫
                                                ((L₃ ⋙ K).associator R₄ L₄).hom ≫
                                                  (L₃ ⋙ K).whiskerLeft adj₄.counit ≫ (L₃ ⋙ K).rightUnitor.hom),
                                left_inv := ⋯, right_inv := ⋯ : TwoSquare H L₃ L₄ K ≃ TwoSquare R₃ K H R₄ } :
                              (a : TwoSquare H L₃ L₄ K) → TwoSquare R₃ K H R₄)
                            β))
                        R₂ ≫
                      (K.associator R₄ R₂).hom)).natTrans.app
        c
⊢ ({
          toFun := fun (α : TwoSquare G (L₁ ⋙ L₃) (L₂ ⋙ L₄) K) ↦
            TwoSquare.mk (R₃ ⋙ R₁) K G (R₄ ⋙ R₂)
              (((R₃ ⋙ R₁) ⋙ G).rightUnitor.inv ≫
                ((R₃ ⋙ R₁) ⋙ G).whiskerLeft
                    (Adjunction.mk'
                        {
                          homEquiv := fun (x : D) (x_1 : F) ↦
                            Equiv.trans (adj₄.homEquiv (L₂.obj x) x_1) (adj₂.homEquiv x (R₄.obj x_1)),
                          unit :=
                            adj₂.unit ≫
                              whiskerRight (L₂.rightUnitor.inv ≫ L₂.whiskerLeft adj₄.unit ≫ (L₂.associator L₄ R₄).inv)
                                  R₂ ≫
                                ((L₂ ⋙ L₄).associator R₄ R₂).hom,
                          counit :=
                            ((R₄ ⋙ R₂).associator L₂ L₄).inv ≫
                              whiskerRight ((R₄.associator R₂ L₂).hom ≫ R₄.whiskerLeft adj₂.counit ≫ R₄.rightUnitor.hom)
                                  L₄ ≫
                                adj₄.counit,
                          homEquiv_unit := ⋯, homEquiv_counit := ⋯ :
                          CoreHomEquivUnitCounit (L₂ ⋙ L₄) (R₄ ⋙ R₂) }).unit ≫
                  ((R₃ ⋙ R₁).associator G ((L₂ ⋙ L₄) ⋙ R₄ ⋙ R₂)).hom ≫
                    (R₃ ⋙ R₁).whiskerLeft (G.associator (L₂ ⋙ L₄) (R₄ ⋙ R₂)).inv ≫
                      (R₃ ⋙ R₁).whiskerLeft (whiskerRight α.natTrans (R₄ ⋙ R₂)) ≫
                        (R₃ ⋙ R₁).whiskerLeft ((L₁ ⋙ L₃).associator K (R₄ ⋙ R₂)).hom ≫
                          ((R₃ ⋙ R₁).associator (L₁ ⋙ L₃) (K ⋙ R₄ ⋙ R₂)).inv ≫
                            whiskerRight
                                (Adjunction.mk'
                                    {
                                      homEquiv := fun (x : A) (x_1 : C) ↦
                                        Equiv.trans (adj₃.homEquiv (L₁.obj x) x_1) (adj₁.homEquiv x (R₃.obj x_1)),
                                      unit :=
                                        adj₁.unit ≫
                                          whiskerRight
                                              (L₁.rightUnitor.inv ≫
                                                L₁.whiskerLeft adj₃.unit ≫ (L₁.associator L₃ R₃).inv)
                                              R₁ ≫
                                            ((L₁ ⋙ L₃).associator R₃ R₁).hom,
                                      counit :=
                                        ((R₃ ⋙ R₁).associator L₁ L₃).inv ≫
                                          whiskerRight
                                              ((R₃.associator R₁ L₁).hom ≫
                                                R₃.whiskerLeft adj₁.counit ≫ R₃.rightUnitor.hom)
                                              L₃ ≫
                                            adj₃.counit,
                                      homEquiv_unit := ⋯, homEquiv_counit := ⋯ :
                                      CoreHomEquivUnitCounit (L₁ ⋙ L₃) (R₃ ⋙ R₁) }).counit
                                (K ⋙ R₄ ⋙ R₂) ≫
                              (K ⋙ R₄ ⋙ R₂).leftUnitor.hom),
          invFun := fun (β : TwoSquare (R₃ ⋙ R₁) K G (R₄ ⋙ R₂)) ↦
            TwoSquare.mk G (L₁ ⋙ L₃) (L₂ ⋙ L₄) K
              ((G ⋙ L₂ ⋙ L₄).leftUnitor.inv ≫
                whiskerRight
                    (Adjunction.mk'
                        {
                          homEquiv := fun (x : A) (x_1 : C) ↦
                            Equiv.trans (adj₃.homEquiv (L₁.obj x) x_1) (adj₁.homEquiv x (R₃.obj x_1)),
                          unit :=
                            adj₁.unit ≫
                              whiskerRight (L₁.rightUnitor.inv ≫ L₁.whiskerLeft adj₃.unit ≫ (L₁.associator L₃ R₃).inv)
                                  R₁ ≫
                                ((L₁ ⋙ L₃).associator R₃ R₁).hom,
                          counit :=
                            ((R₃ ⋙ R₁).associator L₁ L₃).inv ≫
                              whiskerRight ((R₃.associator R₁ L₁).hom ≫ R₃.whiskerLeft adj₁.counit ≫ R₃.rightUnitor.hom)
                                  L₃ ≫
                                adj₃.counit,
                          homEquiv_unit := ⋯, homEquiv_counit := ⋯ : CoreHomEquivUnitCounit (L₁ ⋙ L₃) (R₃ ⋙ R₁) }).unit
                    (G ⋙ L₂ ⋙ L₄) ≫
                  (((L₁ ⋙ L₃) ⋙ R₃ ⋙ R₁).associator G (L₂ ⋙ L₄)).inv ≫
                    whiskerRight ((L₁ ⋙ L₃).associator (R₃ ⋙ R₁) G).hom (L₂ ⋙ L₄) ≫
                      whiskerRight ((L₁ ⋙ L₃).whiskerLeft β.natTrans) (L₂ ⋙ L₄) ≫
                        whiskerRight ((L₁ ⋙ L₃).associator K (R₄ ⋙ R₂)).inv (L₂ ⋙ L₄) ≫
                          (((L₁ ⋙ L₃) ⋙ K).associator (R₄ ⋙ R₂) (L₂ ⋙ L₄)).hom ≫
                            ((L₁ ⋙ L₃) ⋙ K).whiskerLeft
                                (Adjunction.mk'
                                    {
                                      homEquiv := fun (x : D) (x_1 : F) ↦
                                        Equiv.trans (adj₄.homEquiv (L₂.obj x) x_1) (adj₂.homEquiv x (R₄.obj x_1)),
                                      unit :=
                                        adj₂.unit ≫
                                          whiskerRight
                                              (L₂.rightUnitor.inv ≫
                                                L₂.whiskerLeft adj₄.unit ≫ (L₂.associator L₄ R₄).inv)
                                              R₂ ≫
                                            ((L₂ ⋙ L₄).associator R₄ R₂).hom,
                                      counit :=
                                        ((R₄ ⋙ R₂).associator L₂ L₄).inv ≫
                                          whiskerRight
                                              ((R₄.associator R₂ L₂).hom ≫
                                                R₄.whiskerLeft adj₂.counit ≫ R₄.rightUnitor.hom)
                                              L₄ ≫
                                            adj₄.counit,
                                      homEquiv_unit := ⋯, homEquiv_counit := ⋯ :
                                      CoreHomEquivUnitCounit (L₂ ⋙ L₄) (R₄ ⋙ R₂) }).counit ≫
                              ((L₁ ⋙ L₃) ⋙ K).rightUnitor.hom),
          left_inv := ⋯, right_inv := ⋯ } :
        (a : TwoSquare G (L₁ ⋙ L₃) (L₂ ⋙ L₄) K) → TwoSquare (R₃ ⋙ R₁) K G (R₄ ⋙ R₂))
      (TwoSquare.mk G (L₁ ⋙ L₃) (L₂ ⋙ L₄) K
        ((G.associator L₂ L₄).inv ≫
          whiskerRight α.natTrans L₄ ≫
            (L₁.associator H L₄).hom ≫ L₁.whiskerLeft β.natTrans ≫ (L₁.associator L₃ K).inv)) =
    TwoSquare.mk (R₃ ⋙ R₁) K G (R₄ ⋙ R₂)
      ((R₃.associator R₁ G).hom ≫
        R₃.whiskerLeft
            (natTrans
              (({
                    toFun := fun (α : TwoSquare G L₁ L₂ H) ↦
                      TwoSquare.mk R₁ H G R₂
                        ((R₁ ⋙ G).rightUnitor.inv ≫
                          (R₁ ⋙ G).whiskerLeft adj₂.unit ≫
                            (R₁.associator G (L₂ ⋙ R₂)).hom ≫
                              R₁.whiskerLeft (G.associator L₂ R₂).inv ≫
                                R₁.whiskerLeft (whiskerRight α.natTrans R₂) ≫
                                  R₁.whiskerLeft (L₁.associator H R₂).hom ≫
                                    (R₁.associator L₁ (H ⋙ R₂)).inv ≫
                                      whiskerRight adj₁.counit (H ⋙ R₂) ≫ (H ⋙ R₂).leftUnitor.hom),
                    invFun := fun (β : TwoSquare R₁ H G R₂) ↦
                      TwoSquare.mk G L₁ L₂ H
                        ((G ⋙ L₂).leftUnitor.inv ≫
                          whiskerRight adj₁.unit (G ⋙ L₂) ≫
                            ((L₁ ⋙ R₁).associator G L₂).inv ≫
                              whiskerRight (L₁.associator R₁ G).hom L₂ ≫
                                whiskerRight (L₁.whiskerLeft β.natTrans) L₂ ≫
                                  whiskerRight (L₁.associator H R₂).inv L₂ ≫
                                    ((L₁ ⋙ H).associator R₂ L₂).hom ≫
                                      (L₁ ⋙ H).whiskerLeft adj₂.counit ≫ (L₁ ⋙ H).rightUnitor.hom),
                    left_inv := ⋯, right_inv := ⋯ : TwoSquare G L₁ L₂ H ≃ TwoSquare R₁ H G R₂ } :
                  (a : TwoSquare G L₁ L₂ H) → TwoSquare R₁ H G R₂)
                α)) ≫
          (R₃.associator H R₂).inv ≫
            whiskerRight
                (natTrans
                  (({
                        toFun := fun (α : TwoSquare H L₃ L₄ K) ↦
                          TwoSquare.mk R₃ K H R₄
                            ((R₃ ⋙ H).rightUnitor.inv ≫
                              (R₃ ⋙ H).whiskerLeft adj₄.unit ≫
                                (R₃.associator H (L₄ ⋙ R₄)).hom ≫
                                  R₃.whiskerLeft (H.associator L₄ R₄).inv ≫
                                    R₃.whiskerLeft (whiskerRight α.natTrans R₄) ≫
                                      R₃.whiskerLeft (L₃.associator K R₄).hom ≫
                                        (R₃.associator L₃ (K ⋙ R₄)).inv ≫
                                          whiskerRight adj₃.counit (K ⋙ R₄) ≫ (K ⋙ R₄).leftUnitor.hom),
                        invFun := fun (β : TwoSquare R₃ K H R₄) ↦
                          TwoSquare.mk H L₃ L₄ K
                            ((H ⋙ L₄).leftUnitor.inv ≫
                              whiskerRight adj₃.unit (H ⋙ L₄) ≫
                                ((L₃ ⋙ R₃).associator H L₄).inv ≫
                                  whiskerRight (L₃.associator R₃ H).hom L₄ ≫
                                    whiskerRight (L₃.whiskerLeft β.natTrans) L₄ ≫
                                      whiskerRight (L₃.associator K R₄).inv L₄ ≫
                                        ((L₃ ⋙ K).associator R₄ L₄).hom ≫
                                          (L₃ ⋙ K).whiskerLeft adj₄.counit ≫ (L₃ ⋙ K).rightUnitor.hom),
                        left_inv := ⋯, right_inv := ⋯ : TwoSquare H L₃ L₄ K ≃ TwoSquare R₃ K H R₄ } :
                      (a : TwoSquare H L₃ L₄ K) → TwoSquare R₃ K H R₄)
                    β))
                R₂ ≫
              (K.associator R₄ R₂).hom)

Tactic:
ext c