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
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. ...
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 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. ...
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 ...
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 (...
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 ...
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 ...
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 ...
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 ...
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 ...
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.
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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. ...
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