>>12620816What you try to define as meta-numbers are known in type theory as codata (co-data, the dual of data).
Tldr: "finite" objects are called data, they are defined using constructors. Constructors take objects (eg, digits) and spit out data. For example, to build lists of digits,all you need the empty list [] as a starting point, and the `cons` constructor that takes as arguments a digit and a list, and returns a new list being the appending of the first argument to its second argument. Eg. cons(2, [1,9] ) = [2,1,9]
Now that works with finite, "transparent" objects such as lists. But we also have things like processes, networked computers, and streams. You can't model a computer with witch you're exchanging signals trough the network as data. Why? Well, firstly, you can say it's "generating" data, but it is not itself data. You can't, trough a network, download the computer itself and know its behavior for all time, as you would a piece of data. It's both "opaque/black-boxed" and "infinite". In the sense that you may continue to exchange data with the computer for an indefinite (possibly infinite) amount of time. You have no way of knowing when its communications will end.
Now how do we model such things? The answer is co-data (the categorical dual of data). Data is defined by what goes into building it ("constructors" that take arguments and spit out data), co-data is defined by what can be extracted from it ("observers" that take co-data as arguments and spit out results).
How do we model streams of digits? (say, a rough approximation of the base-10 numbers from 0 to 1). We define an abstract type `digit_stream`, with two observers:
`head` takes a digit stream and returns the first digit of the stream.
head ([3,5,9,2...) = [5,9,2,...
'tail' takes a digit_stream and returns the remainder-stream
tail([3,5,9,2...) = 3
cont.
