Timeline for Problem with a proof in Wellfounded trees in categories
Current License: CC BY-SA 3.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 18, 2015 at 20:22 | comment | added | Andrej Bauer | You could also write an e-mail to Erik Palmgren. | |
| May 18, 2015 at 19:53 | comment | added | Luca Bressan | I tried, but without success. The problem seems to lie in the fact that the premise of the elimination rule is $x \in A, f \in B(x) \to W, z \in (\Pi u \in B(x))\, C(f(u)) \vdash d(x,f,z) \in C(\mathsf{sup}(x,f))$ and so I can't possibly exhibit a proof-term that $z$ preserves the equivalence relation (it's a variable!), even though I know that in the computation $z$ will be replaced by a function for which I could prove extensionality in principle. But if it's not clear I can expand my post. | |
| May 18, 2015 at 19:04 | comment | added | Andrej Bauer | This is just a guess, but maybe you need to use $W$-induction to simultaneously define $r$ and show that it is extensional. | |
| May 18, 2015 at 14:00 | history | asked | Luca Bressan | CC BY-SA 3.0 |