Skip to main content
Proof Assistants Beta
Trebor's user avatar
Trebor's user avatar
Trebor's user avatar
Trebor
Moderator
  • Member for 2 years, 10 months
  • Last seen this week
Profile Activity

38 Answers

Score Activity Newest
18 votes
Accepted

What difficulties are there in basing a proof assistant on the $\lambda\mu$-calculus and has any proof assistant tried?

10 votes

What's the "Hello, World!" for proof assistants?

10 votes

What is predicativity?

10 votes
Accepted

What is a universe?

10 votes

What is Artin gluing, and how is it useful in proving meta-theoretic properties?

10 votes

What are "fibration/cofibration" in type theory and what are their intuitions?

9 votes

What are good examples of April fools jokes in the proving assistant community?

7 votes
Accepted

How to deal with Binders?

7 votes
Accepted

Canonical forms of combinators

6 votes

In a dependently typed language, are all types statements?

6 votes
Accepted

Why are dependent sums and products called sums and products?

5 votes

How to prove the termination of Ackermann in Lean?

5 votes
Accepted

In HoTT, what is the hlevel of $S^1$?

5 votes
Accepted

Defining coercion for proof irrelevant equality

4 votes

Turning off some sProp checks

4 votes

What is the intuition behind the `Glue` type in Cubical Type Theories

4 votes
Accepted

Can a chain of implications be solved using calc in Lean 4?

3 votes

How do we know that we can trust proof assistance to produce correct results?

3 votes
Accepted

easy infix in Lean

3 votes
Accepted

Naive computation of propositional resizing

3 votes
Accepted

What are instances of a dependent pair type?

3 votes

Using induction to define Indexed family of HITs in agda

3 votes

How are the parts of category theory which make explicit reference to Set different when formalized in a proof assistant that is based on type theory

3 votes
Accepted

How do clausal definitions work?

3 votes
Accepted

Problem proving a binary add function

3 votes
Accepted

Can a metamath identifier be reused across scopes?

2 votes
Accepted

Why is the normal form of an ind-Nat expression with a function type an elimination-of-a-function expression

2 votes
Accepted

Agda: Cannot Instantiate Metavariable

2 votes

State-of-the-art constructive encodings of Reals in a (constructive) type theory that supports quotient-types

2 votes

Are there minimal typed proof verifiers that can deal with the majority of mathematics?

1
2