[ add ] Upwards- and downwards- closed subsets of a given ordered set

[jamesmckinna]

DRAFT

• Subsets are a pain
• Sigma types are a pain
• Insisting on setoids (and hence: Sigma types, else Data.Refinement types, but then the ergonomics of irrelevance gets differently painful?) rather than partial setoids to capture 'sub'-ness is also something of a pain...

Issue: it would be 'useful' infrastructure to add the objects of the issue title, but the design choices are... various, and variously debatable.

Added: label subsets because this may become a pervasive problem going forward?

[JacquesCarette]

I'd say

• 'on the nose' subsets are a pain in dependent type theory, because they need to be encoded via a predicate
• subsets of X encoded as (Y, injection from Y to X) are actually not so bad to work with.

These are, of course, equivalent. But the ergonomics differ a lot. I guess this is yet more Fam-Pow stuff.

[jamesmckinna]

Thanks @JacquesCarette . I guess I shouldn't have opened a 'draft' issue when my thoughts had not yet crystallised.
Trying to define {y : A | x ≲ y} initially stumbled on the realisation that any naive definition of this would only be a partial setoid if A were taken as the Carrier, and hence not able to be an instance of IsPreorder etc., because of our axiomatisation in terms of IsEquivalence as the basis for Relation.Binary.Structures...

... so one solution (a canonical choice of Fam-style injection: proj₁) would be first to define 'Setoid from PartialSetoid' as a Relation.Binary.Construct (or else as additional lemmas in Relation.Binary.Properties.PartialSetoid... which I now got as far as developing), and then define upward closed subset in terms of the obvious partial equivalence structure? Cf. #2816

[JacquesCarette]

My instinct here is that design smells strongly of classical-math / set-theoretical thinking, and may not lead to improvements in MLTT.

[jamesmckinna]

Re: orthodox set-theoretical thinking.
I guess so, given that our Function/Algebra hierarchies are themselves based on Setoids...
... but as I comment on #2796 until we extend such constructions to such a Setoid-based view, it's not clear how the Fam/Pow choice really cashes out; making the family map of a 'Fam-subset' injective (either by design, or by definition as change-of-base of the codomain equivalence along the family map) might help, but such a thing is itself going to only yield a PER on the domain, so a construction such as the one in #2813 might be useful/necessary in order to fit into the Function hierarchy?
Lifting to upwards-/downwards-closed subsets, via an order monomorphism, gives rise to similar phenomena, or can such things be avoided?

[JacquesCarette]

Hoping that @TOTBWF will opine here - he's done more work on this than I have (Order, PER, etc).

[TOTBWF]

Partial setoids move the problem of partiality to maps between partial setoids. There are a bunch of options here, and all of them are varying degrees of tricky:

1. A map A → B of partial setoids is a function A.Carrier → B.Carrier that is congruent with respect to the equivalence relations. This option is pretty blatantly incorrect IMO, as you are still forced to define the function outside of the domain of definition imposed by A's PER.
2. A map A → B is a function f : ∀ (x : A.Carrier) → x A.≈ x → B along with a separate proof of congruence. This is going to be a bit wonky in agda-stdlib, as our setoids use a type-valued equivalence relation, so we really do need to worry about which proof of x A.≈ x we use. Absent some extra coherence proofs, I think this is going to be really unpleasant.
3. A variation of (1) and (2) that omits congruence from the definition of the maps, and instead imposes a partial equivalence relation on the types of maps A.Carrier → B.Carrier (f : ∀ (x : A.Carrier) → x A.≈ x → B, resp) that says
   that f ≈ g when ∀ x y → x A.≈ y → f x A.≈ g y. This means that a map that isn't congruent is going to not be equal to itself, and thus "undefined".
4. A map A → B is a functional relation of partial setoids, EG: a relation R : A.Carrier → B.Carrier → Type κ that is:

• Congruent: ∀ x x' y y' → x A.≈ x' → y B.≈ y' → R x y → R x' y'
• Strict: ∀ x y → R x y → x A.≈ x × y B.≈ y
• Single-Valued: ∀ x y y' → R x y → R x y' → y B.≈ y'
• Total: ∀ x → x A.≈ x → Σ[ y ∈ B ] (R x y)

This last choice is arguably the "right" definition, as it gives you effective (sub)quotients. Unfortunately, this is not well-suited to predicative foundations, as now your maps are going to be parameterized by some annoying κ...

[jamesmckinna]

Re: 2
As elsewhere, modulo potential difficulties caused by --irrelevant-projections, can the problem of different proofs of Defined x = x A.≈ x be alleviated by marking such a field irrelevant? (alternatively, use of Data.Refinement with the refinement predicate P being Defined)

In practice, they may also be a better fit when such equality is in fact, Decidable (or variations on that theme in Relation.Nullary.Recomputable), thanks to Relation.Nullary.Decidable.Core.recompute...?

[jamesmckinna]

Re: 4
The compromise I had been thinking about would involve kernels/subsetoids as in #2816 for the PER structure induced by x y → P x × x ≈ y × P y, which is what I really discern as going on in #2829 , via lifting arbitrary P to Relation.Unary.Closure.Base.◇ _≈_ P (indeed, finessing the closedness/respects properties in general via such a construction, and if necessary, going via #2070 / #2071 to be able to work directly only with the ordering relation)... etc. for a more stdlib-compliant approach?

[TOTBWF]

As per my comment on #2829, I think the nicest way to define upwards/downwards closed subsets is via homomorphisms into the order on Set, which seems to be hinted at in #2070. This has some other benefits, like being able to inherit a bunch of properties from the pointwise orderings on monotone maps P -> Q.

[TOTBWF]

As for PERs, I think that we really want to avoid using them unless we absolutely have to. If Setoids are a way of taking your type theory and augmenting it with quotients, Partial Setoids are a way of taking your type theory and basically turning it into a more complicated version of structural theory.