Questions tagged [type-theory]
Use this tag for questions about type theories, which are formal systems to specify properties of objects.
35
questions
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 ...
- 133
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.
...
- 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 (...
- 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 ...
- 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.
- 1,721
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 ,...
- 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 ...
- 1,721
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 ...
- 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/...
- 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 ...
- 1,721
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
...
- 736
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 ...
- 1,721
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 ...
- 893
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 ...
- 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 ...
- 893
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 ...
- 893
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.
...
- 893
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 ...
- 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 ...
- 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 &...
- 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 ...
- 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 ...
- 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 ...
- 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 ...
- 356
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 ...
- 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/...
- 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 ...
- 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 ...
- 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 ...
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 ...
- 221
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'...
- 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}...
- 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 ...
- 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 ...
- 1,881
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 ...
- 432