diff --git a/theories/Basics/Trunc.v b/theories/Basics/Trunc.v index 2eea849982..622e519bc1 100644 --- a/theories/Basics/Trunc.v +++ b/theories/Basics/Trunc.v @@ -535,4 +535,13 @@ Proof. exact (equiv_iff_hprop_uncurried (iff_contr_hprop A)). Defined. +(** If a type [A] implies that it is [n.+1]-truncated, then it is [n.+1]-truncated. **) +Definition istrunc_self_implies_istrunc {n : trunc_index} {A : Type} (H : A -> IsTrunc n.+1 A) + : IsTrunc n.+1 A. +Proof. + apply istrunc_S. + intros a b. + exact (H a a b). +Defined. + (** If you are looking for a theorem about truncation, you may want to read the note "Finding Theorems" in "STYLE.md". *)