Questions tagged [equality]

Questions pertaining to equality in type theory (all kinds of equality are included: judgemental, propositional, observational, setoid equality, etc.) and equality reasoning in proof assistants.

Filter by
Sorted by
Tagged with
9 votes
2 answers
367 views

Defining coercion for proof irrelevant equality

Say I would like to define coercion for proof irrelevant equality between types. In Coq I try ...
user avatar
  • 1,662
11 votes
2 answers
325 views

Proving uniqueness of an instance of an indexed inductive type

Consider the simple indexed inductive type Inductive Single : nat -> Set := | single_O : Single O | single_S {n} : Single n -> Single (S n). Intuitively, I ...
user avatar
  • 213
11 votes
0 answers
129 views

What are the practical differences between intensional and extensional type theories?

It is already proved that MLTT with equality reflection is equivalent to MLTT with an intensional equality, plus UIP and function extensionality. So theoretically the differences between intensional ...
user avatar
  • 2,246
2 votes
2 answers
124 views

How do I make use of an irrelevant equality in a proof?

open import Agda.Primitive import Relation.Binary.PropositionalEquality as Eq open Eq public open Eq.≡-Reasoning Suppose I have a dependent pair whose second ...
user avatar
8 votes
1 answer
139 views

How does Metamath Zero handle CIC as in Lean or Coq?

Metamath Zero (MM0) is a proof assistant developed by Mario Carneiro. It has a metalogic very similar to the metalogic of MetaMath, but it also borrows design choices from Lean (and maybe other ...
user avatar
  • 3,355
13 votes
2 answers
166 views

What are the upsides and downsides of typed vs untyped conversion?

What are the tradeoffs between untyped and type-directed conversion in dependent type theory, and is there any consensus on what's "better"? Background Generally speaking, in dependent type ...
user avatar
8 votes
1 answer
161 views

Is there an elegant way of proving an equality A=B by going in both directions?

I would like to prove an equality by splitting it into a proof in each direction. Is there a more elegant style to start such a proof than this way:: ...
user avatar
14 votes
2 answers
172 views

What is the difference between refl and rfl in Lean 3?

I already know that refl is called a tactic, and that rfl is a term; can you explain with examples how they technically differ? ...
user avatar