Sökning: "Initiality"

Hittade 1 avhandling innehållade ordet Initiality.

1. 1. A Proof and Formalization of the Initiality Conjecture of Dependent Type Theory

   Författare :Menno de Boer; Peter LeFanu Lumsdaine; Alexander Berglund; Bas Spitters; Stockholms universitet; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Dependent type theory; Category theory; Contextual categories; Initiality; Formalization; Mathematics; matematik; matematisk logik; Mathematical Logic;

   Sammanfattning : In this licentiate thesis we present a proof of the initiality conjecture for Martin-Löf’s type theory with 0, 1, N, A+B, ∏AB, ∑AB, IdA(u,v), countable hierarchy of universes (Ui)iєN closed under these type constructors and with type of elements (ELi(a))iєN. We employ the categorical semantics of contextual categories. LÄS MER