Paper Info
Title
A Construction of Type: Type in Martin-Löf's Partial Type Theory with One Universe
Abstract
ing on w and pairing with oe(p(c); (x)Ap(q(c); x) ! p(c)) in the first coordinateyieldshoe(p(c);(x)Ap(q(c); x) ! p(c));(w)(Ap(q(c); p(w)); (x)Ap(q(c); Ap(q(w); x)))i 2 PAR;i.e. s (c) 2 PAR.We define the operator that builds the universe (U1; T1) by puttingf(c) := s (c) +hn 1 ; (x)R 1 (x; p(c))i;for c 2 PAR, and let e := fix((c)f(c)). Hence e 2 PAR is a fixed point of f ,e = f(e). The right summand of f corresponds to the rules (2).We now interpret Type:Type. The universe ...
Year
DOI
Venue
1991
10.2178/jsl/1183743747
J. Symb. Log.
DocType
Volume
Issue
Journal
56
3
Citations 
PageRank 
References 
1
0.43
3
Authors
1
Name
Order
Citations
PageRank
Erik Palmgren123343.17