Skip to main content
13 votes

In what intensional type theories can absurdity be made definitionally proof irrelevant?

If you are happy to have your False live in a separate sort, then you can do this with strict propositions in Coq (and any other system that have those, which I ...
Meven Lennon-Bertrand's user avatar
9 votes
Accepted

Strong eta-rules for functions on sum types

If we have $\eta$ for functions and also your pointwise conversion rule, that implies the full $\eta$ rule for the (finite) domain type. When checking conversion of arbitrary $t,u$, we can abstract ...
András Kovács's user avatar
8 votes

In what intensional type theories can absurdity be made definitionally proof irrelevant?

I think the paper you're looking for is Definitional Proof Irrelevance Without K (I seem to remember that there was some sort of snag in Agda, but I can't for the life of me remember what it was.) ...
Joey Eremondi's user avatar
5 votes
Accepted

What is the well-established η law for naturals?

I find it's best to think of $\eta$ laws for inductive types in terms of their categorical semantics as initial algebras. Recall that initiality for $(\mathbb{N},0,\mathsf{succ})$, regarded as an ...
C.B. Aberlé's user avatar
3 votes

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

When you're absolutely sure you don't need it. Then disabling eta equality for a record saves time for Agda. For instance, the Iso type for isomorphism is mostly used to carry the information of an ...
ice1000's user avatar
  • 6,276
1 vote
Accepted

Eta-equality for records: the case of semigroups

One approach is to do things the other way around: define SG with all the fields, without any one of them being defined. Then define an interface that will ...
Meven Lennon-Bertrand's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible