The tag has no wiki summary.

learn more… | top users | synonyms

10
votes
2answers
1k views

What is the manner of inconsistency of Girard's paradox in Martin Lof type theory

I am aware that assigning the type of Type to be Type (rather than stratifying to a hierarchy of types) leads to an inconsistency. But does this inconsistency allow the construction of a well-typed ...
7
votes
4answers
872 views

Can dependent sums be encoded as dependent products?

Please forgive any unorthodox notation or obvious errors here... I'm trying to get an intuition for dependently typed languages, so I'm starting out by seeing which analogies I can take from the ...
3
votes
1answer
458 views

What notions of universe does predicative type theory admit?

Palmgren (1997), On universes in type theory, discusses work of several theorists that provide what we might call a family of Large Universe Axioms (LUAs) for predicative type theory, culminating in ...
6
votes
2answers
657 views

Recursively dependent types?

Is there such a thing as "recursively dependent types"? Specifically, I would like a dependent type theory containing a type $A(x)$ which depends on a variable $x: A(z)$, where $z$ is a particular ...
13
votes
7answers
2k views

What is lambda calculus related to?

So I'm not much of a math guy but I've really enjoyed programming in Lisp and have become interested in the ideas of lambda calculus which it is based. I was wondering if anyone had a suggestion ...