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
132 views

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
157 views

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
387 views

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
341 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 ...
  • 213
10 votes
0 answers
137 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 ...
  • 2,916
3 votes
2 answers
132 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 ...
  • 151
8 votes
1 answer
163 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 ...
  • 4,690
13 votes
2 answers
204 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 ...
8 votes
1 answer
164 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:: ...
16 votes
2 answers
208 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? ...