Questions tagged [type-theory]

Use this tag for questions about type theories, which are formal systems to specify properties of objects.

Filter by
Sorted by
Tagged with
3 votes
1 answer
107 views

What are instances of a dependent pair type?

Currently I am learning about dependent pair ($\Sigma$-)types, and I'm having some trouble understanding how an instance of a dependent type could be formed. I think I understand how the type of a ...
user avatar
5 votes
2 answers
152 views

How to prove in Lean that sums are distributive?

Assume we are given three types in Lean. constants A B C : Type There is a canonical map of the following form. ...
user avatar
  • 433
9 votes
1 answer
242 views

Current status of cubical inductive families

I have the impression that cubical type theory hasn't dealt with inductive families yet. But the only source on this matter I can get is this Agda issue. What I've gathered is Agda supports defining (...
user avatar
  • 2,246
11 votes
2 answers
423 views

Replacing (strict) positivity with monotonicity on propositions

When defining an inductive type, there is a famous "positivity" restriction on the constructor types. For example, an inductive type $\mathsf D$ has constructor $\mathsf c : F(\mathsf D) \to ...
user avatar
  • 2,246
11 votes
2 answers
310 views

What is a commuting conversion and why are they problematic?

Off and on I have heard of the jargon "commuting conversion" but I don't really know what it means. I've heard commuting conversions are problematic but I don't know why.
user avatar
11 votes
0 answers
153 views

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 ,...
user avatar
  • 2,246
9 votes
2 answers
275 views

What is hereditary substitution and why should I use it?

What is hereditary substitutio,n and why should I use it? I've been taking a look at hereditary substitution for my little programming language, because hereditary substitution is supposed to give a ...
user avatar
18 votes
2 answers
359 views

What are the motivations for different variants of categorical models of dependent type?

I am new to the categorical semantics for dependent type theories, so it is surprising for me to see nLab introduces so many variants of categorical models, including comprehension categories, display ...
user avatar
  • 419
13 votes
2 answers
606 views

What are "fibration/cofibration" in type theory and what are their intuitions?

I keep seeing these phrasing in some proof assistants/elaborators and their issues/internal discussions (e.g. Github search results in cooltt), that seems not that related to the actual proofs/...
user avatar
  • 141
7 votes
0 answers
98 views

Is every logical theory embeddable in a dependently typed extensional type theory?

In category theory by the Yoneda embedding every category $\mathcal{C}$ is a subcategory of a category of presheafs $[\mathcal{C}^{\text{op}}, \text{Set}]$. Every category of presheafs is a topos and ...
user avatar
14 votes
2 answers
364 views

Can mathematical formalizations in NuPRL be trusted as correct in the greater mathematical practice?

In A Cubical Language for Bishop Sets, the authors write: As a consequence of its fundamentally untyped nature, formalizing a theorem in Nuprl does not imply the correctness of the corresponding ...
user avatar
6 votes
1 answer
99 views

Typing proof trees or proof objects

Is there a theory of typing proof objects or proof trees? Partially inspired by this question and answer, I was wondering about separating type checking into two phases: the first phase infers a full ...
user avatar
14 votes
2 answers
234 views

What axioms have a computational interpretation?

The type of call/cc (which may be realized with the 𝜆𝜇-calculus) corresponds with Peirce's Law, which implies LEM. This answer by Pierre-Marie Pédrot explains how ...
user avatar
11 votes
0 answers
76 views

Rules for mutual inductive/coinductive types

Some proof assistants, like Agda and maybe Coq, allow families of mutually defined types, or nested definitions of types, in which some are inductive and others are coinductive. I have no idea what ...
user avatar
  • 2,079
11 votes
3 answers
210 views

Why does it matter if canonicity holds for irrelevant types?

Suppose you were to add a non-constructive axiom which only applies to irrelevant types, such as the irrelevance axiom. To my understanding canonicity and strong normalization are defining features of ...
user avatar
17 votes
2 answers
326 views

What is the trade-off to accepting impredicative propositions?

Impredicativity greatly increases the logical strength of a formal system, and impredicative propositions are also a consequence of various axioms including LEM and Zorn's Lemma. An impredicative sort ...
user avatar
14 votes
1 answer
255 views

Why should you "never resort to polymorphism when initiality would do"?

In the concluding statement of "universe hierarchies", Conor McBride calls it [...] that key lesson which I learned from James McKinna: never resort to polymorphism when initiality will do. ...
user avatar
16 votes
1 answer
1k views

So many data types, so little time

I find my mathematics and programming background$^*$ do not endow me with much understanding of type theory as it pertains to proof assistants. To remedy this shortcoming I don't expect a Royal Road ...
user avatar
  • 509
7 votes
2 answers
201 views

What's “conservativity” in terms of type theory and how is it useful?

I have heard that an extension to a type theory can be said to be conservative, which means it may add new formulae to the original type theory, for example new type formers and their intro/elim rules ...
user avatar
  • 4,136
11 votes
2 answers
319 views

What is a universe?

What is a universe? More specifically, Is a type system without a term-type distinction, are universes just ordinary types? If (1) is true, can we the system-builders freely choose which types are &...
user avatar
  • 2,467
20 votes
2 answers
240 views

In what intensional type theories can absurdity be made definitionally proof irrelevant?

Various type theories have, over the years, explored extending the definitional equality with a variety of eta-laws and various forms of proof irrelevance. Quite a lot of systems manage eta for ...
user avatar
  • 721
6 votes
1 answer
230 views

Type Theory research groups

Research about type theory, internal languages, intuitionism, constructivism, and proof assistants is, at the moment, not as fashionable as other branches of mathematics are, say for example algebraic ...
user avatar
  • 433
13 votes
2 answers
173 views

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 ...
user avatar
  • 2,467
13 votes
2 answers
166 views

What are the upsides and downsides of typed vs untyped conversion?

What are the tradeoffs between untyped and type-directed conversion in dependent type theory, and is there any consensus on what's "better"? Background Generally speaking, in dependent type ...
user avatar
13 votes
9 answers
408 views

How to represent mathematical partial functions in a type-theory based proof assistant?

For example, if I want to define multiplication inverse on the rational type, intuitively we would define: ÷ : Q -> <Q \ {0}> -> Q But how would I ...
user avatar
  • 4,136
7 votes
2 answers
189 views

Can the development of proof assistants make mathematicians switch their framework?

The Stack Exchange bot reminded me that I had committed myself to asking some questions, but please allow a possibly naive question, possibly of a philosophical nature rather than mathematical/...
user avatar
  • 173
3 votes
0 answers
76 views

What is the relation of $\lambda^\to$ and $\lambda^{\to\times}$ to cartesian closed categories?

I am learning about the categorical semantics of type theory. I've written some preliminary results in Agda. In particular, I partially proved that the contexts and substitutions of simply-typed ...
user avatar
  • 2,246
12 votes
3 answers
227 views

What are the possible kinds of type theories or logics with quotients?

As described in this answer, one of the differences between Coq and Lean is the presence of definitional quotients in the latter. By contrast, the absence of definitional quotients in Coq forces one ...
user avatar
  • 2,467
14 votes
3 answers
452 views

Bringing OOP features into proof assistants?

I am aware that some of the proof assistants (e.g., Isabelle/HOL, Coq) provide an implementation of the so-called record types. For example, the library HOL-Algebra associated with the standard ...
user avatar
12 votes
2 answers
129 views

What about dependent types is useful for theorem provers?

There are a good number of theorem provers which use dependent typing as a part of their type systems. It seems this proportion is much higher than in programming languages. So what is useful about ...
user avatar
32 votes
3 answers
436 views

What is predicativity?

Type systems, and the proof assistants based on them, are frequently divided into predicative and impredicative. What exactly does this mean? I've heard the slogan "impredicativity means you can'...
user avatar
  • 2,467
9 votes
1 answer
165 views

How does the elimination rule of the heterogeneous equality type imply a weak version of K?

A heterogeneous equality type has the former $$\cfrac{\Gamma\vdash A~\texttt{type} \quad \Gamma\vdash B~\texttt{type} \quad \Gamma\vdash a:A \quad \Gamma\vdash b:B}{\Gamma\vdash a\simeq b~\texttt{type}...
user avatar
  • 4,136
19 votes
2 answers
211 views

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 ...
user avatar
  • 2,467
24 votes
4 answers
531 views

What are the differences between MLTT and CIC?

In the theory and design of proof assistants based upon dependent types, I feel like there’s a somewhat cultural divide between the "MLTT" world (with Agda as the main representative proof ...
user avatar
27 votes
2 answers
597 views

What set-theoretic definitions can't easily be formalized in a type theory?

Most proof assistants (with some exceptions like Isabelle/ZF or the B method) rely on type theory. See also the MathOverflow question What makes dependent type theory more suitable than set theory for ...
user avatar
  • 432