daniel gratzer on Nostr: nprofile1q…fw8t5 nprofile1q…sn7dy HOAS is perfectly compatible with funext ...

nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyry2ysn5av9pr8m76kgpggcflz294t0pr9shd99kh8redys7ku0xkefw8t5 (nprofile…w8t5) nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzs8jfr3se3redkc5mknpwqdlx8qhkhggjhshfwfv0nwv7ft76kuyusn7dy (nprofile…n7dy) HOAS is perfectly compatible with funext provided one works in the correct setting, akin to how one may use nominal sets to reason about binding via exponentiation by the type of names.