Skip to main content
30 votes
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 ...
Andrej Bauer's user avatar
  • 9,573
19 votes

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 ...
Namdak Tönpa's user avatar
11 votes
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 ...
Neel Krishnaswami's user avatar
11 votes

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 ...
Nike Dattani's user avatar
  • 1,165
8 votes
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$ ...
Andrej Bauer's user avatar
  • 9,573
7 votes
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 ...
Couchy's user avatar
  • 2,271
7 votes
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 ...
Kevin Buzzard's user avatar
7 votes

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 ...
Eric's user avatar
  • 971
7 votes

What's "predicative" about pC(u)IC?

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ɪᴄ ...
ionchy's user avatar
  • 1,026
6 votes

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 (...
Ilk's user avatar
  • 547
5 votes
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 ...
Li-yao Xia's user avatar
  • 1,857
4 votes
Accepted

What is a 'truncation'?

Yes, truncations are a form of modalities, as explained in Section 7.7 of the HoTT book.
Andrej Bauer's user avatar
  • 9,573
4 votes
Accepted

What's "predicative" about pC(u)IC?

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…...
Meven Lennon-Bertrand's user avatar
3 votes
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 ...
Couchy's user avatar
  • 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 : ...
Meven Lennon-Bertrand's user avatar
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 ...
Jason Rute's user avatar
  • 8,905

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