Skip to content
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

Jump to bottom

major refactoring #241

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

major refactoring #241

wants to merge 1 commit into from

Conversation

williamdemeo
Copy link
Member

@williamdemeo williamdemeo commented Nov 9, 2023 •
edited
Loading

  • make compatible with Agda 2.6.4
  • make compatible with agda-stdlib 2.0
  • rename some level variables using new convention
    • α -> a
    • β -> b
    • ρᵃ -> α
    • ρᵇ -> β

@williamdemeo
major refactoring
24b55df 
- [X] make compatible with Agda 2.6.4
- [X] make compatible with agda-stdlib 2.0
- [X] renamed some level variables using new convention
   - [X] α -> a
   - [X] β -> b
   - [X] ρᵃ -> α
   - [X] ρᵇ -> β
JacquesCarette
JacquesCarette approved these changes Nov 11, 2023
View reviewed changes
Copy link
Collaborator

@JacquesCarette JacquesCarette left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice. I agree that the two 'TODO's should really be done before this is merged.

williamdemeo
williamdemeo commented Nov 13, 2023
View reviewed changes
src/Base/Functions/Surjective.lagda
where
imgfy→A : Image f ∋ y → Σ[ a ∈ A ] f a ≡ y
imgfy→A (eq a p) = a , sym p
-- `fE y` is a proof of `Image f ∋ y `
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
-- `fE y` is a proof of `Image f ∋ y `

williamdemeo
williamdemeo commented Nov 13, 2023
View reviewed changes
src/Demos/HSP.lagda
@@ -189,10 +189,10 @@ We reproduce the definitions and prove some of their properties inside the next
module _ {𝑨 : Setoid α ρᵃ}{𝑩 : Setoid β ρᵇ} where
open Setoid 𝑨 using () renaming ( _≈_ to _≈ᴬ_ )
open Setoid 𝑩 using () renaming ( _≈_ to _≈ᴮ_ )
open FD _≈ᴬ_ _≈ᴮ_
open FD -- _≈ᴬ_ _≈ᴮ_
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
open FD -- _≈ᴬ_ _≈ᴮ_
open FD

williamdemeo
williamdemeo commented Nov 13, 2023
View reviewed changes
src/Setoid/Homomorphisms/Factor.lagda
(f ̂ 𝑩)(g ∘ (h⁻¹ ∘ c)) ∎
φcomp {f}{c} = trans₂ i (trans₂ ii (trans₂ iii iv))
where
-- TODO: refactor this proof using the new relational reasoning syntax
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Refactor this proof before merge.

williamdemeo
williamdemeo commented Nov 13, 2023
View reviewed changes
src/Setoid/Varieties/Properties.lagda
where private f = _⟨$⟩_ ∣ fh ∣ ; g = _⟨$⟩_ ∣ gh ∣
⊧-I-invar Apq (mkiso fh gh f∼g g∼f) ρ = trans i $ trans ii $ trans iii $ trans iv v
where
-- TODO: refactor this proof using new relational reasoning syntax/style
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Refactor this proof before merge.

@williamdemeo
Copy link
Member Author

williamdemeo commented Nov 13, 2023 •
edited
Loading

@JacquesCarette Thank you for continuing to care about this project and commenting on PRs. I really appreciate your input! 🤗

A couple of issues with this PR (recorded here for my own reference), to be addressed before merging:

  1. Refactor proofs marked "TODO".
  2. Incorporate the above suggested minor changes (which simply remove commented-out code).
  3. Remove notation changes (α -> a, β -> b, etc.) from this PR and make a new one solely for notation changes.
  4. Make a new permanent branch off of the latest master; call it something like "Agda 2.6.3/1.7.2".
  5. Make a new "official release" of agda-algebras based off latest master, in case anyone wants to use the library with Agda 2.6.3 and Agda Standard Library 1.7.2.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@JacquesCarette JacquesCarette JacquesCarette approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@williamdemeo @JacquesCarette