We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
CHANGELOG
1 parent 7069d03 commit 4e87466Copy full SHA for 4e87466
CHANGELOG.md
@@ -151,7 +151,7 @@ Additions to existing modules
151
does-≡ : (a? b? : Dec A) → does a? ≡ does b?
152
```
153
154
-* In `Relation.Nullary.Properties`:
+* In `Relation.Unary.Properties`:
155
```agda
156
map : P ≐ Q → Decidable P → Decidable Q
157
does-≐ : P ≐ Q → (P? : Decidable P) → (Q? : Decidable Q) → does ∘ P? ≗ does ∘ Q?
0 commit comments