Lemma seqsonisaset ( A : hSet ) : isaset ( seqson A ). Proof. intros. unfold seqson. change ( isofhlevel 2 ( nat -> A ) ). apply impredfun. apply (pr2 A). Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.