Definition action_on_bimodule_ob_mor : disp_cat_ob_mor (total_twosided_disp_category bimodule_abgr). Proof. simple refine (_ ,, _). - exact (λ B, let R₁ := (pr1 B : commring) in let G := (pr22 B : abgr) in let R₂ := (pr12 B : commring) in R₁ → G → R₂ → G). - cbn. exact (λ B₁ B₂, let R₁ := (pr1 B₁ : commring) in let G := (pr22 B₁ : abgr) in let R₂ := (pr12 B₁ : commring) in let S₁ := (pr1 B₂ : commring) in let H := (pr22 B₂ : abgr) in let S₂ := (pr12 B₂ : commring) in λ (μ₁ : R₁ → G → R₂ → G) (μ₂ : S₁ → H → S₂ → H) f, let f₁ := (pr1 f : R₁ → S₁) in let f₂ := (pr12 f : R₂ → S₂) in let g := (pr22 f : G → H) in ∏ (x : R₁) (y : G) (z : R₂), g (μ₁ x y z) = μ₂ (f₁ x) (g y) (f₂ z)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Groups. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.Abgr. Require Import UniMath.CategoryTheory.Categories.Commring. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Total. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.Constant. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.DispCatOnTwoSidedDispCat.