Questions tagged [type-rule]

In type theory, a type rule is an inference rule that describes how a type system assigns a type to a syntactic construction. These rules may be applied by the type system to determine if a program is well typed and what type expressions have. (from Wikipedia)

Filter by
Sorted by
Tagged with
9 votes
2 answers

What's the benefit of having pi and sigma types with an invariant parameter?

Ulf Norell wrote this in his PhD thesis (figure 1.6): This contradicts my stereotype on pi & sigma types, where pi parameter should be contravariant and sigma parameter is covariant. Why is Agda ...
10 votes
0 answers

Is there a proof assistant (or an embedding) for the (co)end calculus?

A Higher-Order Calculus for Categories describes a system where you can conveniently perform manipulations with categories, functors, Yoneda embeddings etc. An example of the rules is: $$\frac{\Gamma ,...
14 votes
2 answers

Tools for checking the consistency of a type theory

My question is twofold: How do you define consistency (analogously to the concept in first-order logic) in the context of a type theory? Are there any tools that can check consistency? I have seen a ...
18 votes
2 answers

What is the difference between judgmental equality, definitional equality, and equality types?

This answer to this question about η-equivalence in Coq draws a distinction between judgmental equality and definitional equality. In the simply typed lambda calculus (henceforth STLC), the following ...