Skip to main content
24 votes
Accepted

Why not have `Prop : Set` in Coq?

As it often happens with Coq, the answer is historical reasons. In the original version dating back from 1984, Coq was based on the Calculus of Constructions, a barebone dependent type theory. In ...
Pierre-Marie Pédrot's user avatar
11 votes

What is a universe?

Note: I'm approaching this from a purely syntactic perspective. I'm sure that a deeper answer could be given from the semantic perspective. In all type theories I'm aware of, a universe is a type that ...
Matthew McQuaid's user avatar
9 votes
Accepted

What is a universe?

There's a simple criterion for a term $U$ to be a universe... If there exists $\Gamma, t, T$ such that $\Gamma \vdash t : T$ and $\Gamma \vdash T : U$. So, (1) is unproblematic, but (2) is false, (3) ...
Trebor's user avatar
  • 3,967
8 votes
Accepted

Explicit vs implicit universes in lean

Type* is just a shorthand for Type _, where the _ is a wildcard (or more accurately, a ...
Eric's user avatar
  • 971
7 votes
Accepted

Is coercion to a higher universe injective?

You did not specify whether you want Tarski or Russell universes, so let me do Tarski-style, as it is more reasonable anyhow. Suppose we have two universes $U$ and $V$ with $U : V$, and given $t : U$ ...
Andrej Bauer's user avatar
  • 9,194
6 votes

Universe inconsistency as an effect

I don't have an answer, but I would like to provide some buzzwords and references that will make it easier to find relevant literature. Some background information Computational effects and dependent ...
Andrej Bauer's user avatar
  • 9,194
6 votes
Accepted

Is it possible to prove (-> (= (Either Trivial Trivial) (left sole) (right sole)) Absurd) in Pie?

I think your argument is correct about being able to directly show that $\mathsf{left}\ x \neq \mathsf{right}\ y$. Traditionally the 'on paper' presentations of type theory do not require the motive ...
Dan Doel's user avatar
  • 982
6 votes
Accepted

Parameterized Datatypes in a Universe à la Tarski?

Arg : (c : Code) -> (El c -> Desc) -> Desc Are you sure this is what you mean? I think the usual constructor is closer to the following: ...
gallais's user avatar
  • 1,166
5 votes
Accepted

Cardinality of Type in a given universe

Equality is not provable. Indeed, it is consistent that univ.{u u+1} < #(Type u) at every level u. Recall that the universe ...
François G. Dorais's user avatar
4 votes
Accepted

Unexpected eta expansion in constant definition

Mike Shulman got it right: this is a tricky question of how Coq solves unification problems. In short, in the first definition Coq takes the heuristic solution of letting your hole be unified with <...
Meven Lennon-Bertrand's user avatar
4 votes
Accepted

Universe polymorphism and modules in Coq

If you go polymorphic, you should probably go all the way, and also use a polymorphic product type, like so: ...
Meven Lennon-Bertrand's user avatar
4 votes
Accepted

Feferman's universes for proof assistants?

The concrete suggestion you make, namely to use ZFC/S, is quite difficult to appraise. The only way to answer it is to actually try formalizing mathematics in it. One possibility is for you (or your ...
Andrej Bauer's user avatar
  • 9,194
4 votes
Accepted

Is there any universe polymorphic version of univalence?

At least in papers on cubical type theory, 'respecting equivalence' is somewhat independent of universes. There is a judgmental notion of paths: $$Γ,i ⊢ T\ \mathsf{type} \\ Γ,i ⊢ t : T$$ The top being ...
Dan Doel's user avatar
  • 982
3 votes
Accepted

How much duplication does universe polymorphism actually save us?

I don't have a statistical conclusion (I wish this question is still answerable without statistical analysis :D), but my impression on universe levels is that we usually use up to 2 different levels ...
ice1000's user avatar
  • 6,186
3 votes

Abstracting over large types in type theory

What you suggest is possible for certain kinds of type theories. For example, the $\lambda$-calulus $F_\omega$ (see Figure 2 of this paper) supports universal quantification over all types, and even ...
Andrej Bauer's user avatar
  • 9,194
3 votes
Accepted

Naive computation of propositional resizing

I realized the answer very quickly. It goes wrong immediately. In a context with O : {i : Level}(p : Type i) -> isProp p, we can formulate Russell's paradox with ...
Trebor's user avatar
  • 3,967
3 votes
Accepted

Universe polymorphism and Coq standard library

Sadly, at the moment, there are no standard-ish libraries using universe polymorphism. A similar question arose some time ago and the Coq Zulip, and it seems multiple people from multiple projects ...
Meven Lennon-Bertrand's user avatar
2 votes

increasing the universe level of a type in Lean by force

You can define a universe polymorphic version of Cat. ...
Christopher Hughes's user avatar
2 votes

Stacks versus universes

I am not a topos theorist, but here are my 2cts as a type theorist, so take it with a grain of salt. If you have universes in your ambient topos, whatever it is, then you can define internally there ...
Pierre-Marie Pédrot's user avatar
1 vote

Is it possible to prove (-> (= (Either Trivial Trivial) (left sole) (right sole)) Absurd) in Pie?

You can construct a function that translates left to 0 and right to 1, therefore I believe you can still prove your point. By ...
aish721's user avatar
  • 11

Only top scored, non community-wiki answers of a minimum length are eligible