michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fiddling with Equality

Browse source
This commit is contained in:
wadler 2018-03-11 18:52:48 -03:00
parent b191d639c8
commit c90f0f9af0
6 changed files with 541 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
index.md
View file

@ -23,7 +23,7 @@ material in a different way; see the [Preface](Preface).
- [Naturals: Natural numbers](Naturals)
- [Properties: Proof by induction](Properties)
- [Relations: Inductive Definition of Relations](Relations)
- [Equivalence: Equivalence and equational reasoning](Equivalence)
- [Equality: Equality and equational reasoning](Equality)
- [Isomorphism: Isomorphism and embedding](Isomorphism)
- [Logic: Logic](Logic)
- [Lists: Lists and other data types](Lists)

481
src/Equality.lagda Normal file
View file

@ -0,0 +1,481 @@
---
title : "Equality: Equality and equational reasoning"
layout : page
permalink : /Equality
---
<!-- TODO: Consider changing `Equivalence` to `Equality` or `Identity`.
Possibly introduce the name `Martin Löf Identity` early on. -->
Much of our reasoning has involved equality. Given two terms `M`
and `N`, both of type `A`, we write `M ≡ N` to assert that `M` and `N`
are interchangeable. So far we have taken equivalence as a primitive,
but in fact it can be defined using the machinery of inductive
datatypes.
## Imports
Nearly every module in the Agda
standard library, and every chapter in this book, imports equality.
Since we define equality here, any such
import would create a conflict. The only import we make is the
definition of type levels, which is so primitive that it precedes
the definition of equality.
\begin{code}
open import Agda.Primitive using (Level; lzero; lsuc)
\end{code}
## Equivalence
We declare equivality as follows.
\begin{code}
data _≡_ {ℓ} {A : Set ℓ} (x : A) : A → Set ℓ where
refl : x ≡ x
\end{code}
In other words, for any type `A` and for any `x` of type `A`, the
constructor `refl` provides evidence that `x ≡ x`. Hence, every value
is equivalent to itself, and we have no other way of showing values
are equivalent. We have quantified over all levels, so that we can
apply equivalence to types belonging to any level. The definition
features an asymetry, in that the first argument to `_≡_` is given by
the parameter `x : A`, while the second is given by an index in `A → Set ℓ`.
This follows our policy of using parameters wherever possible.
The first argument to `_≡_` can be a parameter because it doesn't vary,
while the second must be an index.
We declare the precedence of equivalence as follows.
\begin{code}
infix 4 _≡_
\end{code}
We set the precedence of `_≡_` at level 4, the same as `_≤_`,
which means it binds less tightly than any arithmetic operator.
It associates neither to the left nor right; writing `x ≡ y ≡ z`
is illegal.
## Equality is an equivalence relation
An equivalence relation is one which is reflexive, symmetric, and transitive.
Reflexivity is built-in to the definition of equivalence, via the
constructor `refl`. It is straightforward to show symmetry.
\begin{code}
sym : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≡ y → y ≡ x
sym refl = refl
\end{code}
How does this proof work? The argument to `sym` has type `x ≡ y`,
but on the left-hand side of the equation the argument has been instantiated to the pattern `refl`,
which requires that `x` and `y` are the same. Hence, for the right-hand side of the equation
we need a term of type `x ≡ x`, and `refl` will do.
It is instructive to develop `sym` interactively.
To start, we supply a variable for the argument on the left, and a hole for the body on the right:
sym : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≡ y → y ≡ x
sym e = {! !}
If we go into the hole and type `C-C C-,` then Agda reports:
Goal: .y ≡ .x
————————————————————————————————————————————————————————————
e : .x ≡ .y
.y : .A
.x : .A
.A : Set .ℓ
.ℓ : .Agda.Primitive.Level
If in the hole we type `C-C C-C e` then Agda will instantiate `e` to all possible constructors,
with one equation for each. There is only one possible constructor:
sym : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≡ y → y ≡ x
sym refl = {! !}
If we go into the hole again and type `C-C C-,` then Agda now reports:
Goal: .x ≡ .x
————————————————————————————————————————————————————————————
.x : .A
.A : Set .ℓ
.ℓ : .Agda.Primitive.Level
This is the key step---Agda has worked out that `x` and `y` must be the same to match the pattern `refl`!
Finally, if we go back into the hole and type `C-C C-R` it will
instantiate the hole with the one constructor that yields a value of
the expected type.
sym : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≡ y → y ≡ x
sym refl = refl
This completes the definition as given above.
Transitivity is equally straightforward.
\begin{code}
trans : ∀ {ℓ} {A : Set ℓ} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl
\end{code}
Again, a useful exercise is to carry out an interactive development, checking
how Agda's knowledge changes as each of the two arguments is
instantiated.
## Congruence and Substitution
Equality also satisfies *congruence*. If two terms are equal,
they remain so after the same function is applied to both.
\begin{code}
cong : ∀ {ℓ} {A B : Set ℓ} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
cong f refl = refl
\end{code}
Once more, a useful exercise is to carry out an interactive development.
If two values are equal and a predicate holds of the first then it also holds of the second.
\begin{code}
subst : ∀ {A : Set} {x y : A} (P : A → Set) → x ≡ y → P x → P y
subst P refl px = px
\end{code}
## Tabular reasoning
Here we show how to support the form of tabular reasoning
we have used throughout the book. We package the declarations
into a module, named `≡-Reasoning`, to match the format used in Agda's
standard library.
\begin{code}
module ≡-Reasoning {ℓ} {A : Set ℓ} where
infix 1 begin_
infixr 2 _≡⟨⟩_ _≡⟨_⟩_
infix 3 _∎
begin_ : ∀ {x y : A} → x ≡ y → x ≡ y
begin x≡y = x≡y
_≡⟨⟩_ : ∀ (x {y} : A) → x ≡ y → x ≡ y
x ≡⟨⟩ x≡y = x≡y
_≡⟨_⟩_ : ∀ (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
x ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z
_∎ : ∀ (x : A) → x ≡ x
x ∎ = refl
open ≡-Reasoning
\end{code}
Opening the module makes all of the definitions
available in the current environment.
As a simple example, let's look at the proof of transitivity
rewritten in tabular form.
\begin{code}
trans′ : ∀ {ℓ} {A : Set ℓ} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans′ {ℓ} {A} {x} {y} {z} x≡y y≡z =
begin
x
≡⟨ x≡y ⟩
y
≡⟨ y≡z ⟩
z
∎
\end{code}
According to the fixity declarations, the body parses as follows.
begin (x ≡⟨ x≡y ⟩ (y ≡⟨ y≡z ⟩ (z ∎)))
The application of `begin` is purely cosmetic, as it simply returns
its argument. That argument consists of `_≡⟨_⟩_` applied to `x`,
`x≡y`, and `y ≡⟨ y≡z ⟩ (z ∎)`. The first argument is a term, `x`,
while the second and third arguments are both proofs of equations, in
particular proofs of `x ≡ y` and `y ≡ z` respectively, which are
combined by `trans` in the body of `_≡⟨_⟩_` to yield a proof of `x ≡
z`. The proof of `y ≡ z` consists of `_≡⟨_⟩_` applied to `y`, `y≡z`,
and `z ∎`. The first argument is a term, `y`, while the second and
third arguments are both proofs of equations, in particular proofs of
`y ≡ z` and `z ≡ z` respectively, which are combined by `trans` in the
body of `_≡⟨_⟩_` to yield a proof of `y ≡ z`. Finally, the proof of
`z ≡ z` consists of `_∎` applied to the term `z`, which yields `refl`.
After simplification, the body is equivalent to the following term.
trans x≡y (trans y≡z refl)
We could replace all uses of tabular reasoning by a chain of
applications of `trans`; the result would be more compact but harder to read.
Also note that the syntactic trick behind `∎` means that the chain
always ends in the form `trans e refl`, where `e` proves some equation,
even though `e` alone would do.
<!--
## Tabular reasoning, another example
As a second example of tabular reasoning, we consider the proof that addition
is commutative. We first repeat the definitions of naturals and addition.
We cannot import them because (as noted at the beginning of this chapter)
it would cause a conflict.
\begin{code}
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)
\end{code}
To save space we postulate (rather than prove in full) two lemmas,
and then repeat the proof of commutativity.
\begin{code}
postulate
+-identity : ∀ (m : ℕ) → m + zero ≡ m
+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
{-
+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
begin
m + zero
≡⟨ +-identity m ⟩
m
≡⟨⟩
zero + m
∎
+-comm m (suc n) =
begin
m + suc n
≡⟨ +-suc m n ⟩
suc (m + n)
≡⟨ cong suc (+-comm m n) ⟩
suc (n + m)
≡⟨⟩
suc n + m
∎
-}
\end{code}
The tabular reasoning here is similar to that in the
preceding section, the one addition being the use of
`_≡⟨⟩_`, which we use when no justification is required.
One can think of occurrences of `≡⟨⟩` as an equivalent
to `≡⟨ refl ⟩`.
Agda always treats a term as equivalent to its
simplified term. The reason that one can write
suc (n + m)
≡⟨⟩
suc n + m
is because Agda treats both terms as the same.
This also means that one could instead interchange
the lines and write
suc n + m
≡⟨⟩
suc (n + m)
and Agda would not object. Agda only checks that the terms
separated by `≡⟨⟩` are equivalent; it's up to us to write
them in an order that will make sense to the reader.
-->
## Rewriting
Consider a property of natural numbers, such as being even.
\begin{code}
data even : ℕ → Set where
ev0 : even zero
ev+2 : ∀ {n : ℕ} → even n → even (suc (suc n))
\end{code}
In the previous section, we proved addition is commutative.
Given evidence that `even (m + n)` holds,
we ought also to be able to take that as evidence
that `even (n + m)` holds.
Agda includes special notation to support just this
kind of reasoning. To enable this notation, we use
pragmas to tell Agda which type
corresponds to equivalence.
\begin{code}
{-# BUILTIN EQUALITY _≡_ #-}
\end{code}
We can then prove the desired property as follows.
\begin{code}
postulate
+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
even-comm : ∀ (m n : ℕ) → even (m + n) → even (n + m)
even-comm m n ev rewrite +-comm m n = ev
\end{code}
Here `ev` ranges over evidence that `even (m + n)` holds, and we show
that it is also provides evidence that `even (n + m)` holds. In
general, the keyword `rewrite` is followed by evidence of an
equivalence, and that equivalence is used to rewrite the type of the
goal and of any variable in scope.
It is instructive to develop `even-comm` interactively.
To start, we supply variables for the arguments on the left, and a hole for the body on the right:
even-comm : ∀ (m n : ℕ) → even (m + n) → even (n + m)
even-comm m n ev = {! !}
If we go into the hole and type `C-C C-,` then Agda reports:
Goal: even (n + m)
————————————————————————————————————————————————————————————
ev : even (m + n)
n : ℕ
m : ℕ
Now we add the rewrite.
even-comm : ∀ (m n : ℕ) → even (m + n) → even (n + m)
even-comm m n ev rewrite +-comm m n = {! !}
If we go into the hole again and type `C-C C-,` then Agda now reports:
Goal: even (n + m)
————————————————————————————————————————————————————————————
ev : even (n + m)
n : ℕ
m : ℕ
Now it is trivial to see that `ev` satisfies the goal, and typing `C-C C-A` in the
hole causes it to be filled with `ev`.
## Multiple rewrites
One may perform multiple rewrites, each separated by a vertical bar. For instance,
here is a second proof that addition is commutative, relying on rewrites rather
than tabular reasoning.
\begin{code}
+-comm′ : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm′ zero n rewrite +-identity n = refl
+-comm′ (suc m) n rewrite +-suc n m | +-comm m n = refl
\end{code}
This is far more compact. Among other things, whereas the previous
proof required `cong suc (+-comm m n)` as the justification to invoke the
inductive hypothesis, here it is sufficient to rewrite with `+-comm m n`, as
rewriting automatically takes congruence into account. Although proofs
with rewriting are shorter, proofs in tabular form make the reasoning
involved easier to follow, and we will stick with the latter when feasible.
## Rewriting expanded
The `rewrite` notation is in fact shorthand for an appropriate use of `with`
abstraction.
\begin{code}
even-comm′ : ∀ (m n : ℕ) → even (m + n) → even (n + m)
even-comm′ m n ev with m + n | +-comm m n
... | .(n + m) | refl = ev
\end{code}
The first clause asserts that `m + n` and `n + m` are identical, and
the second clause justifies that assertion with evidence of the
appropriate equivalence. Note the use of the "dot pattern" `.(n +
m)`. A dot pattern is followed by an expression and is made when
other information allows one to identify the expession in the `with`
clause with the expression it matches against. In this case, the
identification of `m + n` and `n + m` is justified by the subsequent
matching of `+-comm m n` against `refl`. One might think that the
first clause is redundant as the information is inherent in the second
clause, but in fact Agda is rather picky on this point: omitting the
first clause or reversing the order of the clauses will cause Agda to
report an error. (Try it and see!)
## Leibniz equality
The form of asserting equivalence that we have used is due to Martin Löf,
and was published in 1975. An older form is due to Leibniz, and was published
in 1686. Leibniz asserted the *identity of indiscernibles*: two objects are
equal if and only if they satisfy the same properties. This
principle sometimes goes by the name Leibniz' Law, and is closely
related to Spock's Law, ``A difference that makes no difference is no
difference''. Here we define Leibniz equality, and show that two terms
satsisfy Lebiniz equality if and only if they satisfy Martin Löf equivalence.
Leibniz equality is usually formalized to state that `x ≐ y`
holds if every property `P` that holds of `x` also holds of
`y`. Perhaps surprisingly, this definition is
sufficient to also ensure the converse, that every property `P` that
holds of `y` also holds of `x`.
Let `x` and `y` be objects of type $A$. We say that `x ≐ y` holds if
for every predicate $P$ over type $A$ we have that `P x` implies `P y`.
\begin{code}
_≐_ : ∀ {ℓ} {A : Set ℓ} (x y : A) → Set (lsuc ℓ)
_≐_ {ℓ} {A} x y = (P : A → Set ℓ) → P x → P y
\end{code}
Here we must make use of levels: if `A` is a set at level `ℓ` and `x` and `y`
are two values of type `A` then `x ≐ y` is at the next level `lsuc ℓ`.
Leibniz equality is reflexive and transitive,
where the first follows by a variant of the identity function
and the second by a variant of function composition.
\begin{code}
refl-≐ : ∀ {ℓ} {A : Set ℓ} {x : A} → x ≐ x
refl-≐ P Px = Px
trans-≐ : ∀ {ℓ} {A : Set ℓ} {x y z : A} → x ≐ y → y ≐ z → x ≐ z
trans-≐ x≐y y≐z P Px = y≐z P (x≐y P Px)
\end{code}
Symmetry is less obvious. We have to show that if `P x` implies `P y`
for all predicates `P`, then the implication holds the other way round
as well. Given a specific `P` and a proof `Py` of `P y`, we have to
construct a proof of `P x` given `x ≐ y`. To do so, we instantiate
the equality with a predicate `Q` such that `Q z` holds if `P z`
implies `P x`. The property `Q x` is trivial by reflexivity, and
hence `Q y` follows from `x ≐ y`. But `Q y` is exactly a proof of
what we require, that `P y` implies `P x`.
\begin{code}
sym-≐ : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≐ y → y ≐ x
sym-≐ {ℓ} {A} {x} {y} x≐y P = Qy
where
Q : A → Set ℓ
Q z = P z → P x
Qx : Q x
Qx = refl-≐ P
Qy : Q y
Qy = x≐y Q Qx
\end{code}
We now show that Martin Löf equivalence implies
Leibniz equality, and vice versa. In the forward direction, if we know
`x ≡ y` we need for any `P` to take evidence of `P x` to evidence of `P y`,
which is easy since equivalence of `x` and `y` implies that any proof
of `P x` is also a proof of `P y`.
\begin{code}
≡-implies-≐ : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≡ y → x ≐ y
≡-implies-≐ refl P Px = Px
\end{code}
The function `≡-implies-≐` is often called *substitution* because it
says that if we know `x ≡ y` then we can substitute `y` for `x`,
taking a proof of `P x` to a proof of `P y` for any property `P`.
In the reverse direction, given that for any `P` we can take a proof of `P x`
to a proof of `P y` we need to show `x ≡ y`. The proof is similar to that
for symmetry of Leibniz equality. We take $Q$
to be the predicate that holds of `z` if `x ≡ z`. Then `Q x` is trivial
by reflexivity of Martin Löf equivalence, and hence `Q y` follows from
`x ≐ y`. But `Q y` is exactly a proof of what we require, that `x ≡ y`.
\begin{code}
≐-implies-≡ : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≐ y → x ≡ y
≐-implies-≡ {ℓ} {A} {x} {y} x≐y = Qy
where
Q : A → Set ℓ
Q z = x ≡ z
Qx : Q x
Qx = refl
Qy : Q y
Qy = x≐y Q Qx
\end{code}
(Parts of this section are adapted from *≐≃≡: Leibniz Equality is
Isomorphic to Martin-Löf Identity, Parametrically*, by Andreas Abel,
Jesper Cockx, Dominique Devries, Andreas Nuyts, and Philip Wadler,
draft paper, 2017.)

22
src/Relations.lagda
View file

@ -414,6 +414,8 @@ variant that returns the flipped case.
... | forward m≤n = forward (s≤s m≤n)
... | flipped n≤m = flipped (s≤s n≤m)
\end{code}
It differs from the original code in that it pattern
matches on the second argument before the first argument.
## Monotonicity
@ -511,7 +513,7 @@ we will be in a position to show that the three cases are mutually exclusive.)
Show that addition is monotonic with respect to strict inequality.
As with inequality, some additional definitions may be required.
### Exercise (`≤→<`, `<→≤`)
### Exercise (`≤-implies-<`, `<-implies-≤`)
Show that `suc m ≤ n` implies `m < n`, and conversely.
@ -582,6 +584,24 @@ functions and then the equations that define them.
Show that the sum of two odd numbers is even.
## Formalising preorder
\begin{code}
record IsPreorder {A : Set} (_≤_ : A → A → Set) : Set where
field
reflexive : ∀ {x : A} → x ≤ x
trans : ∀ {x y z : A} → x ≤ y → y ≤ z → x ≤ z
IsPreorder-≤ : IsPreorder _≤_
IsPreorder-≤ =
record
{ reflexive = ≤-refl
; trans = ≤-trans
}
\end{code}
## Standard prelude
Definitions similar to those in this chapter can be found in the standard library.

17
src/RelationsAns.lagda
View file

@ -66,16 +66,16 @@ trichotomy (suc m) (suc n) with trichotomy m n
### Relate inequality to strict inequality
\begin{code}
≤→< : ∀ {m n : ℕ} → suc m ≤ n → m < n
≤→< (s≤s z≤n) = z<s
≤→< (s≤s (s≤s m≤n)) = s<s (≤→< (s≤s m≤n))
≤-implies-< : ∀ {m n : ℕ} → suc m ≤ n → m < n
≤-implies-< (s≤s z≤n) = z<s
≤-implies-< (s≤s (s≤s m≤n)) = s<s (≤-implies-< (s≤s m≤n))
<→≤ : ∀ {m n : ℕ} → m < n → suc m ≤ n
<→≤ z<s = s≤s z≤n
<→≤ (s<s m<n) = s≤s (<→≤ m<n)
<-implies-≤ : ∀ {m n : ℕ} → m < n → suc m ≤ n
<-implies-≤ z<s = s≤s z≤n
<-implies-≤ (s<s m<n) = s≤s (<-implies-≤ m<n)
<-trans′ : ∀ {m n p : ℕ} → m < n → n < p → m < p
<-trans′ m<n n<p = ≤→< (helper (<→≤ m<n) (<→≤ n<p))
<-trans′ m<n n<p = ≤-implies-< (helper (<-implies-≤ m<n) (<-implies-≤ n<p))
where
helper : ∀ {m n p : ℕ} → suc m ≤ n → suc n ≤ p → suc m ≤ p
helper sm≤n sn≤p = ≤-trans sm≤n (≤-trans n≤sn sn≤p)
@ -94,7 +94,10 @@ o+o≡e (odd-suc em) on = even-suc (e+o≡o em on)
e+o≡o even-zero on = on
e+o≡o (even-suc om) on = odd-suc (o+o≡e om on)
\end{code}
An alternative proof
\begin{code}
o+o≡e′ : ∀ {m n : ℕ} → odd m → odd n → even (m + n)
o+o≡e′ {suc m} {suc n} (odd-suc em) (odd-suc en)
rewrite +-suc m n = even-suc (odd-suc (e+e≡e em en))

23
src/Equivalence.lagda → src/extra/Equivalence-old.lagda
View file

@ -24,6 +24,7 @@ definition of type levels, which is so primitive that it precedes
the definition of equivalence.
\begin{code}
open import Agda.Primitive using (Level; lzero; lsuc)
open import Data.Nat using (ℕ; zero; suc; _+_)
\end{code}
@ -40,7 +41,7 @@ is equivalent to itself, and we have no other way of showing values
are equivalent. We have quantified over all levels, so that we can
apply equivalence to types belonging to any level. The definition
features an asymetry, in that the first argument to `_≡_` is given by
the parameter `x : A`, while the second is given by `A → Set ℓ`.
the parameter `x : A`, while the second is given by an index in `A → Set ℓ`.
We declare the precedence of equivalence as follows.
\begin{code}
@ -197,6 +198,7 @@ Also note that the syntactic trick behind `∎` means that the chain
always ends in the form `trans e refl` even though `e` alone would do,
where `e` is a proof of an equivalence.
<!--
## Tabular reasoning, another example
@ -205,6 +207,7 @@ is commutative. We first repeat the definitions of naturals and addition.
We cannot import them because (as noted at the beginning of this chapter)
it would cause a conflict.
\begin{code}
{-
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
@ -212,15 +215,17 @@ data ℕ : Set where
_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)
-}
\end{code}
We save space we postulate (rather than prove in full) two lemmas,
To save space we postulate (rather than prove in full) two lemmas,
and then repeat the proof of commutativity.
\begin{code}
postulate
+-identity : ∀ (m : ℕ) → m + zero ≡ m
+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
{-
+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
begin
@ -240,6 +245,7 @@ postulate
≡⟨⟩
suc n + m
∎
-}
\end{code}
The tabular reasoning here is similar to that in the
preceding section, the one addition being the use of
@ -265,10 +271,12 @@ the lines and write
and Agda would not object. Agda only checks that the terms
separated by `≡⟨⟩` are equivalent; it's up to us to write
them in an order that will make sense to the reader.
-->
## Rewriting
Consider a property of natural numbers, such as being even.
\begin{code}
data even : ℕ → Set where
ev0 : even zero
@ -289,6 +297,9 @@ corresponds to equivalence.
We can then prove the desired property as follows.
\begin{code}
postulate
+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
even-comm : ∀ (m n : ℕ) → even (m + n) → even (n + m)
even-comm m n ev rewrite +-comm m n = ev
\end{code}
@ -379,7 +390,7 @@ equal if and only if they satisfy the same properties. This
principle sometimes goes by the name Leibniz' Law, and is closely
related to Spock's Law, ``A difference that makes no difference is no
difference''. Here we define Leibniz equality, and show that two terms
satsisfy Lebiniz equality iff and only if they satisfy Martin Löf equivalence.
satsisfy Lebiniz equality if and only if they satisfy Martin Löf equivalence.
Leibniz equality is usually formalized to state that `x ≐ y`
holds if every property `P` that holds of `x` also holds of
@ -401,10 +412,10 @@ where the first follows by a variant of the identity function
and the second by a variant of function composition.
\begin{code}
refl-≐ : ∀ {ℓ} {A : Set ℓ} {x : A} → x ≐ x
refl-≐ P Px = Px
refl-≐ P Px = Px
trans-≐ : ∀ {ℓ} {A : Set ℓ} {x y z : A} → x ≐ y → y ≐ z → x ≐ z
trans-≐ x≐y y≐z P Px = y≐z P (x≐y P Px)
trans-≐ x≐y y≐z P Px = y≐z P (x≐y P Px)
\end{code}
Symmetry is less obvious. We have to show that if `P x` implies `P y`
@ -417,7 +428,7 @@ hence `Q y` follows from `x ≐ y`. But `Q y` is exactly a proof of
what we require, that `P y` implies `P x`.
\begin{code}
sym-≐ : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≐ y → y ≐ x
sym-≐ {ℓ} {A} {x} {y} x≐y P = Qy
sym-≐ {ℓ} {A} {x} {y} x≐y P = Qy
where
Q : A → Set ℓ
Q z = P z → P x

11
src/extra/Mendler.agda Normal file
View file

@ -0,0 +1,11 @@
module Mendler (F : Set → Set) where
open import Data.Product using (_×_)
Alg : Set → Set₁
Alg X = ∀ (R : Set) → (R → X) → F R → X
test : Set → Set
test A = A × A
test′ : ∀ (R : Set) → Set
test′ A = A × A