# Questions tagged [type-theory]

Use this tag for questions about type theories, which are formal systems to specify properties of objects.

93 questions
Filter by
Sorted by
Tagged with
297 views

### Why does #check add_mul (R := ℕ) return add_mul : ∀ (a b c : ℕ), (a + b) * c = a * c + b * instead of add_mul : Prop?

I don't understand why #check add_mul (R := ℕ) returns add_mul : ∀ (a b c : ℕ), (a + b) * c = a * c + b * c instead of ...
• 175
135 views

### Parametricity and data kinds

I am wondering about the MonoMaybe type family from the monad-validation Haskell library written by Alexis King. Its definition ...
• 287
1 vote
104 views

### Proving Quine's notion that identity belongs to logic within type-constrained proof assistants

I'm having difficulty generalizing the following proof to permit predicates of any finite arity. Consider the following axioms of identity consistent with W. V. O. Quine's argument that relative ...
• 111
148 views

### How exactly solved metas "revisited" in an efficient dependent type checker?

Suppose, for example, we want to type-check the following term: ...
• 123
185 views

### What is the well-established η law for naturals?

Notation. means a general equality. Well, $η$ laws are usually judgmental, but sometimes we provide $η$ laws as theorems. To me $η$ rules are like vibes, because ...
• 6,256
147 views

### What are deductive systems associated with raw type theories?

In the answer to a previous question I have been recommended to read this paper by Philipp Haselwarter and Andrej Bauer. In this paper a class of dependent type theories is formally defined. We are ...
• 227
1 vote
129 views

### Is there a way to incorporate K's axiom while keeping the system consistent with univalence?

It has been known that if a type $A$ has decidable equality, i.e., $\forall a b: A, a = b \vee a \neq b$, then we can happily say that any two proofs for $a = b$ must be identical. Sometimes, we will ...
• 420
119 views

### MLTT with first-order reasoning and equality-reasoning information preservation

Terms in Extensional MLTT don't contain equality-reasoning information (implicit transports), effectively meaning data is lost, which is bad. But at the same time, higher-order reasoning (reasoning ...
• 345
158 views

### Does equality in $\Sigma_{(x : X)} x = x$ implies UIP?

The short version: Is this statement correct? If it is, is it provable in Coq? ...
120 views

### Proving "proof methods" as theorems in type-theory based proof systems

For example, suppose we have proved associativity of some binary operator $+ : T \to T$ as add_assoc : forall (x y : T), x + y + z = x + (y + z). We can thus prove ...
169 views

### Are type universes related to proper classes from set theory?

I'm currently learning Lean 4, and in the book they mention that the type hierarchy was introduced to avoid a version of Russell's paradox. From reading a bit about set theory a while ago, I remember ...
92 views

### Limitations of simple type theory proof assistants for undergraduate-level mathematics?

I'm interested in understanding the practical power and limitations of simple type theory, particularly as compared with dependent type theory, in supporting formalized proofs of theorems liable to ...
• 345
159 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: ...
• 125
240 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 ...
• 73
138 views

### Provable fun-extand "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 ...
• 345
106 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 ...
99 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 ...
• 4,015
171 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, ...
• 4,015
1 vote
31 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 ...
• 311
143 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 ...
• 125
176 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 ...
• 345
268 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 ...
103 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 ...
• 345
101 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 ...
• 345
182 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 ...
• 345
68 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 ...
• 21
354 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?
• 486
1 vote
85 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 ...
• 345
463 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 ...
• 4,015
175 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 ...
• 547
276 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
106 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 ...
• 4,015
281 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 "...
• 345
302 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 ...
• 358
149 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 ...
• 722
245 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 ...
• 3,180
176 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 ...
• 722
564 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 ...
• 3,180
318 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} \...
• 3,180
243 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 ...
• 8,835
250 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
122 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 ...
129 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 ...
77 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. ...
153 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. ...
859 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. ...
697 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 ...
424 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 ...
• 3,180
1 vote
286 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 (...
• 269