[M1-3] Add community-health files and renumber 2.0 → 3.0

.github/ISSUE_TEMPLATE/bug_report.yml

@@ -0,0 +1,65 @@
+name: Bug report
+description: Report something that's broken in agda-algebras.
+labels: ["bug"]
+body:
+  - type: markdown
+    attributes:
+      value: |
+        Thanks for taking the time to report a bug.  Please fill in the fields below so we can reproduce and diagnose the issue quickly.
+
+  - type: textarea
+    id: what-happened
+    attributes:
+      label: What happened?
+      description: A clear description of the problem.  What did you do?  What did you expect?  What happened instead?
+      placeholder: I ran `make check` and got error X on module Y...
+    validations:
+      required: true
+
+  - type: textarea
+    id: reproduction
+    attributes:
+      label: Minimal reproduction
+      description: The smallest Agda snippet or set of commands that reproduces the issue.  If the issue is environmental, describe your setup.
+      render: shell
+    validations:
+      required: true
+
+  - type: input
+    id: agda-version
+    attributes:
+      label: Agda version
+      description: Output of `agda --version`.
+      placeholder: "Agda version 2.8.0"
+    validations:
+      required: true
+
+  - type: input
+    id: stdlib-version
+    attributes:
+      label: Standard-library version
+      placeholder: "2.3"
+    validations:
+      required: true
+
+  - type: input
+    id: agda-algebras-commit
+    attributes:
+      label: agda-algebras commit
+      description: Output of `git rev-parse --short HEAD`.
+      placeholder: "e.g. a1b2c3d"
+    validations:
+      required: false
+
+  - type: dropdown
+    id: install-method
+    attributes:
+      label: Installation method
+      options:
+        - Nix (`nix develop`)
+        - Agda Python installer
+        - Prebuilt binary from Agda releases
+        - Cabal from Hackage
+        - Other (describe in reproduction section)
+    validations:
+      required: true

.github/ISSUE_TEMPLATE/config.yml

@@ -0,0 +1,5 @@
+blank_issues_enabled: false
+contact_links:
+  - name: Project roadmap
+    url: https://github.com/ualib/agda-algebras/blob/master/docs/GITHUB_PROJECT.md
+    about: See the milestone plan to check whether your contribution fits an existing track before filing an issue.

.github/ISSUE_TEMPLATE/design_discussion.yml

@@ -0,0 +1,42 @@
+name: Design discussion
+description: Propose or debate a design decision.
+labels: ["design-discussion"]
+body:
+  - type: markdown
+    attributes:
+      value: |
+        Design-discussion issues are for questions that need to be settled before code is written — should X be a record or a Σ-type?  Which of two naming conventions should we adopt?  Does Y belong in `Setoid/` or `Classical/`?
+
+        For reference, ratified design decisions are recorded in `docs/adr/` (Architecture Decision Records).
+
+  - type: textarea
+    id: question
+    attributes:
+      label: The question
+      description: What decision needs to be made?
+    validations:
+      required: true
+
+  - type: textarea
+    id: options
+    attributes:
+      label: Options under consideration
+      description: List the options with their tradeoffs.  If you have a preferred option, say which and why.
+    validations:
+      required: true
+
+  - type: textarea
+    id: constraints
+    attributes:
+      label: Constraints and stakeholders
+      description: Who is affected by this decision?  What downstream code depends on it?  Are there backwards-compatibility concerns?
+    validations:
+      required: false
+
+  - type: textarea
+    id: proposal
+    attributes:
+      label: Proposed resolution
+      description: If you have a specific resolution in mind, sketch it here.  If you want to leave it open for discussion, that's fine too.
+    validations:
+      required: false

.github/ISSUE_TEMPLATE/feature_request.yml

@@ -0,0 +1,58 @@
+name: Feature request
+description: Suggest a new definition, theorem, or capability for the library.
+labels: ["enhancement"]
+body:
+  - type: markdown
+    attributes:
+      value: |
+        Thanks for suggesting something for agda-algebras.  Before you fill this out, please check the project roadmap in [`docs/GITHUB_PROJECT.md`](https://github.com/ualib/agda-algebras/blob/master/docs/GITHUB_PROJECT.md) — the change you're proposing may already be planned.
+
+  - type: textarea
+    id: what
+    attributes:
+      label: What are you proposing?
+      description: A clear description of the definition, theorem, or capability you'd like to see added.
+    validations:
+      required: true
+
+  - type: textarea
+    id: why
+    attributes:
+      label: Why is this useful?
+      description: What can users do with this that they can't do now?  What does it enable downstream?
+    validations:
+      required: true
+
+  - type: textarea
+    id: mathematical-context
+    attributes:
+      label: Mathematical context
+      description: If this is a formalization of existing mathematics, cite the source (textbook and page, or paper and theorem number).  If it's novel, say so.
+    validations:
+      required: false
+
+  - type: dropdown
+    id: tree
+    attributes:
+      label: Which tree does this belong in?
+      options:
+        - "Setoid/ (canonical for 3.0)"
+        - "Classical/ (planned; specific algebraic theories)"
+        - "Cubical/ (planned; long-term 4.0 target)"
+        - "Base/ (legacy; new code not accepted here)"
+        - "Not sure"
+    validations:
+      required: true
+
+  - type: dropdown
+    id: milestone-fit
+    attributes:
+      label: Does this fit an existing milestone?
+      options:
+        - "M3 — Classical structures"
+        - "M6 — FLRP prerequisites"
+        - "M7 — CSP (finite templates)"
+        - "M9 — Applications of continuous relations"
+        - Other / none
+    validations:
+      required: false

.github/PULL_REQUEST_TEMPLATE.md

@@ -0,0 +1,40 @@
+<!--
+Thanks for contributing to agda-algebras.
+
+Please keep PRs focused — one coherent change per PR.  If you find yourself
+writing a long list below, consider whether the work would be easier to
+review as a sequence of smaller PRs.
+-->
+
+## Summary
+
+<!-- What does this PR do, in one or two sentences? -->
+
+## Related issues
+
+Closes #
+
+<!-- Or "Part of #" if this is one of several PRs addressing an issue. -->
+
+## Type of change
+
+- [ ] Bug fix
+- [ ] New definition, theorem, or feature
+- [ ] Refactoring / cleanup (no user-facing change)
+- [ ] Documentation
+- [ ] Infrastructure (CI, Nix, build)
+- [ ] Other
+
+## Checklist
+
+- [ ] `make check` passes locally under `nix develop`.
+- [ ] New public definitions have prose comment blocks.
+- [ ] Commits are coherent and have explanatory messages.
+- [ ] If this PR touches the `src/` tree, the change is targeted at `Base/`, `Setoid/`, or the shared `Overture/` foundation.
+- [ ] If this PR introduces new notation, it doesn't conflict with notation already used elsewhere in the library.
+
+## Notes for reviewers
+
+<!-- Anything specific you'd like the reviewer to focus on?  Known limitations?  Open questions? -->
+
+

CHANGELOG.md

@@ -0,0 +1,52 @@
+# Changelog
+
+All notable changes to agda-algebras are documented in this file.
+
+The format follows [Keep a Changelog](https://keepachangelog.com/en/1.1.0/) and this project aspires to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
+
+## [Unreleased] — 3.0 development
+
+The 3.0 release is a major reconstruction of agda-algebras building on the Setoid-based redevelopment that shipped in v2.0.1 (December 2021).  Work is organized into milestones tracked in [`docs/GITHUB_PROJECT.md`](docs/GITHUB_PROJECT.md).
+
+### Added
+
++  **Setoid-canonical tree.**  `src/Setoid/` is the canonical development tree for 3.0.
++  **Nix flake** at the repo root pinning Agda 2.8.0 and standard-library 2.3, so `nix develop` provides a reproducible development environment.
++  **`INSTALL.md`** as the canonical installation guide.
++  **GitHub Actions CI** (`.github/workflows/ci.yml`) that type-checks the library on every push and pull request.
++  **Community-health files**: `CONTRIBUTING.md`, `CODE_OF_CONDUCT.md`, issue templates, pull-request template.
++  **Dual license**: Apache 2.0 for source code under `src/`, CC BY 4.0 for documentation under `docs/`.
+
+### Changed
+
++  **Agda target**: 2.6.2 → 2.8.0.
++  **Standard library target**: 1.7 → 2.3.
++  **Pragma**: `--without-K` → `--cubical-compatible` across the tree.  See `docs/lagda/Overture/Basic.lagda` for the reasoning.
++  **Documentation directory**: `doc/` → `docs/` following modern conventions.
++  **README**: rewritten for the 3.0 line.
+
+### Deprecated
+
++  **`docs/INSTALL_AGDA.md`** superseded by `INSTALL.md`.  Retained with a deprecation banner; will be removed in a future release.
+
+### Removed
+
+Nothing removed yet in this cycle.
+
+### Fixed
+
+Nothing to report.  3.0 is a forward-looking reconstruction rather than a bug-fix release.
+
+---
+
+## [2.0.1] — 2021-12-07
+
+Archival release coinciding with the TYPES 2021 submission.  This version was the first to use the Setoid-based formulation, reconstructed from the earlier UALib project.  Archived on Zenodo: [DOI 10.5281/zenodo.5765793](https://doi.org/10.5281/zenodo.5765793).
+
+Targets Agda 2.6.2 and standard-library 1.7.
+
+---
+
+## [1.x and earlier]
+
+The earlier UALib library (GitLab-hosted) and the pre-v2.0.1 agda-algebras work.  No per-version changelog was maintained; see the git log and the related papers for details.

CODE_OF_CONDUCT.md

@@ -0,0 +1,71 @@
+# Contributor Covenant Code of Conduct
+
+## Our Pledge
+
+We pledge to make our community welcoming, safe, and equitable for all.
+
+We are committed to fostering an environment that respects and promotes the dignity, rights, and contributions of all individuals, regardless of characteristics including race, ethnicity, national origin, language, sex, gender identity and expression, sexual orientation, disability, neurotype, physical appearance, body size, caste, age, religion, citizenship, migratory status, economic status, ability level, and any other dimension of diversity.
+
+By embracing these values and committing to our ethical responsibilities, we create an environment that welcomes all people to participate in, contribute to, and benefit from our project.
+
+## Encouraged Behaviors
+
+Community members are encouraged to engage in the following behaviors:
+
++  Demonstrating empathy and kindness toward other people.
++  Communicating respectfully, welcoming differing viewpoints and experiences.
++  Giving and gracefully accepting constructive feedback.
++  Accepting responsibility for our mistakes, apologizing to those affected, and learning from the experience.
++  Focusing on what is best not just for us as individuals, but for the community as a whole.
++  Using welcoming and inclusive language.
+
+## Restricted Behaviors
+
+The following behaviors are unacceptable within our community:
+
++  **Engaging in bigotry.**  Expressing animosity toward or derogating people based on a social characteristic, as described in the Pledge above, will not be tolerated.
++  **Harassing others.**  Harassment includes sustained or willful disruption; stalking; publishing private information without permission; sexual attention or contact without clear consent; trolling, insulting, or derogatory comments; and sustained disruption of community discussion.
++  **Abusing power.**  Power includes institutional, social, and informal power.  Manipulation, coercion, retaliation, and exploitation of power imbalances are unacceptable.
++  **Endangering others.**  Threats, incitement of violence, and doxxing are unacceptable.
+
+## Reporting an Issue
+
+If you experience or witness behavior that violates this Code of Conduct, please report it by emailing [williamdemeo at gmail](mailto:williamdemeo@gmail.com).
+
+Reports will be reviewed by the project maintainers.  We will keep reports confidential to the extent possible while still enabling an appropriate response, and we will respond to the reporter within one week.
+
+If your report concerns a maintainer, you may contact [Jacques Carette](https://www.cas.mcmaster.ca/~carette/) as an alternative.
+
+## Addressing and Repairing Harm
+
+Community moderators will determine consequences for violations based on the nature and severity of the violation, using the following guidelines:
+
+### Correction
+
+*Community impact*: use of inappropriate language or other behavior deemed unprofessional or unwelcome.
+*Consequence*: a private, written warning from the maintainers providing clarity around the nature of the violation and why the behavior was inappropriate.  A public apology may be requested.
+
+### Warning
+
+*Community impact*: a violation through a single incident or series of actions.
+*Consequence*: a warning with consequences for continued behavior.  No interaction with the people involved, including unsolicited interaction with those enforcing the Code of Conduct, for a specified period of time.  Violating these terms may lead to a temporary or permanent ban.
+
+### Temporary Ban
+
+*Community impact*: a serious violation of community standards, including sustained inappropriate behavior.
+*Consequence*: a temporary ban from any sort of interaction or public communication with the community for a specified period of time.
+
+### Permanent Ban
+
+*Community impact*: demonstrating a pattern of violation of community standards, including sustained inappropriate behavior or harassment of an individual, or aggression toward or disparagement of classes of individuals.
+*Consequence*: a permanent ban from any sort of public interaction within the community.
+
+## Scope
+
+This Code of Conduct applies within all community spaces (issues, pull requests, discussions, and any related communication channels), and also applies when an individual is officially representing the community in public spaces.
+
+## Attribution
+
+This Code of Conduct is adapted from the [Contributor Covenant 3.0](https://www.contributor-covenant.org/version/3/0/code_of_conduct/), authored by the Organization for Ethical Source.
+
+