User ice1000

27 votes

1 answer

960 views

What is an algebraic data type?

asked Feb 27, 2022 at 21:58

20 votes

3 answers

417 views

Are implicit arguments essential to (dependently-typed) proof assistants?

asked Feb 8, 2022 at 18:16

18 votes

3 answers

278 views

Is internal parametricity useful in theorem proving?

asked Feb 9, 2022 at 12:19

18 votes

1 answer

185 views

What are the advantages of normalization by evaluation over traditional reduction-based normalization?

asked Feb 9, 2022 at 15:03

18 votes

2 answers

1k views

What's the difference between reflection and tactics?

asked Mar 19, 2022 at 20:29

16 votes

1 answer

1k views

How much of trouble is Lean's failure of normalization, given that logical consistency is not obviously broken?

asked Mar 27, 2022 at 20:07

14 votes

6 answers

1k views

Is there any example of a dependent product that makes sense in a non-type-theory context?

asked Mar 19, 2022 at 20:39

14 votes

1 answer

322 views

What happened to Conor McBride's universe polymorphism proposal?

asked Feb 9, 2022 at 1:46

14 votes

10 answers

577 views

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

asked Feb 15, 2022 at 20:15

12 votes

1 answer

179 views

What are "locales" in Isabelle?

asked Feb 8, 2022 at 18:22

11 votes

1 answer

323 views

Why did Agda give up cumulative universes?

asked Feb 10, 2022 at 1:05

10 votes

2 answers

161 views

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

asked Feb 12, 2022 at 3:11

10 votes

0 answers

309 views

What's "Swedish" style of doing type theory or proof assistants?

asked Mar 21, 2022 at 0:03

10 votes

1 answer

315 views

What are well-founded inductive types?

asked Mar 1, 2022 at 21:20

10 votes

1 answer

263 views

How to implement the type checking of `transp` in de Morgan cubical type theory?

asked Apr 12, 2022 at 13:22

9 votes

2 answers

248 views

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

asked Mar 25, 2022 at 19:02

9 votes

2 answers

255 views

What's the relationship between refinement types and dependent types?

asked Feb 21, 2022 at 4:51

9 votes

1 answer

182 views

How does the elimination rule of the heterogeneous equality type imply a weak version of K?

asked Feb 10, 2022 at 22:50

8 votes

1 answer

160 views

How to quickly look up what constructor/lemma I should use in Lean4?

asked Feb 21, 2022 at 21:26

8 votes

2 answers

234 views

What's “conservativity” in terms of type theory and how is it useful?

asked Feb 26, 2022 at 22:58

8 votes

1 answer

120 views

Is it possible to define `fib` coinductive stream w/o sized types?

asked Feb 12, 2022 at 22:17

8 votes

4 answers

201 views

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

asked Feb 20, 2022 at 19:25

7 votes

1 answer

104 views

How to state and prove the associativity of append of sized vectors with homogeneous equality?

asked Feb 10, 2022 at 1:00

7 votes

1 answer

119 views

How is "propositional canonicity" useful?

asked Mar 16, 2022 at 16:57

6 votes

1 answer

200 views

Proof of symmetry of universe-polymorphic Leibniz equality in Agda

asked Apr 2, 2022 at 13:23

6 votes

2 answers

199 views

Does ST$\lambda$C equal to simple type theory?

asked May 28, 2022 at 2:25

6 votes

1 answer

198 views

Can we completely erase propositions in the type checker?

asked Sep 16, 2022 at 16:36

6 votes

1 answer

170 views

Termination and confluence -- which goes first?

asked Dec 14, 2022 at 5:23

6 votes

0 answers

132 views

How does the modality-based irrelevance compare to universe-based irrelevance (`Prop`)?

asked Feb 1 at 22:56

5 votes

0 answers

107 views

Can we bring unification results under cofibrations outside?

asked Sep 17, 2022 at 2:15

Stack Exchange Network

50 Questions

What is an algebraic data type?

Are implicit arguments essential to (dependently-typed) proof assistants?

Is internal parametricity useful in theorem proving?

What are the advantages of normalization by evaluation over traditional reduction-based normalization?

What's the difference between reflection and tactics?

How much of trouble is Lean's failure of normalization, given that logical consistency is not obviously broken?

Is there any example of a dependent product that makes sense in a non-type-theory context?

What happened to Conor McBride's universe polymorphism proposal?

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

What are "locales" in Isabelle?

Why did Agda give up cumulative universes?

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

What's "Swedish" style of doing type theory or proof assistants?

What are well-founded inductive types?

How to implement the type checking of `transp` in de Morgan cubical type theory?

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

What's the relationship between refinement types and dependent types?

How does the elimination rule of the heterogeneous equality type imply a weak version of K?

How to quickly look up what constructor/lemma I should use in Lean4?

What's “conservativity” in terms of type theory and how is it useful?

Is it possible to define `fib` coinductive stream w/o sized types?

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

How to state and prove the associativity of append of sized vectors with homogeneous equality?

How is "propositional canonicity" useful?

Proof of symmetry of universe-polymorphic Leibniz equality in Agda

Does ST$\lambda$C equal to simple type theory?

Can we completely erase propositions in the type checker?

Termination and confluence -- which goes first?

How does the modality-based irrelevance compare to universe-based irrelevance (`Prop`)?

Can we bring unification results under cofibrations outside?