Setoid on `Σ Carrier P` via `proj₁` ?

[mechvel]

A question: what has standard library to replace the following definition?

setoid₁Σ :  ∀ {α α= β} → (A : Setoid α α=) → (P : (Setoid.Carrier A) → Set β) →    
                                        Setoid (α ⊔ β) _                 
-- Setoid on  Σ Carrier P  defined as the projection to  Carrier.                 
-- For example, the setoid of nonzero elements in ℕ.          
                                                                                  
setoid₁Σ  A P =  record{ Carrier = Σ Carrier P;  ... }                       
  where                                                                           
  open Setoid A using (_≈_;  Carrier)
              
  _='_ :   Rel (Σ Carrier P) _                                                           
  _='_ =   _≈_ on proj₁
  ...                                                            

[MatthewDaggitt]

No we don't. Such a construct could live under Relation.Binary.Construct.Subset. Feel free to open a PR

[mechvel]

This time I tried to do a small PR. I follow the guide by G. Allais:

How to do a small PR:

> git checkout master
> git pull
> git checkout -b my_shiny_feature
> emacs src/THE_AGDA_FILE_I_WANT_TO_MODIFY.agda
> emacs CHANGELOG.md
> git add -p
> git commit
> git push origin -u my_shiny_feature

And then open a PR on github.

OK,

1. I included there the commands make clean, fix-whitespace, make test.
2. I start all this from my current fork, which is not a clone of master.
   And git pull has lead to that that this my fork has merged with something.
   And it has now my intended Relation.Binary.Construct.Sigma
   and also, for example, Data.Nat.Binary.Subtraction which was initially on this fork.
   And this Subtraction has been earlier merged by Matthew, with changing it, to somewhere, but not to master. Because I do not see this Subtraction on master.
3. I have forgotten to delete a backup Construct.Sigma.agda~.

So that some things have got confused.
And there remain the two questions.
(I) Really is this a way to do a small PR of Relation.Binary.Construct.Sigma ?
(II) Matthew has changed Binary.Subtraction, agreed this with me, and wrote that he is going to merge it (to where?). And I do not see Binary.Subtraction in master.
I intend to do a commit of Binary.DivMod on top of master. But it uses Subtraction.
Meanwhile, I try a PR of Construct.Sigma.
How to resolve all these overlaps?

[ajrouvoet]

If you want to make a standalone PR for the Subset module that does not depend on other changes, you can always make a fresh clone of the stdlib, make a fresh branch there. That way your two projects don't interact and it is easy to work on both in parallel if you want.

You can ask these questions also on IRC or on gitter, because they are independent of the discussions on the content of these issues.

[gallais]

The whole point of branches is that you should not need to clone the repository
again and again. I don't know what @mechvel did but if you worked on feature1 on
a branch1 and you start by checking out master, pulling to update it and then
creating branch2 for feature2 it should all be independent!

Anyway, I won't get into more details: we are circling back to the problem of
investing a couple of hours to learn the basics of git rather than expecting
people to provide magic commands at a distance while having no knowledge of
the exact circumstances of your setup.

[ajrouvoet]

Spending some time to learn git would obviously be the more stable solution, I agree of course.