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)

1 question with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
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 ,...
Trebor's user avatar
  • 3,867