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

1 vote
1 answer
105 views

Does Agda's --injective-type-constructors flag have canonicity?

3 votes
1 answer
65 views

Can I specify `refl`'s parameter explicitly in Agda?

5 votes
1 answer
111 views

Application of `SSet` in Agda

6 votes
1 answer
139 views

Strictly-monotone "max" operation for constructive Brouwer-trees?

4 votes
1 answer
80 views

Using induction to define Indexed family of HITs in agda

3 votes
1 answer
85 views

Agda Error after reload when successfully filling a goal

5 votes
2 answers
118 views

Agda: Cannot Instantiate Metavariable

9 votes
2 answers
206 views

How to access local definitions in Agda

4 votes
2 answers
148 views

Turning off some sProp checks

8 votes
2 answers
436 views

Curly Braces and Lambdas in Agda

9 votes
2 answers
387 views

Defining coercion for proof irrelevant equality

6 votes
1 answer
183 views

Proof of symmetry of universe-polymorphic Leibniz equality in Agda

9 votes
2 answers
213 views

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

5 votes
1 answer
251 views

What subtyping rules does Agda support?

Browse more Questions