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

32 Answers

Score Activity Newest
14 votes
Accepted

In Agda, why is universe polymorphism explicit?

13 votes
Accepted

What is the difference between judgmental equality, definitional equality, and equality types?

11 votes

Are there any proof assistants which integrate JITs?

10 votes

What are the differences between MLTT and CIC?

9 votes

Is there a way to automatically translate proofs from one proof assistant to another?

9 votes

Why is cumulativity not a given in proof assistants?

7 votes
Accepted

Does Agda have breaking changes?

7 votes
Accepted

Case splitting with quotient types in Cubical Agda

6 votes

What is bidirectional type checking?

6 votes
Accepted

Why can termination checker affect strict Prop in Agda?

6 votes

What about dependent types is useful for theorem provers?

5 votes

What are some examples of proof assistants doing something useful?

5 votes

What's the difference between a universe level and a natural number?

5 votes
Accepted

When installing Agda does one have to be attentive to a version?

5 votes
Accepted

How could I make a Proof Assistant?

5 votes
Accepted

Interpretation of dependent types: Coherence

4 votes

What are the motivations for different variants of categorical models of dependent type?

4 votes
Accepted

Simple Proof about `String.split`

4 votes

What is a non-canonical term?

4 votes

Can I use if_then_else on indexed paths in HITs?

3 votes
Accepted

How much duplication does universe polymorphism actually save us?

3 votes

Non-trivial examples of dependent sum ($\Sigma$-types) in Lean?

3 votes

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

3 votes

How to represent mathematical partial functions in a type-theory based proof assistant?

3 votes
Accepted

What are the differences and similarities between records, coinductive records, and codatatypes?

3 votes
Accepted

How do I approach the final step in proving the cancellation law in Coq?

2 votes

When should I use `no-eta-equality` in Agda records?

1 vote

Destruction of unification problem on application

1 vote

How does Prop relate to h-prop and double negation?

1 vote

Agda: Cannot Instantiate Metavariable

1
2

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.