Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.

Sign up to join this community
Anybody can ask a question
Anybody can answer
The best answers are voted up and rise to the top

Explore our Questions

4 votes
2 answers
133 views

Turning off some sProp checks

8 votes
2 answers
410 views

Curly Braces and Lambdas in Agda

9 votes
2 answers
367 views

Defining coercion for proof irrelevant equality

6 votes
1 answer
166 views

Proof of symmetry of universe-polymorphic Leibniz equality in Agda

9 votes
2 answers
185 views

What's the benefit of having pi and sigma types with an invariant parameter?

5 votes
1 answer
224 views

What subtyping rules does Agda support?

4 votes
1 answer
90 views

Literate Agda: How do I change the size of the displayed code?

8 votes
1 answer
165 views

Case splitting with quotient types in Cubical Agda

9 votes
3 answers
766 views

Constructive proof of strong normalization for simply typed lambda calculus

7 votes
1 answer
131 views

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

13 votes
2 answers
219 views

In Agda, why is universe polymorphism explicit?

6 votes
1 answer
170 views

Parameterized Datatypes in a Universe à la Tarski?

7 votes
1 answer
87 views

Decidability for an infinite sequence of decidable propositions

6 votes
2 answers
207 views

How to run Agda?

Browse more Questions