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
2 votes
3 answers
75 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
121 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 ...
5 votes
1 answer
194 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,215
1 vote
1 answer
105 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
146 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 ...
  • 2,916
2 votes
1 answer
122 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 ...
7 votes
0 answers
177 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 ...
  • 71
3 votes
1 answer
105 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 ...
  • 4,740
6 votes
3 answers
436 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
79 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
248 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 ...
4 votes
2 answers
115 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 ...
2 votes
1 answer
84 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
121 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
178 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. ...
  • 508
9 votes
1 answer
270 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,916
10 votes
2 answers
445 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,916
13 votes
2 answers
421 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
164 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,916
8 votes
2 answers
314 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
387 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 ...
  • 427
17 votes
2 answers
689 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
101 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
377 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
105 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
253 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
124 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,215
12 votes
3 answers
244 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
356 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
275 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
213 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,740
10 votes
2 answers
370 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,593
21 votes
2 answers
270 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 ...
  • 741
7 votes
1 answer
240 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 ...
  • 508
12 votes
2 answers
206 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,593
13 votes
2 answers
204 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 ...
13 votes
9 answers
449 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,740
8 votes
2 answers
209 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/...
  • 183
4 votes
0 answers
80 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,916
13 votes
3 answers
248 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,593
15 votes
3 answers
470 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
145 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 ...
35 votes
3 answers
624 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,593
9 votes
1 answer
171 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,740
18 votes
2 answers
251 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,593
24 votes
4 answers
611 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 ...
28 votes
2 answers
717 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 ...
  • 427