{R : Ring@{i}} {n : nat} {M : Matrix R n n} : _ <~> IsDiagonal M := ltac:(issig). Global Instance ishprop_isdiagonal {R : Ring@{i}} {n : nat} (M : Matrix R n n) : IsHProp (IsDiagonal M). Proof. snrapply hprop_allpath. intros x y. snrapply ((equiv_ap' ^-1%equiv _ _ )^-1%equiv). rapply path_sigma_hprop; cbn. apply isinj_matrix_diag. exact ((isdiagonal_diag M)^ @ isdiagonal_diag 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.