# 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=10.1.1.26.4213&rep=rep1&type=pdf

#### 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