English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

When we investigate a type system, it is helpful if we can establish thewell-foundedness of types or terms with respect to a certain hierarchy, and theExtended Calculus of Constructions (called $ECC$, defined and studiedcomprehensively in [Luo,1994]) is no exception. However, under a very naturalhierarchy relation (called the cumulativity relation in [Luo,1994]), thewell-foundedness of the hierarchy does not hold generally.  In this article,we show that the cumulativity relation is well-founded if itis restricted to one of the following two natural families of terms:  \begin{enumerate}  \item types in a valid context  \item terms having normal forms  \end{enumerate}  Also, we give an independent proof of the existence of principal types in$ECC$ since it is used in the proof of well-foundedness of cumulativityrelation in a valid context although it is often proved by utilizing thewell-foundedness of the hierarchy, which would make our argument circular ifadopted.

On principal types and well-foundedness of the cummulativity relation in ECC