Zulip Chat Archive

Stream: maths

Topic: Church Numeral Puzzles


view this post on Zulip Kevin Buzzard (May 02 2018 at 19:55):

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

view this post on Zulip Kevin Buzzard (May 02 2018 at 19:55):

I just solved this one:

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 02 2018 at 20:33):

This is the key lemma I've been after:

view this post on Zulip 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 :=

view this post on Zulip Kevin Buzzard (May 02 2018 at 20:35):

I have never used generalizing or simp! before.

view this post on Zulip Kevin Buzzard (May 02 2018 at 20:35):

So thanks very much for these!

view this post on Zulip Kevin Buzzard (May 02 2018 at 20:35):

@Gabriel Ebner

view this post on Zulip Kevin Buzzard (May 02 2018 at 20:36):

I also have this:

view this post on Zulip Kevin Buzzard (May 02 2018 at 20:36):

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

view this post on Zulip 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

view this post on Zulip Chris Hughes (May 02 2018 at 20:47):

Not the cleanest, but done.

view this post on Zulip 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, *]

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 02 2018 at 21:34):

Thanks so much Gabriel!

view this post on Zulip Kevin Buzzard (May 02 2018 at 22:12):

These proofs are really cool :-)

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 02 2018 at 22:16):

The one with clear n_ih is interesting!

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 02 2018 at 22:28):

I think the proof is of_nat_add _ _ :)

view this post on Zulip Kevin Buzzard (May 02 2018 at 22:28):

wait a second

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 02 2018 at 22:29):

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

view this post on Zulip Kenny Lau (May 02 2018 at 22:29):

I thought I already proved it

view this post on Zulip Kevin Buzzard (May 02 2018 at 22:29):

Can you golf it though?

view this post on Zulip Kenny Lau (May 02 2018 at 22:29):

...

view this post on Zulip Kevin Buzzard (May 02 2018 at 22:29):

Did you see Gabriel's proofs?

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 02 2018 at 22:32):

...

view this post on Zulip 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.

view this post on Zulip Kenny Lau (May 02 2018 at 22:37):

I wouldn't prefer it

view this post on Zulip Kevin Buzzard (May 02 2018 at 22:37):

ooh the lam g on my part was a rookie error

view this post on Zulip Kenny Lau (May 02 2018 at 22:37):

you see, it uses the equation compiler

view this post on Zulip Kenny Lau (May 02 2018 at 22:37):

and uses "external" definitional equality

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 02 2018 at 22:38):

do #print prefix chnat.pow to see what I mean

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 02 2018 at 22:40):

hmm...

view this post on Zulip Kenny Lau (May 02 2018 at 22:40):

they don't do ._main if you don't have two cases?

view this post on Zulip Mario Carneiro (May 02 2018 at 22:40):

the eqn compiler always produces ._main I guess

view this post on Zulip Mario Carneiro (May 02 2018 at 22:40):

for uniformity I assume

view this post on Zulip Kenny Lau (May 02 2018 at 22:43):

I don't like main

view this post on Zulip Kenny Lau (May 02 2018 at 22:44):

as a sidenote now I prefer trans_rel_left over calc lol

view this post on Zulip Kenny Lau (May 02 2018 at 22:44):

because _ with the tactics

view this post on Zulip 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?

view this post on Zulip Kenny Lau (May 02 2018 at 22:46):

I think Mario prefers the equation compiler because it looks nicer

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 02 2018 at 22:47):

and def T : B := \lam x, t => def T : B | x := t

view this post on Zulip Kenny Lau (May 02 2018 at 22:47):

what next, \la x, A $ B x => A \o B?

view this post on Zulip Kenny Lau (May 02 2018 at 22:48):

does your optimization have church rosser?

view this post on Zulip Mario Carneiro (May 02 2018 at 22:48):

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

view this post on Zulip Mario Carneiro (May 02 2018 at 22:48):

but usually yes

view this post on Zulip Kenny Lau (May 02 2018 at 22:48):

even if x is a proposition?

view this post on Zulip Mario Carneiro (May 02 2018 at 22:49):

sure, why not?

view this post on Zulip Kenny Lau (May 02 2018 at 22:49):

wow

view this post on Zulip Kevin Buzzard (May 02 2018 at 22:49):

It's the | that causes the trouble

view this post on Zulip Mario Carneiro (May 02 2018 at 22:49):

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

view this post on Zulip Kevin Buzzard (May 02 2018 at 22:49):

suddenly I have pow._main

view this post on Zulip Kenny Lau (May 02 2018 at 22:49):

yay we're on the same side for this time

view this post on Zulip Mario Carneiro (May 02 2018 at 22:49):

Yes, the | triggers the equation compiler

view this post on Zulip Mario Carneiro (May 02 2018 at 22:50):

It also gives you the correct (applied) equation lemma

view this post on Zulip Mario Carneiro (May 02 2018 at 22:50):

rather than the lambda equation lemma

view this post on Zulip Kenny Lau (May 02 2018 at 22:50):

I don't like that

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 02 2018 at 22:51):

What is an example of where this causes you problems?

view this post on Zulip Kenny Lau (May 02 2018 at 22:51):

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

view this post on Zulip Kenny Lau (May 02 2018 at 22:51):

I just don't like it

view this post on Zulip Kevin Buzzard (May 02 2018 at 22:51):

and I am asking why exactly

view this post on Zulip Kenny Lau (May 02 2018 at 22:52):

i don't know

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 02 2018 at 22:53):

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

view this post on Zulip Kenny Lau (May 02 2018 at 22:53):

I'm convinced you can't do it

view this post on Zulip Kenny Lau (May 02 2018 at 22:53):

you need a higher order functional

view this post on Zulip Kenny Lau (May 02 2018 at 22:54):

since chNat lives in Type 1

view this post on Zulip Kenny Lau (May 02 2018 at 22:54):

you need an empowered chNat that lives in Type 2

view this post on Zulip Kenny Lau (May 02 2018 at 22:54):

Ackermann isn't primitive recursive

view this post on Zulip Kenny Lau (May 02 2018 at 22:54):

its image is in Delta_1 not Delta_0

view this post on Zulip Kenny Lau (May 02 2018 at 22:54):

in the arithmetic hierarchy

view this post on Zulip Kevin Buzzard (May 02 2018 at 22:54):

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

view this post on Zulip Kenny Lau (May 02 2018 at 22:54):

whatever that means

view this post on Zulip Kevin Buzzard (May 02 2018 at 22:54):

(for good reason!)

view this post on Zulip Mario Carneiro (May 02 2018 at 22:54):

what ackermann church question

view this post on Zulip Kevin Buzzard (May 02 2018 at 22:54):

fill in the def above

view this post on Zulip Kenny Lau (May 02 2018 at 22:54):

@Mario Carneiro make ackermann using church

view this post on Zulip Kevin Buzzard (May 02 2018 at 22:55):

so that it commutes with usual ack on nat

view this post on Zulip Kenny Lau (May 02 2018 at 22:55):

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

view this post on Zulip Kevin Buzzard (May 02 2018 at 22:55):

I don't have a clue

view this post on Zulip Mario Carneiro (May 02 2018 at 22:55):

You can do it

view this post on Zulip Kevin Buzzard (May 02 2018 at 22:55):

I just think this is really cool :-)

view this post on Zulip Kevin Buzzard (May 02 2018 at 22:55):

How do you know you can do it?

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 02 2018 at 22:56):

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

view this post on Zulip 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"

view this post on Zulip Kenny Lau (May 02 2018 at 22:57):

the former

view this post on Zulip Mario Carneiro (May 02 2018 at 22:57):

I mean there is a solution in less than 50 chars

view this post on Zulip Kevin Buzzard (May 02 2018 at 22:57):

:-)

view this post on Zulip Kenny Lau (May 02 2018 at 22:57):

??????

view this post on Zulip Kenny Lau (May 02 2018 at 22:57):

50 chars....

view this post on Zulip Mario Carneiro (May 02 2018 at 22:57):

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

view this post on Zulip Kevin Buzzard (May 02 2018 at 22:57):

that's not polynomial time though

view this post on Zulip Mario Carneiro (May 02 2018 at 22:58):

heck no

view this post on Zulip Kevin Buzzard (May 02 2018 at 22:58):

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

view this post on Zulip Kevin Buzzard (May 02 2018 at 22:59):

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

view this post on Zulip Kenny Lau (May 02 2018 at 22:59):

@Mario Carneiro so what is wrong with my analysis?

view this post on Zulip Mario Carneiro (May 02 2018 at 22:59):

Ah, I see what you mean now

view this post on Zulip Mario Carneiro (May 02 2018 at 23:00):

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

view this post on Zulip Kenny Lau (May 02 2018 at 23:00):

exactly

view this post on Zulip Mario Carneiro (May 02 2018 at 23:00):

but lean has universe issues

view this post on Zulip Kenny Lau (May 02 2018 at 23:00):

we're in typed lamdba calculus

view this post on Zulip 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)}

view this post on Zulip Kevin Buzzard (May 02 2018 at 23:00):

which comes with a free theorem

view this post on Zulip Mario Carneiro (May 02 2018 at 23:00):

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

view this post on Zulip Kevin Buzzard (May 02 2018 at 23:01):

oh wait I can do it by cheating!

view this post on Zulip Kevin Buzzard (May 02 2018 at 23:01):

There's a projection from church nat to nat

view this post on Zulip Mario Carneiro (May 02 2018 at 23:01):

exactly

view this post on Zulip Mario Carneiro (May 02 2018 at 23:01):

so you do an induction on nat -> nat

view this post on Zulip Kenny Lau (May 02 2018 at 23:02):

that's cheating

view this post on Zulip Kevin Buzzard (May 02 2018 at 23:02):

so I can define an "incorrect" pow

view this post on Zulip Kevin Buzzard (May 02 2018 at 23:02):

But this is cheating

view this post on Zulip Kevin Buzzard (May 02 2018 at 23:02):

Is this what they do with pred?

view this post on Zulip Mario Carneiro (May 02 2018 at 23:02):

like I said, you need inductive types

view this post on Zulip Kenny Lau (May 02 2018 at 23:02):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 02 2018 at 23:02):

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

view this post on Zulip Kevin Buzzard (May 02 2018 at 23:02):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (May 02 2018 at 23:04):

solve the halting problem of course

view this post on Zulip Kevin Buzzard (May 02 2018 at 23:04):

in the proof I'm envisaging

view this post on Zulip Kenny Lau (May 02 2018 at 23:04):

you...

view this post on Zulip Kevin Buzzard (May 02 2018 at 23:04):

:-)

view this post on Zulip Kevin Buzzard (May 02 2018 at 23:04):

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

view this post on Zulip Mario Carneiro (May 02 2018 at 23:09):

wait, no I lied again, it is possible

view this post on Zulip Kenny Lau (May 02 2018 at 23:09):

hmm

view this post on Zulip Mario Carneiro (May 02 2018 at 23:09):

the motive is X → X

view this post on Zulip Kenny Lau (May 02 2018 at 23:10):

you need to store a function each time

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 02 2018 at 23:20):

That makes me slightly sad

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 02 2018 at 23:24):

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

view this post on Zulip Kevin Buzzard (May 02 2018 at 23:25):

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

view this post on Zulip 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}

view this post on Zulip Kevin Buzzard (May 02 2018 at 23:30):

Do you think that's the same?

view this post on Zulip Kevin Buzzard (May 02 2018 at 23:30):

You are quantifying over g too

view this post on Zulip Kevin Buzzard (May 02 2018 at 23:31):

It might be the same

view this post on Zulip Mario Carneiro (May 02 2018 at 23:34):

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

view this post on Zulip Mario Carneiro (May 02 2018 at 23:34):

and it doesn't require evaluating m at a function type

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 02 2018 at 23:36):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 02 2018 at 23:38):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 02 2018 at 23:49):

This is really interesting

view this post on Zulip Kevin Buzzard (May 02 2018 at 23:49):

I identified nat as the universal object

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 02 2018 at 23:50):

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

view this post on Zulip Kevin Buzzard (May 02 2018 at 23:50):

I think I see what I'm missing

view this post on Zulip Kevin Buzzard (May 02 2018 at 23:51):

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

view this post on Zulip Kevin Buzzard (May 02 2018 at 23:51):

and I would be assuming m was a functor

view this post on Zulip Kevin Buzzard (May 02 2018 at 23:51):

and trying to represent it

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 03 2018 at 01:12):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 03 2018 at 01:23):

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

view this post on Zulip Kevin Buzzard (May 03 2018 at 01:23):

I want to say that Type is a category.

view this post on Zulip Mario Carneiro (May 03 2018 at 01:23):

It is

view this post on Zulip Kevin Buzzard (May 03 2018 at 01:23):

Then m wants to be a functor from Type to Type

view this post on Zulip Kevin Buzzard (May 03 2018 at 01:23):

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

view this post on Zulip Mario Carneiro (May 03 2018 at 01:24):

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

view this post on Zulip Mario Carneiro (May 03 2018 at 01:24):

i.e. everything is functorial

view this post on Zulip Kevin Buzzard (May 03 2018 at 01:24):

I don't know what that means

view this post on Zulip Mario Carneiro (May 03 2018 at 01:24):

HoTT is a lot like this

view this post on Zulip Kevin Buzzard (May 03 2018 at 01:24):

Oh I see

view this post on Zulip Mario Carneiro (May 03 2018 at 01:24):

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

view this post on Zulip Mario Carneiro (May 03 2018 at 01:25):

everything is "fibrant"

view this post on Zulip Mario Carneiro (May 03 2018 at 01:25):

whatever that means

view this post on Zulip Kevin Buzzard (May 03 2018 at 01:25):

Let me modify Type

view this post on Zulip Kevin Buzzard (May 03 2018 at 01:25):

so that its objects are still terms whose type is Type

view this post on Zulip Mario Carneiro (May 03 2018 at 01:25):

but that's basically why univalence works

view this post on Zulip Kevin Buzzard (May 03 2018 at 01:25):

but the morphisms are equivs

view this post on Zulip Kevin Buzzard (May 03 2018 at 01:25):

Now m is a map on objects

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 03 2018 at 01:26):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 03 2018 at 01:27):

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

view this post on Zulip Mario Carneiro (May 03 2018 at 01:27):

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

view this post on Zulip Mario Carneiro (May 03 2018 at 01:28):

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

view this post on Zulip Mario Carneiro (May 03 2018 at 01:28):

I think that's going to be true in general

view this post on Zulip Mario Carneiro (May 03 2018 at 01:28):

It really is a functoriality condition

view this post on Zulip Kevin Buzzard (May 03 2018 at 01:29):

You have to be careful

view this post on Zulip Kevin Buzzard (May 03 2018 at 01:29):

Given a map A to B

view this post on Zulip Mario Carneiro (May 03 2018 at 01:29):

it's just this weird higher order functoriality thing

view this post on Zulip Mario Carneiro (May 03 2018 at 01:29):

It seems like logical relations generate the condition well

view this post on Zulip Kevin Buzzard (May 03 2018 at 01:29):

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

view this post on Zulip Kevin Buzzard (May 03 2018 at 01:30):

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

view this post on Zulip Kevin Buzzard (May 03 2018 at 01:30):

I can only see a functor in the equiv category

view this post on Zulip Kevin Buzzard (May 03 2018 at 01:31):

Maybe we mean different things by functorially

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 03 2018 at 01:31):

and I can always do this

view this post on Zulip Mario Carneiro (May 03 2018 at 01:31):

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

view this post on Zulip Mario Carneiro (May 03 2018 at 01:32):

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

view this post on Zulip Kevin Buzzard (May 03 2018 at 01:33):

I can't make that concept into a functor

view this post on Zulip Kevin Buzzard (May 03 2018 at 01:34):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 03 2018 at 01:36):

where a : X -> Y is our fixed morphism to commute over

view this post on Zulip Mario Carneiro (May 03 2018 at 01:37):

Applying this definition to [(R -> R) -> R -> R] gives exactly the condition I wrote down

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 03 2018 at 01:44):

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

view this post on Zulip 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