From 2ec50ea46538e60bfc76cc6bd66bf9951f7b9903 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 9 Oct 2023 14:46:59 +0200 Subject: [PATCH] Update src/set-theory/countable-sets.lagda.md Co-authored-by: Egbert Rijke --- src/set-theory/countable-sets.lagda.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/set-theory/countable-sets.lagda.md b/src/set-theory/countable-sets.lagda.md index 5e6ee66763..44accd6a8c 100644 --- a/src/set-theory/countable-sets.lagda.md +++ b/src/set-theory/countable-sets.lagda.md @@ -178,7 +178,8 @@ module _ decidable-subprojection-ℕ-enumeration : enumeration X → decidable-subprojection-ℕ X - pr1 (pr1 (decidable-subprojection-ℕ-enumeration (f , H)) n) = f n ≠ inr star + pr1 (pr1 (decidable-subprojection-ℕ-enumeration (f , H)) n) = + f n ≠ inr star pr1 (pr2 (pr1 (decidable-subprojection-ℕ-enumeration (f , H)) n)) = is-prop-neg pr2 (pr2 (pr1 (decidable-subprojection-ℕ-enumeration (f , H)) n)) =