ReactiveX has become a standard model for event-driven programming and is used widely in the industry. A study of future types such as promises in JavaScript was carried out, describing future types with the future modality of linear-time temporal logic using Curry-Howard correspondence. In this work, we will try to extend the work on the promises to describe the more complicated type of observable (in the Rx sense) which is an infinite stream of events.