Skip to content

parity is a Semiring homomorphism #1894

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 16 commits into from
Jan 9, 2023
Merged

parity is a Semiring homomorphism #1894

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
99fa423
added homomorphism proofs
jamesmckinna Dec 21, 2022
a520e5a
narrowed imports
jamesmckinna Dec 21, 2022
f7bfeba
[resolves #1333] writer transformer (#1850)
Dec 30, 2022
af53887
Merge branch 'parity-bis' of https://github.com/jamesmckinna/agda-std…
jamesmckinna Dec 30, 2022
bc74839
removed redundant brackets; fixed lemma dependency; symmetrised appea…
jamesmckinna Dec 30, 2022
86e21e8
streamlined imports
jamesmckinna Dec 30, 2022
3e2a093
further import tweaks
jamesmckinna Dec 30, 2022
47ac8bc
removed original file; rolled contents into `Properties`
jamesmckinna Dec 30, 2022
12c955f
updated `CHANGELOG`
jamesmckinna Dec 30, 2022
9857182
removed redundant parentheses
jamesmckinna Dec 30, 2022
1c9859c
fixed errant merge, I hope
jamesmckinna Dec 30, 2022
64bc521
Revert "[resolves #1333] writer transformer (#1850)"
jamesmckinna Dec 30, 2022
a5c1203
hopefully it's fixed this time around
jamesmckinna Dec 30, 2022
2c7d1ee
removed original file
jamesmckinna Dec 30, 2022
4aaab59
formatting spaces in equational reasoning
jamesmckinna Dec 30, 2022
282f3a7
formatting spaces in equational reasoning
jamesmckinna Dec 30, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 11 additions & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1991,6 +1991,17 @@ Other minor changes
pattern `suc x = con (quote ℕ.suc) (x ⟨∷⟩ [])
```

* Added new proofs in `Data.Parity.Properties`:
```agda
suc-homo-⁻¹ : (parity (suc n)) ⁻¹ ≡ parity n
+-homo-+ : parity (m ℕ.+ n) ≡ parity m ℙ.+ parity n
*-homo-* : parity (m ℕ.* n) ≡ parity m ℙ.* parity n
parity-isMagmaHomomorphism : IsMagmaHomomorphism ℕ.+-rawMagma ℙ.+-rawMagma parity
parity-isMonoidHomomorphism : IsMonoidHomomorphism ℕ.+-0-rawMonoid ℙ.+-0-rawMonoid parity
parity-isNearSemiringHomomorphism : IsNearSemiringHomomorphism ℕ.+-*-rawNearSemiring ℙ.+-*-rawNearSemiring parity
parity-isSemiringHomomorphism : IsSemiringHomomorphism ℕ.+-*-rawSemiring ℙ.+-*-rawSemiring parity
```

* Added new rounding functions in `Data.Rational.Base`:
```agda
floor ceiling truncate round ⌊_⌋ ⌈_⌉ [_] : ℚ → ℤ
Expand Down
Loading