{R S T : Type} {m n} (f : R -> S -> T) : Matrix R m n -> Matrix S m n -> Matrix T m n := fun M N => Build_Matrix T m n (fun i j _ _ => f (entry M i j) (entry N i j)).
Require Import Basics.Overture Basics.Trunc Basics.Tactics Basics.Decidable. Require Import Types.Sigma. Require Import Spaces.List.Core Spaces.List.Theory Spaces.List.Paths. Require Import Algebra.Rings.Ring Algebra.Rings.Module Algebra.Rings.CRing Require Import abstract_algebra. Require Import WildCat.Core WildCat.Paths. Require Import Modalities.ReflectiveSubuniverse.