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 Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

We present a set-theoretic, proof-irrelevant model for Calculus ofConstructions (CC) with predicative induction and judgmental equality inZermelo-Fraenkel set theory with an axiom for countably many inaccessiblecardinals. We use Aczel's trace encoding which is universally defined for anyfunction type, regardless of being impredicative. Direct and concreteinterpretations of simultaneous induction and mutually recursive functions arealso provided by extending Dybjer's interpretations on the basis of Aczel'srule sets. Our model can be regarded as a higher-order generalization of thetruth-table methods. We provide a relatively simple consistency proof of typetheory, which can be used as the basis for a theorem prover.

Proof-irrelevant model of CC with predicative induction and judgmental equality