Timeline for Function extensionality: does it make a difference? why would one keep it out of the axioms?
Current License: CC BY-SA 3.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 17, 2021 at 21:28 | comment | added | Ms. Molly Stewart-Gallus |
I wonder if you can restrict this to Prop. Something like forall (a : Type) (b : Prop) (forall (x : a), f x = g x) -> f = g
|
|
| Feb 1, 2014 at 0:14 | comment | added | Christoph-Simon Senjak | Canonicity means that every closed term of an inductive type normalizes into its canonical form, which is a term only containing its constructors. Like everything of type Nat normalizing to SSS...S0. | |
| Jan 31, 2014 at 16:37 | comment | added | darij grinberg | Is canonicity the idea that the equality type should be an inductive type? | |
| Jan 31, 2014 at 16:34 | comment | added | darij grinberg | What exactly is canonicity? And thanks for the link! | |
| Jan 31, 2014 at 11:34 | history | answered | Christoph-Simon Senjak | CC BY-SA 3.0 |