Исправление quasimoto, (текущая версия) :
Свойства же нужны не ссылки, а значения по ней. То есть надо прочитать, то есть погрузиться в IO, то есть вместо Set/Prop будет IO Set/Prop в роли Set/Prop (IO уровнем выше), что как-то не очень реально. То есть такой пи-тип — {A : Set} {P : A → Set} (ref : & A) → ? (* ref) P, непонятно, что делать с ?.
Исходная версия quasimoto, :
Свойства же нужны не ссылки, а значения по нему. То есть надо прочитать, то есть погрузиться в IO, то есть вместо Set/Prop будет IO Set/Prop в роли Set/Prop (IO уровнем выше), что как-то не очень реально. То есть такой пи-тип — {A : Set} {P : A → Set} (ref : & A) → ? (* ref) P, непонятно, что делать с ?.