added istrunc_self_implies_istrunc

HoTT · Oct 9, 2024 · 30fd00a · 30fd00a
1 parent 9ed2b66
commit 30fd00a
Showing 1 changed file with 9 additions and 0 deletions.
diff --git 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". *)