Adds "pushforward" to Relation.Unary

[bsaul]

This PR adds the pushforward of predicate along a function.

[Taneb]

This seems a reasonable addition, but I'm not familiar with the term "pushforward" in this context. Where does it come from?

[bsaul]

This seems a reasonable addition, but I'm not familiar with the term "pushforward" in this context. Where does it come from?

I'm using the term as in "pushfoward measure" from measure theory. If there's something more standard in the context of predicates, it's fine with me to change.

[Taneb]

I'd personally call the preimage of P under f. But let's wait to see if anyone else has naming ideas before changing it

[jamesmckinna]

If you're going to add this...

... better IMNSVHO that you also prove it is the left adjoint to the change-of-base/pullback operation (as to our calling that operation h ⊢ P, it's conventionally called h * P, but that's not going to fly) ... and on that basis, Lawvere defined it back in the 1960s, and called it ∃ₕ for h: A -> B, and (because Pred is 'sufficiently complete/co-complete': see eg Mac Lane and Moerdijk Ch.1, Sec. 9 on 'Quantifiers' in preseheaf semantics) moreover h * has a right adjoint, ∀ₕ as well (apologies for h here, subscript f doesn't seem to be in the agda-input-mode glossary)...

... But clearly we can't have a notation which is subscripted wrt one argument, moreover which might clash with existing syntax declarations in Relation.Unary, however we end up choosing a cognate name, means there isn't an obvious way forward to me as regards naming... other than to observe that using the 'adjoint' symbol for this operation would be highly sub-optimal, again IMNSVHO... because overspecialising of an 'important' symbol...

Also, see #436 (generalisation to Setoid/arbitrary equality, so adjoint properties would be modulo appropriate Respects proofs) and PR #2419 which introduced

Function.Related.TypeIsomorphisms.∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y)

so at least there are/would be refactoring opportunities here...

So: yes to the addition, but I think we can do better, and to do this well would need a bit more design, I think. Not least because if we add this now, any subsequent generalisation might complicate the name space later wrt deprecation etc., ...

[jamesmckinna]

I'd personally call the preimage of P under f. But let's wait to see if anyone else has naming ideas before changing it

As for 'preimage', I'd rather call it/think it should be called 'image'... ;-) but again, overloaded terminology considered harmful?

As for 'pushforward', I'm aware of the usage in (modern) measure theory, but again, proliferation of new terms-of-art from various domains frustrates any attempt to unify notation/properties... DRY!

[Taneb]

As for 'preimage', I'd rather call it/think it should be called 'image'... ;-) but again, overloaded terminology considered harmful?

You're absolutely right! I got myself confused.

[jamesmckinna]

D'oh...
... for all that I do know or remember, I still forget that
Relation.Unary.Closure.Base.{box|diamond}, when specialised to the relation R given by the graph of f (understood propositionally, and/or setoidally) give us the constructions we want (please check!), together with variations on curry/uncurry to define the various adjunctions should/might give you what you want?

The fine print needs checking though!
in particular, we need to generalise from Rel to REL... hmmm

Possible status:duplicate therefore?

Plus, of course: discoverability as an issue (and perhaps should be added as a new label for issues/PRs... @JacquesCarette !?)

[bsaul]

I still forget that
Relation.Unary.Closure.Base.{box|diamond}, when specialised to the relation R given by the graph of f (understood propositionally, and/or setoidally)

Oh, that's interesting. I can see that, though it was not at all obvious to me until you pointed it out. However box|diamond yield Pred A -> Pred A, not Pred A -> Pred B.

[jamesmckinna]

Oh, that's interesting. I can see that, though it was not at all obvious to me until you pointed it out. However box|diamond yield Pred A -> Pred A, not Pred A -> Pred B.

Yes, they need to be generalised from R : Rel A _ to R : REL A B _, and then specialised to R defined by R x y = f x ≈ y, etc.
Sorry if my remarks about generalisation/refactoring were too telegraphic...

[bsaul]

I'd personally call the preimage of P under f. But let's wait to see if anyone else has naming ideas before changing it

As for 'preimage', I'd rather call it/think it should be called 'image'... ;-) but again, overloaded terminology considered harmful?

For that matter, I would've called _⊢_ preimage instead of "Update". Anyway, I don't know how to avoid overloaded terminology in general, though it's a worthy goal.

[bsaul]

So: yes to the addition, but I think we can do better, and to do this well would need a bit more design, I think. Not least because if we add this now, any subsequent generalisation might complicate the name space later wrt deprecation etc., ...

Ok, though I'm not clear exactly what, if anything, I can/should do now.

[gallais]

Let me offer an orthogonal remark. Instead of

_⊣_ : (A → B) → Pred A ℓ → Pred B _

I would prefer

_⊣_ : Pred A ℓ → (A → B) → Pred B _

The idea behind f ⊢ P is that it represents the Martin-Löf tradition of only mentioning
the updates to the ambient context when describing a P family indexed by contexts, e.g.
(_, σ) ⊢ Tm τ is "a term of type τ in the ambient context extended with a fresh σ".

Conversely, I'd expect a peeling off action to keep the family P on the pointy side of the
turnstyle as we are once again acting on the context rather than on the predicate.

[bsaul]

The idea behind f ⊢ P is that it represents the Martin-Löf tradition on only mentioning
the updates to the ambient context when describing a P family indexed by context, e.g.
(_, σ) ⊢Tm τ is "a term of type τ in the ambient context extended with a fresh σ.

Thanks. This makes sense.

[bsaul]

I would prefer

_⊣_ : Pred A ℓ → (A → B) → Pred B _

Works for me.

[jamesmckinna]

As for how to proceed now, we could merge the definition as is (modulo exact shape of types)essentially as a provisional addition for v2.4, but I think that leaves a complicated refactoring downstream for v3.0 to generalise things ... appropriately.

But I'm guessing that that might be more work than you're able to take on for the present PR @bsaul ?

My teaching this semester might make it tricky for me to take on before the new year, for example.

So I'd welcome further input from the other core maintainers on this one!

[jamesmckinna]

Let me offer an orthogonal remark. Instead of

_⊣_ : (A → B) → Pred A ℓ → Pred B _

Conversely, I'd expect a peeling off action to keep the family P on the pointy side of the turnstyle as we are once again acting on the context rather than on the predicate.

... that may be fine for the left adjoint, but what about the right adjoint? Hence my suggested generalisation of diamond (left) and box (right), rather than more turnstiles...

[jamesmckinna]

My (new suggested) names are only suggestions, but I think in the interests of treating the left- and right- adjoints on an even footing, we shouldn't simply use a symbol which flips the turnstile for the sake of privileging one over the other.

As for the proofs of the adjoint transformers in Relation.Unary.Properties, those too can be added downstream, unless you feel like adding them here yourself?

[jamesmckinna]

In a spirit of 'compromise', and taking @gallais 's nudge about relative position wrt the turnstile, suggest instead:

Suggested change

	_⊣_ : (A → B) → Pred A ℓ → Pred B _
	f ⊣ P = λ b → ∃ λ a → f a ≡ b × P a
	∃[_]⊢_ : (A → B) → Pred A ℓ → Pred B ℓ
	∃[ f ]⊢ P = λ b → ∃ λ a → f a ≡ b × P a

so that one can also then add (plus fixing up the fixity declarations! sigh...)

∀[_]⊢_ : (A → B) → Pred A ℓ → Pred B ℓ
∀[ f ]⊢ P = λ b → ∀ a → f a ≡ b → P a

per Lawvere, and consider refinements of this in a setoidal context downstream?