Definition end_right_map : ProdF --> ProdM. Proof. use ProductArrow. intro f ; cbn. refine (ProductPr _ _ _ (pr12 f) · #F (_ ,, _)). - exact (pr22 f). - exact (identity _). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.OppositeCategory.Core. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Equalizers.