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
0 votes
1 answer

Equational reasoning in Coq

I've been doing some exercises on Coq, and have stuck for the next problem: Let T: Set with 2 operations f, ...
4 votes
2 answers

Why do coinductive types require bisimilarity relations?

I was messing around with induction stuff again and some stuff seems to require bisimilarity relations instead of just equality when dualizing for coinductive types. ...
9 votes
2 answers

Defining coercion for proof irrelevant equality

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

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 ...
  • 213
10 votes
0 answers

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 ...
  • 2,916
3 votes
2 answers

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 ...
  • 151
8 votes
1 answer

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 ...
  • 4,690
13 votes
2 answers

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 ...
8 votes
1 answer

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:: ...
16 votes
2 answers

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? ...