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)

Filter by
Sorted by
Tagged with
3 votes
1 answer

Universe polymorphism and modules in Coq

The following code (without universe polymorphism) is accepted by Coq (8.16.0) : ...
  • 133
1 vote
0 answers

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): <...
  • 445
1 vote
2 answers

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: ...
  • 317
5 votes
1 answer

Unexpected eta expansion in constant definition

Start from this example in section 2.1.14: Polymorphic Universes in Coq's reference maunual (slightly modified): ...
9 votes
2 answers

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 ...
7 votes
1 answer

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: ...
15 votes
1 answer

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, ...
13 votes
0 answers

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-...
  • 455
6 votes
1 answer

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 ...
11 votes
1 answer

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 ...
  • 3,061
10 votes
2 answers

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,611
11 votes
1 answer

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

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 ...