From 44ac5e1dade12e6f1fe4db7c4ad54b09462f6d46 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 10 Oct 2024 18:50:12 +0100 Subject: [PATCH] rename istrunc_inhabited_istrunc Signed-off-by: Ali Caglayan --- theories/Basics/Trunc.v | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/theories/Basics/Trunc.v b/theories/Basics/Trunc.v index 622e519bc1..74b010ca60 100644 --- a/theories/Basics/Trunc.v +++ b/theories/Basics/Trunc.v @@ -536,12 +536,9 @@ Proof. 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. +Definition istrunc_inhabited_istrunc {n : trunc_index} + {A : Type} (H : A -> IsTrunc n.+1 A) + : IsTrunc n.+1 A + := istrunc_S _ (fun a b => H a a b). (** If you are looking for a theorem about truncation, you may want to read the note "Finding Theorems" in "STYLE.md". *)