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

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 logical objects:

```
data _≡_ {A : Set}(x : A) : A → Set where
refl : x ≡ x
_≢_ : {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 \]

TODO: write the type version as well.

The laws of equality are same as what we saw earlier in equality:

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

, `⊤`

or `Bool`

.

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

to prove an equivalence relation:

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

To see that this applies to a `singleton`

:

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

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, though symmetry can: