Proof Assistants Beta
Andrej Bauer's user avatar
Andrej Bauer's user avatar
Andrej Bauer's user avatar
Andrej Bauer
  • Member for 1 year, 9 months
  • Last seen this week
Profile Activity

101 Answers

Score Activity Newest
9 votes
Accepted

Strong induction on ℕ with function α → ℕ

9 votes
Accepted

Attempts to accommodate theories of different consistency strength in single assistant

8 votes
Accepted

Are eliminators useful in practice, or are they only useful in the metatheory?

8 votes

What are the possible kinds of type theories or logics with quotients?

8 votes
Accepted

In the "Simply Easy!" paper, why is it safe to evaluate types in the empty environment?

8 votes

Formal description of algorithmic subtyping/cumulativity

8 votes
Accepted

Defining essentially unique objects with typeclasses

8 votes

When is hProp equivalent to the subobject classifier?

8 votes

Does one need a type-theoretical axiom of choice for singletons?

8 votes
Accepted

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

7 votes
Accepted

Can I prove this axiom without using excluded-middle property?

7 votes

Can a theorem prover reason about its own faulty hardware?

7 votes
Accepted

verifying combinatorial constructions - choice of a proof assistant

7 votes
Accepted

Is coercion to a higher universe injective?

6 votes

Universe inconsistency errors when using ZF model in Coq

6 votes

Why does it matter if canonicity holds for irrelevant types?

6 votes
Accepted

Partial and multi-valued choice principles/description operators

6 votes
Accepted

How can you represent a dependent type visually?

6 votes

Universe inconsistency as an effect

6 votes

How to prove that addition is commutative for conatural numbers in Coq

5 votes

I'm stuck trying to prove ∀x : ℕ, 3 | (x + 5x) with Coq

5 votes
Accepted

Unclarity about Preorder class in Lean4

5 votes

Algorithm for the locally nameless representation used by Lean

5 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

5 votes

Converting between formulations of reals in Coq

5 votes

Is there computational interpretation for countable choice?

5 votes
Accepted

Understanding the complete lattice definition of impredicativity

5 votes
Accepted

How to implement first-order relational structures in Coq?

5 votes

Notation for indefinite integrals

5 votes
Accepted

Coq: Would adding "inline inductive definition expressions" introduce inconsistency?

Your privacy

By clicking “Accept all cookies”, you agree Stack Exchange can store cookies on your device and disclose information in accordance with our Cookie Policy.