Build_Matrix' (R : Type) (m n : nat) (l : list (list R)) (wf_row : length l = m) (wf_col : for_all (fun row => length row = n) l) : Matrix R m n. Proof. snrefine (_; _). - snrapply list_sigma. + exact l. + exact wf_col. - by lhs nrapply length_list_sigma. 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.