{R : Ring} {e f : R} `{IsIdempotent R e, IsIdempotent R f} : _ <~> IsOrthogonal R e f := ltac:(issig). Global Instance ishprop_isorthogonal R e f `{IsIdempotent R e, IsIdempotent R f} : IsHProp (IsOrthogonal R e f). Proof. exact (istrunc_equiv_istrunc _ ). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids. Require Import Basics.Equivalences Basics.Trunc Types.Sigma WildCat.Core. Require Import Nat.Core Rings.Ring.