Bowuigi: i have just discovered myself that it is possible to do this. in a non-modal frp setting, we can posit the context "Gamma = (mkStream : Type -> Type), (n : Nat), (worldVector abbrev wvec : Finite n -> Exists (T : Type). mkStream T), (worldClosure : (T : Type) -> mkStream T -> Exists (fin : Finite n). leftProjection (wvec fin) = T)" where "Exists ... : ... -> (..., ...)" is the dependent... ... pair function that encodes the proposition (the right term) that something (the left term) exists, with "leftProjection" and "rightProjection" being the functions that extract from an "existsTerm : Exists ..." the left term (said to exists) and the right term (encoding the proposition stating what exactly the left term satisfies). then "wvec" is a term whose value is the "n"-length vector containing the reactive streams... ... defining the "real world" in our context, and finally "worldClosure" is the term whose type tells us that only the streams in "wvec" define our world. then, the judgment "Gamma, ..., (A : Type) |- streamValTerm : mkStream A", telling us "streamValTerm" is a stream-value and so "mkStream A" is non-empty type encoding a stream, allows us to infer "Gamma, ..., (A : Type) |- Exists (fin : Finite n). leftProjection (wvec... ... fin) = A", i.e., "A" is just one of the initial stream-making types that we used to set our world up.