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
0 votes
1 answer
134 views

Why inductive types (or variants) are so rigid in terms of the set of constructors

An inductive type definition normally carries a set of constructors C, but I am not so sure why the set of constructors C is always once-for-all statically defined. For instance: ...
Tiago Campos's user avatar
5 votes
0 answers
213 views

Mere propositions and Consistency with Impredicativity, Excluded Middle and Large Elimination

Setup Current Understanding I've recently been trying to learn about the interaction of Impredicative Polymorphism, Large Elimination and Excluded Middle (notably, inconsistency). Notably, this is ...
idka's user avatar
  • 73
2 votes
1 answer
122 views

Provable `fun-ext`and "rewriting under binders" in intensional MLTT

I've noticed that the underlying judgemental machinery of intensional MLTT can be extended such that function extensionality becomes provable. Or in other words it becomes possible to "rewrite ...
Russoul's user avatar
  • 345
0 votes
0 answers
97 views

Formalization of partial functions for combinatorial counting

I need assistance in defining axioms for partial functions in total function theory that is available in Coq. Specifically, I'm looking for a constructive definition of a partial function that ...
arshiamoeini's user avatar
4 votes
1 answer
94 views

General method for disproving possibility of judgemental equality

There is a slick definition of categories (as a record type with eta-equality) such that taking the opposite category twice results in the original one judgementally. Similar tricks seems to exist for ...
Trebor's user avatar
  • 3,688
4 votes
1 answer
142 views

New types in higher order logic

From my understanding, most descriptions of higher order logic have a clear "phase distinction": We first describe the types, which are usually syntactically simple trees. For concreteness, ...
Trebor's user avatar
  • 3,688
1 vote
1 answer
22 views

Type class constaint is ignored in type synonym definition

My class constraint is ignored in a type synonym definition: for type_synonym 'value myTypeOperator = "'value::group_add" I get ...
Gergely's user avatar
  • 267
2 votes
2 answers
134 views

What if identity type in extensional type theory were possibly non-deterministic?

In extensional type theory, identity types are lifted to the definitional equality mechanism, this lead to a bunch of problems, and I imagine that's why they are not very popular. My question is if we ...
Tiago Campos's user avatar
4 votes
1 answer
168 views

Co-induction principle

It's known that Nat-ind = Nat-rec ⨯ Nat-initiality Has someone figured out how to define a suitable Conat-coind such that ...
Russoul's user avatar
  • 345
2 votes
2 answers
232 views

Is there a most flexible type theory or proof assistant?

My understanding is that a programming language designed for “doing math” would basically: Be able to represent mathematical ideas (hopefully in a similar way to non-programmatic mathematical ...
Julius H.'s user avatar
  • 175
2 votes
1 answer
98 views

Is existence of Stream as final co-algebra for the suitable functor enough to write functions into equality of streams by co-induction in ExtMLTT?

Suppose we work inside MLTT with equality reflection (extensional MLTT). Assume I postulate existence of Streams as final co-algebra for the suitable functor. Is that enough to prove the bisimulation ...
Russoul's user avatar
  • 345
2 votes
1 answer
86 views

Abstracting over large types in type theory

In dependent type theory usually the typing context lets you abstract over arbitrary elements of some (dependent) types. Now if one wants to abstract over an arbitrary (but not quite) type, they can ...
Russoul's user avatar
  • 345
3 votes
2 answers
134 views

State-of-the-art constructive encodings of Reals in a (constructive) type theory that supports quotient-types

I don't think a particular choice of such type theory matters much. Extensional MLTT, SetoidTT, OTT, HoTT, HOTT, CuTT -- they all support quotient types. Reals is supposed to be a Set (in HoTT ...
Russoul's user avatar
  • 345
2 votes
0 answers
52 views

Tool for typing mathematical physics, e.g. differential geometry

Many expressions in mathematical physics use a rather sloppy notation, e.g. the Lie bracket on a vector field is defined using ambiguous notation, where $X : M \rightarrow TM$ is first defined as a ...
user2361's user avatar
5 votes
2 answers
307 views

Type Theory Lean 3 to Lean 4

I'm aware of Lean's type theory. Did the type theory of lean change at all as we moved to Lean 4? Are there any references to this?
Alex Byard's user avatar
1 vote
1 answer
77 views

Is every type-theoretic function ℕ → A extensionally equal to one written in terms of the ℕ-eliminator

In Category Theory the Natural Numbers object ℕ has the universal mapping-out property that tells us how to build arrows out of ℕ into an arbitrary object A. But it doesn't say that every arrow ...
Russoul's user avatar
  • 345
4 votes
1 answer
421 views

Semantics of type theory

There are many tools regarding the semantics of type theory. On one hand, we may organize the structure of substitutions explicitly, resulting in notions such as CwFs, CwAs, natural models, display ...
Trebor's user avatar
  • 3,688
5 votes
1 answer
151 views

State of art for observational equality, on the injectivity requirement

I am reading through the papers, "Observational equality: Now for good" (${TT}^{obs}$) and "Impredicative Observational Equality" (${CC}^{obs}$) by Pujet and Tabareau, and I am ...
Ilk's user avatar
  • 517
4 votes
1 answer
232 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 ...
user32157's user avatar
  • 151
4 votes
0 answers
90 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 ...
Trebor's user avatar
  • 3,688
9 votes
1 answer
232 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 "...
Russoul's user avatar
  • 345
15 votes
3 answers
264 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 ...
Nathan's user avatar
  • 348
3 votes
1 answer
139 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 ...
Nico's user avatar
  • 722
10 votes
1 answer
218 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 ...
Mike Shulman's user avatar
  • 2,912
9 votes
1 answer
159 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 ...
Nico's user avatar
  • 722
22 votes
0 answers
513 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 ...
Mike Shulman's user avatar
  • 2,912
9 votes
1 answer
227 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} \...
Mike Shulman's user avatar
  • 2,912
2 votes
1 answer
216 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 ...
Jason Rute's user avatar
  • 7,240
4 votes
1 answer
239 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 ...
Daniel Donnelly's user avatar
1 vote
1 answer
114 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 ...
bodacious_bandit's user avatar
0 votes
1 answer
104 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 ...
Daniel Donnelly's user avatar
2 votes
1 answer
73 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. ...
Molly Stewart-Gallus's user avatar
4 votes
2 answers
146 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. ...
Molly Stewart-Gallus's user avatar
3 votes
3 answers
510 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. ...
Jozef Mikušinec's user avatar
11 votes
3 answers
377 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 ...
Jozef Mikušinec's user avatar
6 votes
1 answer
369 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 ...
Mike Shulman's user avatar
  • 2,912
1 vote
1 answer
196 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 (...
Ember Edison's user avatar
4 votes
2 answers
173 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 ...
Trebor's user avatar
  • 3,688
2 votes
1 answer
192 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 ...
Pietro Braione's user avatar
8 votes
0 answers
253 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 ...
Shuchy's user avatar
  • 81
3 votes
1 answer
129 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 ...
ice1000's user avatar
  • 5,877
6 votes
3 answers
525 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 ...
anime cat girl's user avatar
0 votes
0 answers
94 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 ...
Molly Stewart-Gallus's user avatar
5 votes
1 answer
297 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 ...
Molly Stewart-Gallus's user avatar
3 votes
2 answers
157 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 ...
Robert Watson's user avatar
3 votes
1 answer
150 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 ...
Molly Stewart-Gallus's user avatar
4 votes
1 answer
196 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 ...
aradarbel10's user avatar
6 votes
2 answers
232 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. ...
Nico's user avatar
  • 722
9 votes
1 answer
340 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 (...
Trebor's user avatar
  • 3,688
10 votes
2 answers
512 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 ...
Trebor's user avatar
  • 3,688