Skip to main content

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
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 ...
12121's user avatar
  • 175
4 votes
2 answers
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 ...
Naïm Favier's user avatar
1 vote
0 answers
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 ...
James Bowery's user avatar
2 votes
2 answers
148 views

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

Suppose, for example, we want to type-check the following term: ...
MaiaVictor's user avatar
3 votes
1 answer
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 ...
ice1000's user avatar
  • 6,256
3 votes
1 answer
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 ...
Bruno's user avatar
  • 227
1 vote
3 answers
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 ...
Hiroki Chen's user avatar
0 votes
0 answers
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 ...
Russoul's user avatar
  • 345
3 votes
1 answer
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? ...
Liu Xiaoyi's user avatar
4 votes
0 answers
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 ...
user23220385's user avatar
2 votes
1 answer
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 ...
Sasha Krassovsky's user avatar
3 votes
0 answers
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 ...
Cris P's user avatar
  • 345
0 votes
1 answer
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: ...
Tiago Campos's user avatar
5 votes
0 answers
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 ...
idka's user avatar
  • 73
2 votes
1 answer
138 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
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 ...
arshiamoeini's user avatar
4 votes
1 answer
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 ...
Trebor's user avatar
  • 4,015
4 votes
1 answer
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, ...
Trebor's user avatar
  • 4,015
1 vote
1 answer
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 ...
Gergely's user avatar
  • 311
2 votes
2 answers
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 ...
Tiago Campos's user avatar
4 votes
1 answer
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 ...
Russoul's user avatar
  • 345
2 votes
2 answers
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 ...
Julius Hamilton's user avatar
2 votes
1 answer
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 ...
Russoul's user avatar
  • 345
2 votes
1 answer
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 ...
Russoul's user avatar
  • 345
3 votes
2 answers
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 ...
Russoul's user avatar
  • 345
2 votes
0 answers
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 ...
user2361's user avatar
6 votes
2 answers
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?
Alex Byard's user avatar
1 vote
1 answer
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 ...
Russoul's user avatar
  • 345
5 votes
1 answer
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 ...
Trebor's user avatar
  • 4,015
5 votes
1 answer
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 ...
Ilk's user avatar
  • 547
4 votes
1 answer
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 ...
user32157's user avatar
  • 151
4 votes
0 answers
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 ...
Trebor's user avatar
  • 4,015
9 votes
1 answer
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 "...
Russoul's user avatar
  • 345
16 votes
3 answers
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 ...
Nathan's user avatar
  • 358
3 votes
1 answer
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 ...
Nico's user avatar
  • 722
10 votes
1 answer
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 ...
Mike Shulman's user avatar
  • 3,180
9 votes
1 answer
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 ...
Nico's user avatar
  • 722
22 votes
0 answers
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 ...
Mike Shulman's user avatar
  • 3,180
9 votes
1 answer
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} \...
Mike Shulman's user avatar
  • 3,180
2 votes
1 answer
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 ...
Jason Rute's user avatar
  • 8,835
4 votes
1 answer
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 ...
HighAsAKiteOnMath's user avatar
1 vote
1 answer
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 ...
bodacious_bandit's user avatar
0 votes
1 answer
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 ...
HighAsAKiteOnMath's user avatar
2 votes
1 answer
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. ...
Ms. Molly Stewart-Gallus's user avatar
4 votes
2 answers
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. ...
Ms. Molly Stewart-Gallus's user avatar
3 votes
3 answers
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. ...
Jozef Mikušinec's user avatar
11 votes
3 answers
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 ...
Jozef Mikušinec's user avatar
6 votes
1 answer
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 ...
Mike Shulman's user avatar
  • 3,180
1 vote
1 answer
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 (...
Ember Edison's user avatar
4 votes
2 answers
181 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
  • 4,015