New posts in Type Theory

Is simply typed lambda calculus with fixed-point combinator Turing-complete?

Why would the category of sets be intuitionistic?

What exactly is a judgement?

What is the definition of computational content?

History of the notation for substitution

Equivalent form of the Univalence Axiom

How do we express measurable spaces using type theory?

How true are theorems proved by Coq?

Can type constructors be considered as types in functional programming languages?

What is the correct term for _ in a type hint?