I respect all directions of research in type theory. That being said, #AntiWTypeCrew, and I look forward to finally defeating it tomorrow
I've decided to pick four eta reductions as my hallowed laws and discarded the rest
I have not and will not prove that terms will normalize, but I think they do, since they're reduction rules and they go from bigger terms to smaller terms (no substitution required)
I'm not too sure about confluence since I did discard one big giant rule that's supposed to help the set be equivalent in some sense to the proper (but undecidable?) eta equivalence rule, but I've decided to solve that problem by not caring
Γ = (P: Unit -> Type), (x: Unit), (f: (x: Unit) -> P x)]
Jesus: One of you will betray me tonight.
Γ ⊢ case_P x of [() ⇒ f ()] ⇝ f x: Is it me, Jesus?
Γ ⊢ case_(λx. Unit) x of [() ⇒ ()] ⇝ x: Is it me, Jesus?
Jesus: It's not you either.
Γ ⊢ case_P x of [() ⇒ f ()] ⇝ f (): Is it me, Jesus?
Jesus: *mockingly* Is it meee, Jesuuus??
I could add a reduction rule that reduces anything of type Unit to ()... This would be for literally any inductive type shaped like a unit...... That feels cursed
Page 16 to 20
I'm not too pleased at the big arbitrary summary of basic types that I need to introduce at the bottom of p. 16 but I really didn't want to write all the typing rules out here and I'm sure eventually I'll have a section or chapter on MLTT types where all of that can go
Also Jordy did not like the eta contraction rules lol
A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.