relator.lift_fun

Stream: general

[Yaël Dillies]

What's the logic behind calling this relator.lift_fun?

def lift_fun (R : α → β → Prop) (S : γ → δ → Prop) (f : α → γ) (g : β → δ) : Prop :=
∀ ⦃a b⦄, R a b → S (f a) (g b)

Is it because it lifts two relations α → β → Prop, γ → δ → Prop to a relation (α → γ) → (β → δ) → Prop? Also, what does this relator stand for? This has nothing to do with the group-theoric relator, right?

[Yaël Dillies]

Bump! Does anybody know?

[Reid Barton]

I think "relator" is just another word for "relation", "lift" is as usual meaningless, and "fun" refers to f and g

[Reid Barton]

Wait no, "fun" is probably because it produces a relation between function types

[Reid Barton]

Aha, apparently "relator" means something like a functor that operates on relations rather than functions, see https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.26.4213&rep=rep1&type=pdf

[Yaël Dillies]

Ahah! I couldn't find anything about it.

[Kyle Miller]

Interesting, lift_fun R S f g indicates that (f, g) is a morphism between R and S in the "subscone of Set x Set." It seems that this subscone can be used to define a double category on Set? Objects are sets, vertical morphisms are functions, horizontal morphisms are relations, and 2-morphisms correspond to quadruples satisfying lift_fun.

Maybe another description is that if you take the functor F : Set -> Rel that sends functions to their graph, then lift_fun describes the morphisms in the comma category (F/F). (It's interesting how lift_fun R S is a relation in its own right, so it is itself an object in this category.)