Zulip Chat Archive

Stream: general

Topic: relator.lift_fun

Yaël Dillies (Aug 17 2021 at 09:09):

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 (Aug 20 2021 at 09:56):

Bump! Does anybody know?

Reid Barton (Aug 20 2021 at 11:39):

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

Reid Barton (Aug 20 2021 at 11:46):

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

Reid Barton (Aug 20 2021 at 12:14):

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

Yaël Dillies (Aug 20 2021 at 18:34):

Ahah! I couldn't find anything about it.

Kyle Miller (Aug 20 2021 at 19:25):

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.)

Last updated: Dec 20 2023 at 11:08 UTC