(R : Ring@{i}) (n : nat) : Ring. Proof. snrapply Build_Ring. - exact (abgroup_matrix R n n). - exact matrix_mult. - exact (identity_matrix R n). - exact (associative_matrix_mult R n n n n). - exact (left_distribute_matrix_mult R n n n). - exact (right_distribute_matrix_mult R n n n). - exact (left_identity_matrix_mult R n n). - exact (right_identity_matrix_mult R n n). 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.