On Wednesday, 6 February 2019 05:13:35 UTC+1, Anders Mörtberg wrote: > > Consider the interval HIT, it is contractible and hence equivalent to > Unit. But it also lets you prove function extensionallity which you > definitely don't get from the Unit type. > I have the feeling that function extensionality is special in the sense that the proof that I know of, as well as that of function extensionality in ETT, relies on the fact that we can replace judgmentally equal terms under lambdas, which is like function extensionality for judgmental equality. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.