Questions tagged [type-theory]
Use this tag for questions about type theories, which are formal systems to specify properties of objects.
64
questions
3
votes
1
answer
85
views
State of art for observational equality, on the injectivity requirement
I am reading through the papers, "Observational equality, now!" (${TT}^{obs}$) and "Impredicative Observational Equality" (${CC}^{obs}$) by Pujet and Tabareau, and I am trying to ...
- 497
4
votes
1
answer
183
views
What types can be written in Kind but not Lean?
The Kind programming language has a sufficiently powerful type system to support proving theorems like in Lean, Coq, Idris, or Agda. I've seen it said that Kind has an even more powerful type system ...
- 151
4
votes
0
answers
65
views
Independence of function extensionality
Who first realized that function extensionality cannot be proved within vanilla MLTT, or some variations of it? Now to my knowledge the simplest way to show this is by syntactic models. But surely ...
- 3,261
9
votes
1
answer
160
views
What is the intuition behind the `Glue` type in Cubical Type Theories
I have some clues regarding Glue based on a paper here and the accepted answer here.
The first resource says that Glue "...
- 91
14
votes
3
answers
220
views
Counterexamples in Type Theory
The title pretty much covers it. I'm wondering if someone is maintaining a list of counterexamples in type theory. I'm aware of Counterexamples in Type Systems, which I think is very nice, but I guess ...
- 328
3
votes
1
answer
115
views
Stacks versus universes
This is a vague question, and I apologize in advance for it. I do not need a definite answer, I am happy to just get some general ideas.
An elementary topos can model higher order logic over a ...
- 680
9
votes
1
answer
174
views
Universe inconsistency as an effect
The Internet tells me there is some work on languages that permit general recursion but carry information about possible divergence in the type system. For instance, the simply-typed language Koka ...
- 2,832
9
votes
1
answer
128
views
Interpretation of dependent types: Coherence
I have trouble understanding precisely how dependent type theories are intepreted in categories (in the most simple case, for example in a locally cartesian closed category). I know that a type in ...
- 680
22
votes
0
answers
441
views
Categorical semantics of Agda
I would like to know the state of the art regarding the categorical semantics of the type theory implemented by Agda — or at least some approximation of that type theory that is amenable to ...
- 2,832
8
votes
1
answer
155
views
Strong eta-rules for functions on sum types
I am wondering whether a rule like the following is consistent with decidable conversion and type-checking for dependent type theory:
$$ \frac{f\, g : (x:\mathsf{bool}) \to C~x\quad f~\mathsf{tt} \...
- 2,832
2
votes
1
answer
173
views
Is type checking in "Ideal Lean" computably enumerable?
There are actually two type theoretic foundations of Lean given in Mario Carneiro's master's thesis. They are the same, except for how definitional equality is treated:
“algorithmic” definitional ...
- 5,748
3
votes
1
answer
203
views
How can you represent a dependent type visually?
So, obviously for a term $t$ of type $T$, I would represent it as:
T
+-----------+
| |
| t |
| |
+-----------+
That is a node ...
1
vote
1
answer
107
views
How do I work with ints when using coq-of-ocaml for OCaml to Coq conversion?
I am trying to use coq-of-ocaml to convert a simple recursive factorial function written in OCaml into Coq. I have a testing_factorial.ml file which defines the ...
0
votes
1
answer
95
views
How do you implement what's in the Pierce Book precisely? And why / why not have evaluation just mutate ParseTree's of a PEG parser generator library?
Here is a link to the "Pierce Book" or Benjamin Pierce's draft transcript of (the first part of) "Types and Programming Languages".
On PDF page 28 you'll see an OCaml ...
2
votes
1
answer
72
views
How do clausal definitions work?
I'm most familiar with the metatheory of calculi based around expressions.
But systems like Agda use separate clauses for definitions.
...
- 2,628
4
votes
2
answers
130
views
Pragmatic encodings of inductive inductive types
What's the most pragmatic encoding for inductive-inductive types such as for a universe of types?
In pseudo Coq syntax.
...
- 2,628
2
votes
3
answers
169
views
Equality of records with members whose types are dependent (Lean 4)
(Previously, I asked
about converting a term a: A to a term of type B provided that A = B.
...
- 247
10
votes
3
answers
215
views
Given `A = B`, how to prove `a: A` also has type B in Lean 4
I guess my question can be reduced to implementing this function:
def abEq (A B : Type) (a: A) (ab : A = B): B := sorry
I am new to Lean 4 and started learning ...
- 247
6
votes
1
answer
283
views
Very dependent functions
A "very dependent function" is a function whose output type at input $n$ depends on its own output values at inputs $k<n$. Is there a precise definition of such things that makes sense ...
- 2,832
1
vote
1
answer
148
views
Does Agda's --injective-type-constructors flag have canonicity?
Since 2010/01/07, when the Anti-classicality of Agda was proved by Chung-Kil Hur, Agda's --injective-type-constructors is separated from the main branch of Agda (...
- 109
4
votes
2
answers
165
views
Formalization of abstract definitions
I'm asking about the abstract keyword in Agda and equivalent features in other languages. It marks a definition as non-expandable, potentially speeding up ...
- 3,261
2
votes
1
answer
156
views
What are references for learning type theory?
What could be a good set of references for starting to learn type theory? We can assume that the students have a computer science background but not specifically on functional programming or lambda ...
- 186
8
votes
0
answers
198
views
Alternatives to universe levels
All of the type theory based proof assistants that I have seen have an infinite hierarchy of type universes to avoid the type of types being a term of itself. Are there alternative systems which could ...
- 81
3
votes
1
answer
116
views
What's the difference between a computation rule and a definitional equality?
In http://www.cse.chalmers.se/~coquand/comp.pdf, Coquand said:
One important point is that we cannot hope this computation rule to be interpreted as a definitional equality, since reflexivity is not ...
- 5,424
6
votes
3
answers
462
views
How are the parts of category theory which make explicit reference to Set different when formalized in a proof assistant that is based on type theory
In category theory a presheaf is defined as a functor whose target is $\mathrm{Set}$, and the concept is used to state the Yoneda lemma. The appearance of $\mathrm{Set}$ in the definition comes from ...
0
votes
0
answers
86
views
Existential variables in dependent type theory
For the kernel of a proof assistant free variables/universal quantification may be sufficient. In higher level languages such as Coq's tactic language indeterminate variables (not sure of the wording ...
- 2,628
5
votes
1
answer
267
views
What is a weak function space and what does it have to do with HOAS?
What is a weak function space and what does it have to do with higher order abstract syntax?
I mean I know what a weak function space is. It's that thing you use for HOAS in Lambda Prolog or toolkits ...
- 2,628
3
votes
2
answers
134
views
What is a non-canonical term?
I've heard the phrase used in relation to comparing proof assistants, but I don't understand what it means.
For example, for introducing an instance of coinductive types, Agda uses destructors and ...
3
votes
1
answer
139
views
Is there any work on the use of free logic in proof assistants?
I've been reading up on free logic. I have a hunch it could be useful for type theory. For example, the fixed point of an expression might not always exist or an expression might not be well typed in ...
- 2,628
4
votes
1
answer
143
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 ...
- 237
6
votes
2
answers
203
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.
...
- 680
9
votes
1
answer
298
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 (...
- 3,261
10
votes
2
answers
480
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 ...
- 3,261
13
votes
2
answers
456
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.
- 2,628
10
votes
0
answers
174
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 ,...
- 3,261
8
votes
2
answers
364
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 ...
- 2,628
18
votes
2
answers
422
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 ...
- 429
17
votes
2
answers
763
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/...
- 181
6
votes
0
answers
105
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 ...
- 2,628
14
votes
2
answers
399
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
...
- 809
6
votes
1
answer
135
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 ...
- 2,628
15
votes
2
answers
292
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 ...
- 983
12
votes
0
answers
145
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,832
12
votes
3
answers
281
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 ...
- 983
17
votes
2
answers
409
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 ...
- 983
15
votes
1
answer
294
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.
...
- 983
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 ...
- 519
8
votes
2
answers
229
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 ...
- 5,424
10
votes
2
answers
402
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,651
21
votes
2
answers
304
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 ...
- 751