Type theory in cosmology?

I ran across something interesting in the book Cosmology by Liebscher (2005). A conundrum known as Olbers's paradox has provided motivation for cosmological considerations. This paradox demonstrates that, if there were an infinity of potentially observable stars, the sky should have infinite brightness. Modern cosmology takes this as a proof that the universe has a history in which there were no stars, and thus the number of stars we can see by looking far enough away from Earth is effectively limited by time.

There is an alternative attempt to resolve this paradox, credited to Lambert (1761), which assumes the universe consists of systems of different order. As Liebscher describes, "a system of order n contains g_n systems of order n-1, where g_n is the multiplicity. . . now every integral over the universe may converge." This naturally reminded me of type theory being invoked to resolve paradoxes of semantics etc. Lambert's "ordered universe" cosmology is known to be inadequate because it predicts an inhomogeneous universe at every distance scale, which is contrary to observation. Many would also say that type theory is an inadequate solution for our problems in logic and linguistics.