fact: CoInductive νTypeFrom n (X: (νTypeAt n).(prefix)): Type@{m'} := cons { this: (νTypeAt n).(Frame).(frame) (♢ n) X -> HSet@{m}; next: νTypeFrom n.+1 (X; this); }.
imports: Logic.FunctionalExtensionality Bonak(Notation) Bonak(RewLemmas) Bonak(HSet) Bonak(LeYoneda)