3 Pull requests merged by 2 people

• [ refactor ] Rename Algebra.Lattice.Properties.BooleanAlgebra.{⊥≉⊤,⊤≉⊥}

  #2686 merged Mar 27, 2025

• [ add ] wellfoundedness of Relation.Binary.Construct.Add.Infimum.Strict

  #2683 merged Mar 27, 2025

• [Refactor] imports to use Relation.Nullary.Irrelevant

  #2676 merged Mar 23, 2025

3 Issues closed by 2 people

• [ refactor ] Simplify `Data.List.Relation.Binary.Lex.NonStrict.<-asymmetric`

  #2679 closed Mar 28, 2025

• two names in "Algebra.Lattice.Properties.BooleanAlgebra" are confusing

  #2685 closed Mar 27, 2025

• [ add ] well-foundedness of the lifting of a relation to `Maybe`?

  #2682 closed Mar 22, 2025

1 Issue opened by 1 person

• [ refactor ] rationalise the common APIs for `List` and `Vec` versions of `Data.*.Relation.Binary.Lex.*`

  #2687 opened Mar 28, 2025

13 Unresolved conversations

Sometimes conversations happen on old items that aren’t yet closed. Here is a list of all the Issues and Pull Requests with unresolved conversations.

• [ refactor ] Revise definitions, consequences, and use, of `Algebra.Definitions.(Almost)*Cancellative`

  #2573 commented on Mar 27, 2025 • 10 new comments

• [ refactor ] deprecate `Algebra.Structures.IsGroup.{uniqueˡ-⁻¹|uniqueʳ-⁻¹}` with knock-ons for `Algebra.Module.*`

  #2571 commented on Mar 27, 2025 • 6 new comments

• [ add ] `Relation.Binary.Properties.PartialSetoid`

  #2678 commented on Mar 27, 2025 • 4 new comments

• [ refactor ] (Re)define `(Is)TightApartness` and `(Is)HeytingCommutativeRing`/`(Is)HeytingField`

  #2588 commented on Mar 25, 2025 • 1 new comment

• Snoclists?

  #2684 commented on Mar 25, 2025 • 0 new comments

• Optimising `Setoid`s/reasoning by 'rewriting' otherwise higher-dimensional equalities

  #2629 commented on Mar 28, 2025 • 0 new comments

• [ refactor ] Exchange components of `Relation.Binary.Definitions._Respects₂_`

  #2515 commented on Mar 24, 2025 • 0 new comments

• [ refactor ] rectify binder names in `Relation.Binary.Definitions`

  #2552 commented on Mar 24, 2025 • 0 new comments

• [ refactor ] fixes #2568; proves full symmetry for `Bijection`

  #2569 commented on Mar 24, 2025 • 0 new comments

• [ refactor ] Add equality as a parameter to `Algebra.Consequences.Base`

  #2572 commented on Mar 24, 2025 • 0 new comments

• [ refactor ] Symmetry of `Bijection` as a consequence of properties of a given `Surjective` function

  #2583 commented on Mar 25, 2025 • 0 new comments

• [ refactor ] use `variable`s in `Algebra.Consequences.Base`

  #2592 commented on Mar 24, 2025 • 0 new comments

• [ refactor ] Redefine `Relation.Binary.Definitions.Adjoint`, plus knock-on `Function.Consequences`

  #2599 commented on Mar 24, 2025 • 0 new comments