Questions tagged [universe]
In mathematics, and particularly in set theory, category theory, type theory, and the foundations of mathematics, a universe is a collection that contains all the entities one wishes to consider in a given situation. (from Wikipedia)
23 questions
1
vote
1
answer
88
views
Terms are not types, but could I have Type be a subclass of Term in my OOP / C++ dependent type hierarchy?
Here's the code so far in "Type.h".
...
- 313
6
votes
2
answers
555
views
Could Prop be the top universe?
In the type theoretic domain (and I am specifically interested in constructive systems, should this be relevant to my question: I am not sure), AIUI, a typical hierarchy of universes looks like this:
<...
- 587
1
vote
0
answers
97
views
Heterogeneous lists, large indices
Recently I had cause to define a type of heterogeneous lists in Lean, and wrote
...
- 111
5
votes
1
answer
220
views
Universe polymorphism and Coq standard library
When developing in Coq with the Universe Polymorphism flag on, the standard library introduces unwelcome universe constraints because it is universe monomorphic.
Is there an alternative standard ...
- 75
0
votes
1
answer
156
views
increasing the universe level of a type in Lean by force
Given some term
A : Sort u
in Lean, is there a way to artificially increase the universe level and promote A to a term
...
- 732
8
votes
1
answer
267
views
Feferman's universes for proof assistants?
I asked this question on MathOverflow a few months ago, but received no answers.
There are some mathematicians who are comfortable with ZFC but uneasy with large cardinals. For them, it may be ...
- 505
2
votes
1
answer
108
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
2
votes
1
answer
135
views
Naive computation of propositional resizing
As far as I know, it is not known whether cubical type theories with propositional resizing admit computational interpretations. But here is an obvious attempt: Turn off universe checking locally, and ...
- 4,344
3
votes
1
answer
161
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 ...
- 732
11
votes
1
answer
276
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,270
4
votes
1
answer
114
views
Universe polymorphism and modules in Coq
The following code (without universe polymorphism) is accepted by Coq (8.16.0) :
...
- 175
1
vote
0
answers
188
views
Descriptions of heterogenous datatypes
When attempting to describe the datatype as appearing in my previous question, using indexed descriptions in style of The Gentle Art of Levitation to describe this datatype (using Agda for examples):
<...
- 547
1
vote
2
answers
257
views
Is it possible to prove (-> (= (Either Trivial Trivial) (left sole) (right sole)) Absurd) in Pie?
In this question, I am talking about the language Pie described in the book The Little Typer.
One can derive that $0=1$ is contradictory:
...
- 316
5
votes
1
answer
117
views
Unexpected eta expansion in constant definition
Start from this example in section 2.1.14: Polymorphic Universes in Coq's reference maunual (slightly modified):
...
- 90
9
votes
2
answers
563
views
Is coercion to a higher universe injective?
A type that is a member of a universe can be coerced into a higher universe. Is that coercion injective? That is, if two elements of U1 are equal after being coerced to U2, does that imply they are ...
- 153
8
votes
1
answer
440
views
Cardinality of Type in a given universe
I'm trying to determine the cardinality of Type u in Lean 3. So far I've been able to prove two inequalities:
...
- 183
20
votes
1
answer
1k
views
Why not have `Prop : Set` in Coq?
My understanding of Coq is that Prop : Type_1, Set : Type_1, and then Type_1 : Type_2, ...
- 303
13
votes
0
answers
386
views
Unintentionally proven false theorem with type-in-type outside logic and foundations?
We are all familiar with Russell's paradox, and it is known that Per Martin-Löf proved that type-in-type is normalizing and consistent (which is false), by accidentally using an assumption in his meta-...
- 484
6
votes
1
answer
260
views
Parameterized Datatypes in a Universe à la Tarski?
I'm wondering, is there a way to make a Universe à la Tarski that models all of the types in an open type theory, where there can be user defined parameterized inductive types?
For context, I'm trying ...
- 1,001
11
votes
1
answer
262
views
How much duplication does universe polymorphism actually save us?
From my rough impression, in (formalizing) everyday mathematics we almost never use universe polymorphism in a way that stretches the proof-theoretic strength. It merely saves us some duplication.
My ...
- 4,344
14
votes
2
answers
681
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 &...
- 3,561
11
votes
1
answer
276
views
Explicit vs implicit universes in lean
I've seen in mathlib several cases where the universes are explicit, that is Type u instead of Type*. Is there any advantage in ...
- 213
8
votes
1
answer
261
views
Is there any universe polymorphic version of univalence?
People would say in univalent type theory, anything you defined for types should respect equivalence since univalence told you equivalence equivalent to equality. But that's not correct. Only ...
- 690