Unary integers

Signed-off-by: Ali Caglayan <[email protected]>
HoTT · May 18, 2024 · 0938eee · 0938eee
1 parent 3956d68
commit 0938eee
Show file tree

Hide file tree

Showing 4 changed files with 489 additions and 4 deletions.
diff --git a/theories/Basics/Decidable.v b/theories/Basics/Decidable.v
@@ -121,6 +121,14 @@ Global Instance decidable_empty : Decidable Empty
 
 (** ** Transfer along equivalences *)
 
+Definition decidable_iff {A B} (f : A -> B) (f' : B -> A)
+  : Decidable A -> Decidable B.
+Proof.
+  intros [a|na].
+  - exact (inl (f a)).
+  - exact (inr (fun b => na (f' b))).
+Defined.
+
 Definition decidable_equiv (A : Type) {B : Type} (f : A -> B) `{IsEquiv A B f}
 : Decidable A -> Decidable B.
 Proof.