(R : Ring) := nat. Global Instance isgraph_matrixcat {R : Ring} : IsGraph ( R) := {| Hom := Matrix R |}. Global Instance is01cat_matrixcat {R : Ring} : Is01Cat ( R). Proof. snrapply Build_Is01Cat. - exact (identity_matrix R). - intros l m n M N. exact (matrix_mult N M). Defined.
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.