# Zulip Chat Archive

## Stream: maths

### Topic: Church Numeral Puzzles

#### Kevin Buzzard (May 02 2018 at 19:55):

I am trying to understand church numerals by writing a collection of basic theorems about them.

#### Kevin Buzzard (May 02 2018 at 19:55):

I just solved this one:

#### Kevin Buzzard (May 02 2018 at 19:56):

def chℕ := Π X : Type, (X → X) → X → X namespace chnat open nat definition to_nat : chℕ → ℕ := λ m, m ℕ nat.succ 0 def of_nat : ℕ → chℕ | (zero) := λ X f x, x | (succ n) := λ X f x, f (of_nat n X f x) -- f (f^n x) definition of_nat' : ℕ → chℕ | 0 := λ X f x, x | (n + 1) := λ X f x, of_nat' n X f (f x) -- f^n (f x) theorem of_nat_is_of_nat' (n : ℕ) : of_nat n = of_nat' n := sorry end chnat

#### Kevin Buzzard (May 02 2018 at 19:57):

it was harder than I expected though, so I probably missed a trick, which is why I mention it here.

#### Gabriel Ebner (May 02 2018 at 20:06):

Hmm, this was a pretty straightforward induction:

theorem of_nat_is_of_nat' (n : ℕ) : of_nat n = of_nat' n := begin induction n with n; funext X f x; simp! *, clear n_ih, induction n generalizing x; simp! *, end

#### Kevin Buzzard (May 02 2018 at 20:33):

This is the key lemma I've been after:

#### Kevin Buzzard (May 02 2018 at 20:33):

lemma of_nat_functorial (n : ℕ) (X Y : Type) (a : X → Y) (f : X → X) : ∀ x, a (of_nat n X f x) = @of_nat n (X → Y) (λ g x', g (f x')) a x :=

#### Kevin Buzzard (May 02 2018 at 20:35):

I have never used `generalizing`

or `simp!`

before.

#### Kevin Buzzard (May 02 2018 at 20:35):

So thanks very much for these!

#### Kevin Buzzard (May 02 2018 at 20:35):

@Gabriel Ebner

#### Kevin Buzzard (May 02 2018 at 20:36):

I also have this:

#### Kevin Buzzard (May 02 2018 at 20:36):

`example (m n : ℕ) : of_nat (m + n) = of_nat m + of_nat n := sorry`

#### Chris Hughes (May 02 2018 at 20:47):

lemma of_nat_functorial : ∀ (n : ℕ) (X Y : Type) (a : X → Y) (f : X → X) (x : X), a (of_nat n X f x) = @of_nat n (X → Y) (λ g x', g (f x')) a x | 0 := by intros; refl | (n+1) := begin assume X Y a f x, rw [of_nat], dsimp, rw ← of_nat_functorial, dsimp, apply congr_arg, clear of_nat_functorial, induction n with n ih generalizing x, refl, rw of_nat, dsimp, rw ih, end

#### Chris Hughes (May 02 2018 at 20:47):

Not the cleanest, but done.

#### Gabriel Ebner (May 02 2018 at 20:58):

These lemmas are all induction+simp, if you set them up correctly:

instance: has_add chℕ := ⟨λ a b X f, a _ f ∘ b _ f⟩ @[simp] lemma chℕ_add (a b : chℕ) : a + b = (λ X f, a _ f ∘ b _ f) := rfl @[simp] lemma of_nat_f (n X f x) : of_nat n X f (f x) = f (of_nat n X f x) := by induction n generalizing x; simp! * local attribute [-simp] add_comm lemma of_nat_add (m n : ℕ) : of_nat (m + n) = of_nat m + of_nat n := by induction n with n generalizing m; funext X f x; simp [of_nat, *]

#### Gabriel Ebner (May 02 2018 at 21:00):

Unfortunately you can't orient `of_nat_f`

the other way around because it won't work as a simp lemma then.

#### Kevin Buzzard (May 02 2018 at 21:34):

Thanks so much Gabriel!

#### Kevin Buzzard (May 02 2018 at 22:12):

These proofs are really cool :-)

#### Kevin Buzzard (May 02 2018 at 22:13):

I understand better the way you think about the question now. I want to prove all the intermediate lemmas first, because historically I have been trained to go forwards. You just keep reducing the problem to simpler statements by induction because dependent type theory is somehow better at pushing backwards.

#### Kevin Buzzard (May 02 2018 at 22:16):

The one with `clear n_ih`

is interesting!

#### Kevin Buzzard (May 02 2018 at 22:26):

def pow : chℕ → chℕ → chℕ := λ m n, λ X f x, n (X → X) (λ g, (m X g)) f x theorem of_nat_pow (m n : ℕ) : of_nat (m + n) = of_nat m + of_nat n := sorry

#### Mario Carneiro (May 02 2018 at 22:28):

I think the proof is `of_nat_add _ _`

:)

#### Kevin Buzzard (May 02 2018 at 22:28):

wait a second

#### Kevin Buzzard (May 02 2018 at 22:29):

def chℕ := Π X : Type, (X → X) → X → X namespace chnat open nat definition to_nat : chℕ → ℕ := λ m, m ℕ nat.succ 0 def of_nat : ℕ → chℕ | (zero) := λ X f x, x | (succ n) := λ X f x, f (of_nat n X f x) -- f (f^n x) def pow : chℕ → chℕ → chℕ := λ m n, λ X f x, n (X → X) (λ g, (m X g)) f x theorem of_nat_pow (m n : ℕ) : of_nat (m ^ n) = pow (of_nat m) (of_nat n) := sorry end chnat

#### Kevin Buzzard (May 02 2018 at 22:29):

I think that runs and asks the question I want to ask :-)

#### Kenny Lau (May 02 2018 at 22:29):

I thought I already proved it

#### Kevin Buzzard (May 02 2018 at 22:29):

Can you golf it though?

#### Kenny Lau (May 02 2018 at 22:29):

...

#### Kevin Buzzard (May 02 2018 at 22:29):

Did you see Gabriel's proofs?

#### Mario Carneiro (May 02 2018 at 22:31):

def chℕ := Π X : Type, (X → X) → X → X namespace chnat open nat def to_nat (m : chℕ) : ℕ := m ℕ nat.succ 0 def of_nat : ℕ → chℕ | (zero) X f x := x | (succ n) X f x := f (of_nat n X f x) -- f (f^n x) def pow (m n : chℕ) : chℕ | X f x := n (X → X) (m X) f x theorem of_nat_pow (m n : ℕ) : of_nat (m ^ n) = pow (of_nat m) (of_nat n) := sorry end chnat

golfed

#### Kenny Lau (May 02 2018 at 22:32):

...

#### Kevin Buzzard (May 02 2018 at 22:35):

Mario I guess that in reality I am more interested in the style. Is yours both preferable and golfier? Ultimately I want to write good style Lean.

#### Kenny Lau (May 02 2018 at 22:37):

I wouldn't prefer it

#### Kevin Buzzard (May 02 2018 at 22:37):

ooh the `lam g`

on my part was a rookie error

#### Kenny Lau (May 02 2018 at 22:37):

you see, it uses the equation compiler

#### Kenny Lau (May 02 2018 at 22:37):

and uses "external" definitional equality

#### Kenny Lau (May 02 2018 at 22:38):

like it isn't "expressionally equal" but somehow they made it definitionally equal (by all those ._equation_1) thing

#### Kenny Lau (May 02 2018 at 22:38):

do `#print prefix chnat.pow`

to see what I mean

#### Mario Carneiro (May 02 2018 at 22:39):

huh? There is no fancy business in any of the definitions except `of_nat`

, but that was already defined by eqn compiler

#### Kenny Lau (May 02 2018 at 22:40):

hmm...

#### Kenny Lau (May 02 2018 at 22:40):

they don't do `._main`

if you don't have two cases?

#### Mario Carneiro (May 02 2018 at 22:40):

the eqn compiler always produces `._main`

I guess

#### Mario Carneiro (May 02 2018 at 22:40):

for uniformity I assume

#### Kenny Lau (May 02 2018 at 22:43):

I don't like main

#### Kenny Lau (May 02 2018 at 22:44):

as a sidenote now I prefer `trans_rel_left`

over `calc`

lol

#### Kenny Lau (May 02 2018 at 22:44):

because _ with the tactics

#### Kevin Buzzard (May 02 2018 at 22:45):

Oh you're right Kenny. So Mario does this mean that the lambda style is preferred in practice?

#### Kenny Lau (May 02 2018 at 22:46):

I think Mario prefers the equation compiler because it looks nicer

#### Mario Carneiro (May 02 2018 at 22:46):

I always locally optimize `def T : A -> B := \lam x, t`

=> `def T (x : A) : B := t`

#### Mario Carneiro (May 02 2018 at 22:47):

and `def T : B := \lam x, t`

=> `def T : B | x := t`

#### Kenny Lau (May 02 2018 at 22:47):

what next, `\la x, A $ B x`

=> `A \o B`

?

#### Kenny Lau (May 02 2018 at 22:48):

does your optimization have church rosser?

#### Mario Carneiro (May 02 2018 at 22:48):

that one depends on whether the \o gets in the way later

#### Mario Carneiro (May 02 2018 at 22:48):

but usually yes

#### Kenny Lau (May 02 2018 at 22:48):

even if `x`

is a proposition?

#### Mario Carneiro (May 02 2018 at 22:49):

sure, why not?

#### Kenny Lau (May 02 2018 at 22:49):

wow

#### Kevin Buzzard (May 02 2018 at 22:49):

It's the `|`

that causes the trouble

#### Mario Carneiro (May 02 2018 at 22:49):

it often doesn't work as a straight replacement since it could be dependent

#### Kevin Buzzard (May 02 2018 at 22:49):

suddenly I have `pow._main`

#### Kenny Lau (May 02 2018 at 22:49):

yay we're on the same side for this time

#### Mario Carneiro (May 02 2018 at 22:49):

Yes, the `|`

triggers the equation compiler

#### Mario Carneiro (May 02 2018 at 22:50):

It also gives you the correct (applied) equation lemma

#### Mario Carneiro (May 02 2018 at 22:50):

rather than the lambda equation lemma

#### Kenny Lau (May 02 2018 at 22:50):

I don't like that

#### Kevin Buzzard (May 02 2018 at 22:51):

But Kenny is that just because you haven't learned how to use the more complex type properly?

#### Kevin Buzzard (May 02 2018 at 22:51):

What is an example of where this causes you problems?

#### Kenny Lau (May 02 2018 at 22:51):

heh... I use the equation compiler all the time

#### Kenny Lau (May 02 2018 at 22:51):

I just don't like it

#### Kevin Buzzard (May 02 2018 at 22:51):

and I am asking why exactly

#### Kenny Lau (May 02 2018 at 22:52):

i don't know

#### Mario Carneiro (May 02 2018 at 22:52):

I understand wanting a simple underlying term, but that's an issue best aimed at the equation compiler

#### Kevin Buzzard (May 02 2018 at 22:53):

I am just learning all these tricks now. I have learned that when you write a substantial amount of code you end up picking stuff up as you need it; Kenny you wrote a lot of code a lot quicker than me.

#### Kevin Buzzard (May 02 2018 at 22:53):

Mario, did you do my Ackermann church question? ;-)

#### Kenny Lau (May 02 2018 at 22:53):

I'm convinced you can't do it

#### Kenny Lau (May 02 2018 at 22:53):

you need a higher order functional

#### Kenny Lau (May 02 2018 at 22:54):

since chNat lives in Type 1

#### Kenny Lau (May 02 2018 at 22:54):

you need an empowered chNat that lives in Type 2

#### Kenny Lau (May 02 2018 at 22:54):

Ackermann isn't primitive recursive

#### Kenny Lau (May 02 2018 at 22:54):

its image is in Delta_1 not Delta_0

#### Kenny Lau (May 02 2018 at 22:54):

in the arithmetic hierarchy

#### Kevin Buzzard (May 02 2018 at 22:54):

`def ack : chℕ → chℕ → chℕ := sorry -- KB didn't try this one`

#### Kenny Lau (May 02 2018 at 22:54):

whatever that means

#### Kevin Buzzard (May 02 2018 at 22:54):

(for good reason!)

#### Mario Carneiro (May 02 2018 at 22:54):

what ackermann church question

#### Kevin Buzzard (May 02 2018 at 22:54):

fill in the def above

#### Kenny Lau (May 02 2018 at 22:54):

@Mario Carneiro make ackermann using church

#### Kevin Buzzard (May 02 2018 at 22:55):

so that it commutes with usual ack on nat

#### Kenny Lau (May 02 2018 at 22:55):

@Kevin Buzzard or do you already know that one can't do it

#### Kevin Buzzard (May 02 2018 at 22:55):

I don't have a clue

#### Mario Carneiro (May 02 2018 at 22:55):

You can do it

#### Kevin Buzzard (May 02 2018 at 22:55):

I just think this is really cool :-)

#### Kevin Buzzard (May 02 2018 at 22:55):

How do you know you can do it?

#### Kenny Lau (May 02 2018 at 22:56):

@Mario Carneiro I tried to do it and found myself requiring a more complex term in each iteration

#### Kenny Lau (May 02 2018 at 22:56):

you can't iterate on (chN -> chN) either

#### Kevin Buzzard (May 02 2018 at 22:57):

When a computer scientist says "you can do it" do they mean "there exists some computer code which does that job" or "it's possible to construct, in polynomial time, some computer code which does that job"

#### Kenny Lau (May 02 2018 at 22:57):

the former

#### Mario Carneiro (May 02 2018 at 22:57):

I mean there is a solution in less than 50 chars

#### Kevin Buzzard (May 02 2018 at 22:57):

:-)

#### Kenny Lau (May 02 2018 at 22:57):

??????

#### Kenny Lau (May 02 2018 at 22:57):

50 chars....

#### Mario Carneiro (May 02 2018 at 22:57):

so just go through all the lambda terms, you'll get it

#### Kevin Buzzard (May 02 2018 at 22:57):

that's not polynomial time though

#### Mario Carneiro (May 02 2018 at 22:58):

heck no

#### Kevin Buzzard (May 02 2018 at 22:58):

Just to be clear, we're talking about the church numeral type without the axiom.

#### Kevin Buzzard (May 02 2018 at 22:59):

`def chℕ := Π X : Type, (X → X) → X → X`

#### Kenny Lau (May 02 2018 at 22:59):

@Mario Carneiro so what is wrong with my analysis?

#### Mario Carneiro (May 02 2018 at 22:59):

Ah, I see what you mean now

#### Mario Carneiro (May 02 2018 at 23:00):

In lambda calculus it's untyped so there is no problems

#### Kenny Lau (May 02 2018 at 23:00):

exactly

#### Mario Carneiro (May 02 2018 at 23:00):

but lean has universe issues

#### Kenny Lau (May 02 2018 at 23:00):

we're in typed lamdba calculus

#### Kevin Buzzard (May 02 2018 at 23:00):

as opposed to his rather more well-behaved friend ```
chℕfree := {m : Π X : Type, (X → X) → X → X // ∀ (X Y : Type) (a : X → Y) (f : X → X) (x : X),
m (X → Y) (λ g, g ∘ f) a x = a (m X f x)}
```

#### Kevin Buzzard (May 02 2018 at 23:00):

which comes with a free theorem

#### Mario Carneiro (May 02 2018 at 23:00):

you can still do it but you need inductive types, I think

#### Kevin Buzzard (May 02 2018 at 23:01):

oh wait I can do it by cheating!

#### Kevin Buzzard (May 02 2018 at 23:01):

There's a projection from church nat to nat

#### Mario Carneiro (May 02 2018 at 23:01):

exactly

#### Mario Carneiro (May 02 2018 at 23:01):

so you do an induction on `nat -> nat`

#### Kenny Lau (May 02 2018 at 23:02):

that's cheating

#### Kevin Buzzard (May 02 2018 at 23:02):

so I can define an "incorrect" pow

#### Kevin Buzzard (May 02 2018 at 23:02):

But this is cheating

#### Kevin Buzzard (May 02 2018 at 23:02):

Is this what they do with pred?

#### Mario Carneiro (May 02 2018 at 23:02):

like I said, you need inductive types

#### Kenny Lau (May 02 2018 at 23:02):

that's like asking can I define pow by of_nat and to_nat

#### Kevin Buzzard (May 02 2018 at 23:02):

If you were to project to nat and then project back with any of add, mul or pow

#### Mario Carneiro (May 02 2018 at 23:02):

I think you are right that chN only allows primrec definitions directly

#### Kevin Buzzard (May 02 2018 at 23:02):

you would get a different answer to the "pure" answers which exist

#### Kenny Lau (May 02 2018 at 23:03):

I mean there is a solution in less than 50 chars

this wouldn't work. how are you going to check if a given lambda term produces ack?

#### Mario Carneiro (May 02 2018 at 23:04):

solve the halting problem of course

#### Kevin Buzzard (May 02 2018 at 23:04):

in the proof I'm envisaging

#### Kenny Lau (May 02 2018 at 23:04):

you...

#### Kevin Buzzard (May 02 2018 at 23:04):

:-)

#### Kevin Buzzard (May 02 2018 at 23:04):

it's going to follow from some cunning unravelling isn't it?

#### Mario Carneiro (May 02 2018 at 23:09):

wait, no I lied again, it is possible

#### Kenny Lau (May 02 2018 at 23:09):

hmm

#### Mario Carneiro (May 02 2018 at 23:09):

the motive is `X → X`

#### Kenny Lau (May 02 2018 at 23:10):

you need to store a function each time

#### Kevin Buzzard (May 02 2018 at 23:18):

theorem nat_of_chnat_of_nat (n : ℕ) : to_nat (of_nat n) = n := sorry -- exercise -- breakthough! I implemented my exciting new foo function on church numerals def foo : ℕ → ℕ → ℕ := sorry def choo (m n : chℕ) : chℕ := of_nat (foo (to_nat m) (to_nat n)) theorem amazing_compatibility (a b : ℕ) : of_nat (foo a b) = choo (of_nat a) (of_nat b) := begin unfold choo, simp [nat_of_chnat_of_nat] end

#### Kevin Buzzard (May 02 2018 at 23:20):

That makes me slightly sad

#### Kevin Buzzard (May 02 2018 at 23:21):

I spent some time today thinking about the Church Numeral which given X and f and x, returns x unless X = nat and f = succ and x = 0, in which case it returns 1

#### Kevin Buzzard (May 02 2018 at 23:22):

it's quite a good way of reminding yourself exactly how far you can expect to push things

#### Kevin Buzzard (May 02 2018 at 23:24):

e.g. I believe that funny numeral doesn't commute with + 1 and this can be easily checked via very concrete calculation on nat

#### Kevin Buzzard (May 02 2018 at 23:24):

so you know you shouldn't be trying to prove that add commutes

#### Kevin Buzzard (May 02 2018 at 23:25):

I'm not sure what Mr Ackermann would have thought about evaluating his function there

#### Mario Carneiro (May 02 2018 at 23:26):

By the way, you got the free statement a bit off:

def chℕfree := {m : Π X : Type, (X → X) → X → X // ∀ (X Y : Type) (a : X → Y) (f : X → X) (g : Y → Y), a ∘ f = g ∘ a → m Y g ∘ a = a ∘ m X f}

#### Kevin Buzzard (May 02 2018 at 23:30):

Do you think that's the same?

#### Kevin Buzzard (May 02 2018 at 23:30):

You are quantifying over g too

#### Kevin Buzzard (May 02 2018 at 23:31):

It might be the same

#### Mario Carneiro (May 02 2018 at 23:34):

It might be the same, but my version fits a more regular pattern

#### Mario Carneiro (May 02 2018 at 23:34):

and it doesn't require evaluating `m`

at a function type

#### Mario Carneiro (May 02 2018 at 23:35):

It's basically saying that if `a : f -> g`

is a natural transformation, then so is `m`

#### Mario Carneiro (May 02 2018 at 23:36):

That's probably a poor reading, but something like that

#### Mario Carneiro (May 02 2018 at 23:38):

What makes `chN`

not quite as powerful as system T is that `chN`

isn't a type in the internal sense

#### Mario Carneiro (May 02 2018 at 23:38):

with impredicative quantification (like in system F) this would work

#### Mario Carneiro (May 02 2018 at 23:41):

Godel's system T is simply typed lambda calculus with arrows and products, and a type `N`

with `0 : N`

and `S : N -> N`

and `iter_A : (A -> A) -> A -> N -> A`

#### Mario Carneiro (May 02 2018 at 23:42):

Then `N`

there is just like lean's `ℕ`

, but `chℕ`

is not a substitute because it lives in `Type 1`

so it is not a type in STLC

#### Kevin Buzzard (May 02 2018 at 23:49):

This is really interesting

#### Kevin Buzzard (May 02 2018 at 23:49):

I identified nat as the universal object

#### Kevin Buzzard (May 02 2018 at 23:49):

and just wrote down some kind of standard maths functory thing about evaluating the universal object at a map

#### Kevin Buzzard (May 02 2018 at 23:50):

but, like induction, you might think about universal objects in a different way to us

#### Kevin Buzzard (May 02 2018 at 23:50):

I think I see what I'm missing

#### Kevin Buzzard (May 02 2018 at 23:51):

In my world, a would be a map in the category

#### Kevin Buzzard (May 02 2018 at 23:51):

and I would be assuming m was a functor

#### Kevin Buzzard (May 02 2018 at 23:51):

and trying to represent it

#### Kevin Buzzard (May 02 2018 at 23:51):

but m being a functor is an extra condition which I have forgotten about because in the examples I know it is always there

#### Kevin Buzzard (May 03 2018 at 01:12):

`example : equiv ℕ chℕfree := ⟨to_chfr,of_chfr,inv₁,inv₂⟩ `

#### Kevin Buzzard (May 03 2018 at 01:17):

Mario's definition definitely works. I wonder if mine (which is implied by Mario's) is too weak.

#### Kevin Buzzard (May 03 2018 at 01:23):

So I understand the category theory language much better than this DTT stuff.

#### Kevin Buzzard (May 03 2018 at 01:23):

I want to say that Type is a category.

#### Mario Carneiro (May 03 2018 at 01:23):

It is

#### Kevin Buzzard (May 03 2018 at 01:23):

Then m wants to be a functor from Type to Type

#### Kevin Buzzard (May 03 2018 at 01:23):

but Church's naive definition just demands a map on objects

#### Mario Carneiro (May 03 2018 at 01:24):

In languages where the naive definition works, that's because of parametric polymorphism

#### Mario Carneiro (May 03 2018 at 01:24):

i.e. everything is functorial

#### Kevin Buzzard (May 03 2018 at 01:24):

I don't know what that means

#### Mario Carneiro (May 03 2018 at 01:24):

HoTT is a lot like this

#### Kevin Buzzard (May 03 2018 at 01:24):

Oh I see

#### Mario Carneiro (May 03 2018 at 01:24):

the language is crafted such that you can't write badly behaved terms at all

#### Mario Carneiro (May 03 2018 at 01:25):

everything is "fibrant"

#### Mario Carneiro (May 03 2018 at 01:25):

whatever that means

#### Kevin Buzzard (May 03 2018 at 01:25):

Let me modify Type

#### Kevin Buzzard (May 03 2018 at 01:25):

so that its objects are still terms whose type is Type

#### Mario Carneiro (May 03 2018 at 01:25):

but that's basically why univalence works

#### Kevin Buzzard (May 03 2018 at 01:25):

but the morphisms are equivs

#### Kevin Buzzard (May 03 2018 at 01:25):

Now m is a map on objects

#### Kevin Buzzard (May 03 2018 at 01:26):

and the data of the equiv is exactly what m needs to be extendible to a map on morphisms I suspect

#### Mario Carneiro (May 03 2018 at 01:26):

Check this out: http://www.cs.bham.ac.uk/~udr/papers/logical-relations-and-parametricity.pdf

#### Kevin Buzzard (May 03 2018 at 01:27):

In fact I guess it's exactly when X and Y biject that I would even dream of identifying `(X->X) -> X -> X`

and the analogous term for `Y`

#### Mario Carneiro (May 03 2018 at 01:27):

It argues that naturality is the wrong idea and should be replaced by parametricity

#### Mario Carneiro (May 03 2018 at 01:27):

I need to finish digesting it though, so don't quote me on that

#### Mario Carneiro (May 03 2018 at 01:28):

Notice though that the condition I gave does not require that a is an equiv

#### Mario Carneiro (May 03 2018 at 01:28):

I think that's going to be true in general

#### Mario Carneiro (May 03 2018 at 01:28):

It really is a functoriality condition

#### Kevin Buzzard (May 03 2018 at 01:29):

You have to be careful

#### Kevin Buzzard (May 03 2018 at 01:29):

Given a map A to B

#### Mario Carneiro (May 03 2018 at 01:29):

it's just this weird higher order functoriality thing

#### Mario Carneiro (May 03 2018 at 01:29):

It seems like logical relations generate the condition well

#### Kevin Buzzard (May 03 2018 at 01:29):

You don't get a map (A to A) to (B to B)

#### Kevin Buzzard (May 03 2018 at 01:30):

So I don't know what you mean when you say functoriality is true "in general"

#### Kevin Buzzard (May 03 2018 at 01:30):

I can only see a functor in the equiv category

#### Kevin Buzzard (May 03 2018 at 01:31):

Maybe we mean different things by functorially

#### Mario Carneiro (May 03 2018 at 01:31):

I mean that if you write down some more complicated thing than chN I can write down a more complicated parametricity constraint for it

#### Mario Carneiro (May 03 2018 at 01:31):

and I can always do this

#### Mario Carneiro (May 03 2018 at 01:31):

and it will involve a function a : X -> Y

#### Mario Carneiro (May 03 2018 at 01:32):

and that function will usually not be required to be an equiv

#### Kevin Buzzard (May 03 2018 at 01:33):

I can't make that concept into a functor

#### Kevin Buzzard (May 03 2018 at 01:34):

For me, F (X -> Y) is a map F X -> F Y

#### Mario Carneiro (May 03 2018 at 01:35):

Here's the setup: we define a collection of logical relations [R] : X -> Y -> Prop. The important one is for arrows: `[R -> S] : (X -> X') -> (Y -> Y') -> Prop`

is defined by

f [R -> S] g <-> \forall x y, x [R] y -> f x [S] g y

#### Mario Carneiro (May 03 2018 at 01:36):

At the base types we define `[R] : X -> Y -> Prop`

by `x [R] y <-> a x = y`

#### Mario Carneiro (May 03 2018 at 01:36):

where `a : X -> Y`

is our fixed morphism to commute over

#### Mario Carneiro (May 03 2018 at 01:37):

Applying this definition to `[(R -> R) -> R -> R]`

gives exactly the condition I wrote down

#### Kevin Buzzard (May 03 2018 at 01:37):

Oh so you're going to tell me that the function I'm looking for is actually a relation

#### Mario Carneiro (May 03 2018 at 01:42):

And we can go further to even get the `a`

part: we can define `[∀ X, R] : (∀ X:Type, P X) -> (∀ X:Type, Q X) -> Prop`

by

F [∀ X, R] G <-> ∀ X Y : Type, ∀ (a : X -> Y), F X [R] G Y

(here if `X`

appears in `R`

it's referring to the relation for the function `a`

)

#### Mario Carneiro (May 03 2018 at 01:43):

Finally, a term is parametrically polymorphic if it is related to itself at its type, i.e. `m [∀ X, (X -> X) -> X -> X] m`

for the case of `chN`

#### Mario Carneiro (May 03 2018 at 01:44):

This is how logical relations work, and how the theorems for free statements are derived

#### Kevin Buzzard (May 03 2018 at 15:34):

Check this out: http://www.cs.bham.ac.uk/~udr/papers/logical-relations-and-parametricity.pdf

That paper

Last updated: May 18 2021 at 08:14 UTC