[ add ] Setoid from PartialSetoid

[jamesmckinna]

This tackles one version of how to develop 'subsetoid's via PERs. Cf. #2814

Not necessarily the 'right' way to go, but still functionality which may be useful in the future

UPDATED: to live under Relation.Binary.Construct

[JacquesCarette]

One quibble, but otherwise I like this now.

[jamesmckinna]

I don't know if it would be worse, or better, to have something like

Suggested change

	open import Data.Product.Base using (_,_; Σ; proj₁; proj₂)
	open import Data.Product.Base using (_,_; Σ)
	renaming (proj₁ to ι; proj₂ to x≈x)

so that subsequent definitions can exploit such 'abstract' vocabulary/notation, rather than expose the concrete projection names?

[jamesmckinna]

Or perhaps better still, remove/inline refl as below, and make

ι : Carrier → S.Carrier
ι = proj₁

so that it may subsequently be exported/exportable as such?

[JacquesCarette]

If you're going to go that route (second suggestion), why not bite the bullet and make the thing a record? Post-facto adding aliases for projections is what agda-unimath does... and it eventually leads to unreadable goals.

I like the first suggestion even less.

[jamesmckinna]

Well, in a way, the record-based version is (arguably) cleaner:

record SubSetoid : Set (a ⊔ ℓ) where

  field
    ι    : S.Carrier
    refl : ι S.≈ ι

open SubSetoid public using (ι)

_≈_ : Rel SubSetoid _
_≈_ = S._≈_ on ι

-- Structure

isEquivalence : IsEquivalence _≈_
isEquivalence = record
  { refl = λ {x = x} → SubSetoid.refl x
  ; sym = S.sym
  ; trans = S.trans
  }

-- Bundle

setoid : Setoid _ _
setoid = record { isEquivalence = isEquivalence }

-- Monomorphism

isRelHomomorphism : IsRelHomomorphism _≈_ S._≈_ ι
isRelHomomorphism = record { cong = id }

isRelMonomorphism : IsRelMonomorphism _≈_ S._≈_ ι
isRelMonomorphism = record { isHomomorphism = isRelHomomorphism ; injective = id }

[JacquesCarette]

I certainly would argue so!

[jamesmckinna]

In the interests of clarity: are you saying that you would prefer that it be changed in favour of the record version?

More than happy to do so if so!

[JacquesCarette]

Yes

[jamesmckinna]

Done. I've retained Carrier as the name of the underlying type, but I suppose something else, such as SubSetoid, would work as well. Field name refl is kept hidden, so that its 'rectification' (wrt implicit quantification) as Setoid.refl is the way to access it.

[JacquesCarette]

I must say that I expected the carrier to be called Carrier (and not ι) with the record called something like 'Reflective' or some such.

Thinking some more, I think having a definition for Defined x (expanding to x S.≈ x) might make the overall definition more perspicuous.

[jamesmckinna]

So...

• Carrier (capitalised) is the carrier type; did you envisage carrier (lower-case) for the name of its inhabitant?
  I was motivated by my proposal under Substructures and quotients in the Algebra.* hierarchy #1899 to have a standardised name which then becomes the underlying function of the homo-/mono-morphism injecting Carrier into S.Carrier... but part of my thinking was also that the record itself doesn't merit an 'interesting' name... because it should only be exposed through its Setoid API, when it would moreover, again receive the name Carrier... (and be renamed, presumably, at any client use-site, if needed)
• adding Defined sounds a good suggestion for Relation.Binary.Definitions... DRY says we should then redefine Reflexive in terms of it?

On naming, I think I was struck looking back over #2071 that the carrier type of the symmetric interior is given an 'interesting'/'informative' name, when in fact that's another case (I now think), where the record type is a concrete implementation detail which should only really be accessed/accessible via the API for the Construct being defined... esp. given that the module import path already cues the construction as that of the symmetric interior...

UPDATED: I've gone back over that last paragraph, and it doesn't any longer make sense!? Sorry for the noise!

Let me retry :
#2071 defines a construction on binary relations, not on types, whereas Carrier constructs a type towards building a Setoid, so it's not obvious that it belongs under Construct?

The operating construct on binary relations involved here is simply _on_, but I'd hesitate before putting the derived constructions as Properties of Relation.Binary.Construct.On...?

[jamesmckinna]

D'oh!?

I've ended up defining
subset = equaliser of kernel pair
for a/the special case of the 'inclusion'...

So it is probably better to refactor this as
kernel pair of arbitrary function (Fam again!?), and then specialise that at id?

Or: take a breath and sit on my hands for a bit...

[JacquesCarette]

Good realization - I certainly had not spotted that. Perhaps sitting is indeed wise.

[jamesmckinna]

UPDATED:

• converted to DRAFT
• added Relation.Binary.Construct.Kernel and Relation.Binary.Construct.SubSetoid for consideration

We can discuss where this might go, if and when, ... later.

[JacquesCarette]

I'm still not happy with this record being called Carrier and its 'carrier' field being called h. To me, Carrier will always mean the underlying type of something Setoid-based. So re-using that name confounds expectations.

It feels like Carrier is instead some kind of Index-type with a distinguished point h.

[jamesmckinna]

I'm still not happy with this record being called Carrier and its 'carrier' field being called h. To me, Carrier will always mean the underlying type of something Setoid-based. So re-using that name confounds expectations.

@JacquesCarette I'm reluctant to antagonise the collective wisdom of McMaster any more than I already seem to be doing over order-theoretic concepts, so I'll try to restate my position FTR, and then happily let others decide what becomes of this:

• one of the end products of this PR is precisely to establish Carrier (the record type) as the Carrier (field value) of "something Setoid based", namely the bundle defining the 'subset on which f and g equalise'
• it's clear you don't like the pun; fair enough, but I would never expect this type to be explicitly exported, except through the Setoid interface (cf. [DRY] what's the best way to publicly re-export properties/structure? #2391 ); I guess I could make it private, to improve matters? Alternatively, it could indeed be renamed, but as I say, I regard it as an abstract data type, existing solely to be a choice of domain for the isRelMonomorphism definition... viz. as a way of speaking about 'the subset on which f and g equalise'
• it's conventional, given f, and g defining some diagram (here: a parallel pair with domain I, as per the 'sub-thing as given by a map on indices' construction, to have h, or perhaps better here, k (for Kernel, except that old-timey category theory books tend to use h for the universal equalising map, and k for the corresponding coequalising map in a coequaliser diagram) define the (appropriate) unique mediating morphism (I won't debate uniqueness or otherwise here, given higher-minded, and higher-dimensional, sensitivities about 'uniqueness up to what?'); given the way that field name become projection functions, that, again precisely, establishes h, or whatever we end up calling it, as a function of type Carrier → I, and again, conventionally, in such a way as to fit the diagram of parallel arrows f, g...
• I've proposed/queried elsewhere the use of a standardised idiom for describing the eventual map ι : Carrier → S.Carrier, as, again precisely, corresponding to 'the injection into S of the subset on which f and g equalise', but again, the actual name seems really neither here nor there, but for the fact that, again from the public exports, h is never again mentioned (so its name is similarly immaterial/abstract)

I'd be quite happy to say 'puns considered harmful', and rename everything, but for the fact that these objects/constructions giving rise to the (intended for public export) definitions

• _≈_
• isEquivalence
• setoid
• isRelMonomorphism

do all need to be named. Perhaps it was failure of imagination on my part not to be able to come up with better ones, but in the end, I thought, it turns out mistakenly, that the ones I chose, for the reasons above, made the best 'fit'.

HTH!

It feels like Carrier is instead some kind of Index-type with a distinguished point h.

See above: h defines, as a projection, a function from Carrier to I.

[JacquesCarette]

Making it private would go part of the way, for sure. Some puns I like, but somehow not this one.

The argument "establishing this as the Carrier of ..." doesn't go very far, as it could be extended to so many more things.

Have you considered Equalizer as the name? EqualAt, if we want a less fancy name?