I should be asleep but guess what I'm not because I am plagued by congruence of convertibility

I'm beginning to think it isn't true as it stands
This was my suspicion from the very start anyway, I was just falsely convinced by Past Work™️

If congruence is true for all substitutions then to prove it isn't true I only need to find a single example where it cannot be proven from what I have, which is only "steps to the same thing" and eta

G = (A C: Type)
(B: A -> Type)
(f: (x:A) -> B x)
(h: ((x:A) -> B x) -> C)

G |- (\x: A. f x) ~ f
(yes good holds by eta)

G |- h (\x: A. f x) ~ h f
(questionable)

It's the substitution of the first convertibility into the application (h y) where y has the function type, so it should hold by congruence, but it doesn't, because it's not the steps-to-same-thing rule (it doesn't step) and it's not eta (doesn't step to a syntactic function)

Follow

Have I been trying to prove something that doesn't hold this entire time

otoh I think transitivity does hold since eta sort of only "expands" once anyway

I am going to march up to INRIA headquarters and complain that their convertibility judgement isn't congruent

Sign in to participate in the conversation
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.