```
module Logic.equality where
open import Logic.logicBasics using (¬; not; xor; ⟂; ⊤; singleton)
open import Lang.dataStructures using (Bool; true; false)
```

We start with the definition of a binary relation:

```
: Set → Set1
Rel = A → A → Set Rel A
```

Equality, or an equivalence, is the most basic comparison that can be performed between two objects. Let us first see how equality (and inequality) looks like for logic:

```
data _≡_ {A : Set}(x : A) : A → Set where
: x ≡ x
refl
_≢_ : {A : Set} → A → A → Set
= ¬ (x ≡ y) x ≢ y
```

Equality can also be derived as a negation of XOR:

\[ a \equiv b ~is~ ~True~ \implies ¬ (a \bigoplus b) ~is~ True \]

```
: Bool → Bool → Bool
equal? = not (xor a b) equal? a b
```

The laws of equality are same as what we saw earlier in equality. However, we derive the the same laws without universe polymorphism:

Relations can conform to certain properties, which later come in handy for classifying relations and building a lot of mathematical structure.

A reflexive relation is one where \[ x ∙ y = y ∙ x \]

```
: {A : Set}
reflexive → Rel A
→ Set
{A} _★_ = (x : A) → x ★ x reflexive
```

A symmetric relation is one where \[ x ∙ y ⟹ y ∙ x \]

```
: {A : Set} → Rel A → Set
symmetric {A} _★_ = (x y : A)
symmetric → x ★ y
→ y ★ x
```

A transitive relation is one where \[ x ∙ y, y ∙ z ~then~ z ∙ x \]

```
: {A : Set} → Rel A → Set
transitive {A} _★_ = (x y z : A)
transitive → x ★ y
→ y ★ z
→ x ★ z
```

A congruent relation is one where a function \[ x ∙ y ⟹ f(x) ∙ f(y) \] or the
function `f`

preserves the relation.

```
: {A : Set} → Rel A → Set
congruent {A} _★_ = (f : A → A)(x y : A)
congruent → x ★ y
→ f x ★ f y
```

A substitutive relation is one where \[ x ∙ y ~and~ (predicate~ y) = ⊤ ⟹ (predicate~ x) = ⊤ \]

```
substitutive : {A : Set} → Rel A → Set1
substitutive {A} _★_ = (P : A → Set)(x y : A)
→ x ★ y
→ P x
→ P y
```

```
record Equivalence (A : Set) : Set1 where
field
_==_ : Rel A
: reflexive _==_
rfl : symmetric _==_
sym : transitive _==_ trans
```

Note, the only difference here is that each law applies to the same datatype, be it `⟂`

, `⊤`

or
`Bool`

.

```
: {A : Set} {x y : A}
symm → x ≡ y
→ y ≡ x
{A} refl = refl symm
```

```
: {A : Set} {x y z : A}
trans → x ≡ y
→ y ≡ z
→ x ≡ z
{A} refl a = a trans
```

Let us fit the above proofs of the properties of the relation `≡`

to prove an equivalence relation:

```
: {A : Set} → Equivalence A
Equiv = record
Equiv {
_==_ = _≡_
; rfl = \x → refl
; sym = \x y → symm
; trans = \x y z → trans
}
```

To see that this applies to a `singleton`

:

```
: singleton ≡ singleton
refl⊤ = Equivalence.rfl Equiv singleton
refl⊤
: singleton ≡ singleton → singleton ≡ singleton
sym⊤ = Equivalence.sym Equiv singleton singleton
sym⊤
: singleton ≡ singleton → singleton ≡ singleton → singleton ≡ singleton
trans⊤ = Equivalence.trans Equiv singleton singleton singleton trans⊤
```

We cannot, however, verify this for `⟂`

explicitly as we cannot produce an object that does not exist /
does not have a constructor.

Inequality `≢`

cannot serve as an equivalence relation as reflexivity and transitivity cannot be
satisfied.