# Tag Info

Accepted

### Why should you "never resort to polymorphism when initiality would do"?

Initiality comes with a powerful universal property which allows you to, internally, prove statements about the constructions you perform. If you give me an element of ...
• 1,264

### What are the advantages to impredicativity?

All impredicativity means is that propositions form a complete lattice! This is a basic principle of mathematics. So if you want to be able to use the architecture of mathematics developed in the last ...
• 2,053

### Which proof assistant would you advise me to learn (in 2022) considering my interests?

There is no single right answer and all of this will be highly subjective. Before I get into the details based on the subjects you want to learn, I would just say, pick something, play around with it,...
• 9,653
Accepted

### What are the advantages to impredicativity?

There are some tricks that only work when you have access to an impredicative universe. They tend to construct "the smallest object" of some kind, without an explicit construction, i.e. a ...
• 2,353

### Could Prop be the top universe?

I am going to interpret your + as "is an element of", i.e., you are asking for a hierachy of universes that looks like this: \mathsf{Set} : \mathsf{Type}...
• 10k

### Counterexamples in Type Theory

Coq maintains a document of historical proofs of absurdity, including brief explanations of the flaw that allowed them to pass. Most of these are more "counter-examples in type theory ...
• 1,547

### Inductive vs. recursive definitions

Defining recursive properties by fixpoint is possible, but it is usually easier to reason on inductively defined ones. Mostly because they come with their own induction principles. If you use fixpoint ...
Accepted

### Pragmatic encodings of inductive inductive types

Your example signature is negative recursive in the second field of Sigma so it can't be encoded in total languages. For internal universes, the usual solution is ...
• 2,077

### Figures on computer proof assistant usage

I don't have answers to most of your questions but another way to look at this question is which proof systems have formalized the most theorems. The largest scale effort that I know of to track ...
• 231
Accepted

### How can you represent a dependent type visually?

I addressed some of these questions in my lecture “Spartan Type Theory” (PDF slides) at the UniMath 2017 school in Birmingham. In particular, slide 18 looks like this: Please look at the slides for ...
• 10k

### Why is it hard to formalize informal proofs?

Are there any theoretical obstacles in formalizing what we actually do when we mentally verify equations, etc? Yes: we don't know what we actually do when we mentally verify equations! This is a glib ...
• 2,053
Accepted

### Naming conventions (letter case, underscores, &c) for Coq

A similar question was recently discussed in the Coq Zulip chat (regular link, no-login-needed link), of which this answer is a summary. The vstyle project is working on building / collecting Coq ...
• 946
Accepted

### Could we speed up ATP or ATD using a directed graph that appears to work like a gigantic brain?

Building that gigantic proof graph as an explicit graph would probably be a very bad idea, given its size and the complexity of "connecting inputs to outputs". Indeed, as you can have an ...
• 5,620

### Counterexamples in Type Theory

Making this a community wiki. Here are a few that come to mind, some more obvious than others, with a theme, and not described in detail. May add more later. A simply typed $\lambda$-term whose ...

### Inductive vs. recursive definitions

Let me just mention a third possibility which is sometimes called "small inversion". This is some kind of middle ground between the two possibilities you present, which gives you some of the ...
• 5,620

### Counterexamples in Type Theory

As mentioned in this answer on this site, so-called "positive coinductive types" break subject reduction.
Accepted

### Figures on computer proof assistant usage

I think one has to be a bit careful here. I wouldn't say the primary users of proof assistants would self identify as mathematicians. I think many use proof assistants for software and hardware ...
• 9,653

### Pragmatic encodings of inductive inductive types

To complement András' answer, and especially if you want to stay in Coq, you can also define such an internal universe using indexed inductive types only. Basically, you replace the definitions of ...
• 5,620
Accepted

### How does Lean4 (or a typical PA) represent lambda functions or in other words arbitrary expressions?

(This answer assumes you already know some of the basics of Lean as in Theorem Proving in Lean 4.) In a typical first logic class or set theory class in college, first order logic is presented as ...
• 9,653

### Which proof assistant would you advise me to learn (in 2022) considering my interests?

I really cannot improve on Jason Rute's answer, but one suggestion I would have: after playing around with whatever theorem prover you decided to use, dabble around with a few others. In particular, ...
• 1,574