proposition: Lemma iso_leibnitz : forall P : Operations -> Type, P A -> P B.
proof: Proof. intros P;apply transport. first [exact iso_same_semirings|exact iso_same_semirings@{V V}]. Qed.
imports: HoTT.Types.Arrow HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.rings