# Tag Info

Accepted

### What is an algebraic data type?

[Note: After some helpful off-line remarks by Martín Escardó I have edited the part about general recursive types. It was at best misleading by trying to paint too simple a picture.] I will start with ...
• 9,573

### What is a Proof Assistant?

Let us clarify some jargon. Usually we call proof assistants systems which can really help us finding proofs, i.e. they should have a tactic language. Systems which lack this feature (tactics) are ...
• 1,297
Accepted

### What is a commuting conversion and why are they problematic?

Syntactically, commuting conversions are part of the $\eta$-rules for left-invertible types -- i.e., types which have pattern-matching eliminators. So if $e : A + B$, the $\eta$-equation for it looks ...
• 2,033

### What is a Proof Assistant?

The term "proof assistant" is usually used to describe a computer software that assists humans with developing formal proofs. A formal proof is a finite sequence of declarative sentences ...
• 1,165
Accepted

### What is a weak function space and what does it have to do with HOAS?

In category theory the adjective “weak” is used when the uniqueness parts of a universal property is removed. For example, a weak product of $A$ and $B$ is an object $P$ with morphisms $p_1 : P \to A$ ...
• 9,573
Accepted

### What is a Proof Assistant?

A proof assistant is a system that translates user input into a formal proof. Ideally, this formal proof should be verifiable by a third party. For example, the user designates a theorem they would ...
• 2,271
Accepted

### How did the meaning of "lifting" in proof assistants arise?

I totally agree that Lean's quotient.lift is disastrously-named as far as mathematicians are concerned. After discussion with the Lean devs it seems that it came ...
• 2,480

### What is a commuting conversion and why are they problematic?

In the comments, it was elaborated that one possible interpretation of a "commuting conversion" refers to $F(G(x))$ vs $G(F(x))$ where one of $F$ or $G$ is a recursor. The problem Here's an ...
• 971

As an additional bit of trivia: I found the following in Chapter 4 of the Coq Reference Manual, V8.4: For Cᴏǫ version V7, this Calculus was known as the Calculus of (Co)Inductive Constructions (Cɪᴄ ...
• 1,026

### Does ST$\lambda$C equal to simple type theory?

I share many of the sentiments of Li-yao Xia's answer and I would like to add some context from literature. For an interesting view of what some people think of, when they say simple type theory (...
• 547
Accepted

### Does ST$\lambda$C equal to simple type theory?

As a matter of modern terminology it's probably fine to identify "simple type theory" with simply typed lambda calculus, or only say STLC. But in the past it did refer to a somewhat specific ...
• 1,857
Accepted

### What is a 'truncation'?

Yes, truncations are a form of modalities, as explained in Section 7.7 of the HoTT book.
• 9,573
Accepted

As far as I know, the "Predicative" part refers to the existence of the type hierarchy. But the CIC/PCIC/PCUIC terminologies are not very fixed, and they can vary quite a lot between article…...
• 5,186
Accepted

### What is an eliminator?

The role of constructors and eliminators can be understood through category theory. For every type former (for example $A\times B$, $A+B$, $A^B$, $\mathbb N$, etc...) we can ask How can we construct ...
• 2,271
1 vote

### What's the difference between a computation rule and a definitional equality?

I think what Coquand means by "computation rule" is the fact that we have $\mathbf{J}(A,a,P,p,a',\mathbf{refl}(A,a,a)) \cong p$ for some notion of equality $\cong$, where (A : \Box), (a : ...
• 5,186
1 vote
Accepted

### Difference between implementation and formalisation in a proof assistant

To turn my comments into an answer: Typically one would talk about formalizing something which starts out as informal. So proof assistants are good at formalizing informal mathematical definitions ...
• 8,905

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