About logic, types and universes
Types of value are a great invention in programming. They are a tool for programmers that report errors in programs before errors are generated in a runtime. As Curry-Howard correspondence teaches us that programs are equal to proofs, type properties may be applied to different theories. For example, some theory may have its syntax and semantics that compose a type. If a theory problem does not conform this type, we may report a syntax or semantic error in the problem setup.
There is a pattern in logic I find particularly interesting regarding to types. Suppose we have a program as a whole in this form:
`((((A -> B) -> C) -> D) -> E) -> ...`,
where `A`, `B`, `C`, ... are logic expressions, and `B` a is subtype of `A`, `C` is a subtype of `B`, `D` is a subtype of `C`, and so on. The idea is that the whole expression should evaluate to true if all the elements are really subtypes each to other, respectively. Let's see how the whole expression behaves:
1. Assume `A` is a top type.
1.1. If there exist an `A` element, then we have a case for typechecking `B -> C` alone, possibly evaluating it to true
1.2. If `A -> B` evaluates to true, then we have a case for typechecking `C -> D` alone, possibly evaluating it to true
1.3. If `B -> C` evaluates to true, then we have a case for typechecking `D -> E` alone, possibly evaluating it to true
1.4. If `C -> D` evaluates to true, then we have a case for typechecking `E -> ...` alone, possibly evaluating it to true
1.5. ...
If `1.1`, `1.2`, ..., onwards all evaluate to true, then the whole `((((A -> B) -> C) -> D) -> E) -> ...` expression is tautology only under one questionable assumption: there has to exist an element of the top type `A`. But does that element really exist without explicitly stating it? Is this a place where we should apply `cogito ergo sum` point from phylosophy?
However, there is a workaround of this problem. In the topmost definition, If `B` follows from `A` by its content, and `C` follows from `A -> B` by its content, then we have a starting tautology spark that lights up the whole Universe of typed expressions without compromising to explicitly state anything outside of this Universe. Hence, we have a self sufficient Universe that evaluates to `true` at its boundary extent if the typing fits correctly each leaf in a sequence from `A` to `true`.