---
layout: default
title : "Legacy.Base.Equality module (The Agda Universal Algebra Library)"
date : "2021-07-26"
author: "agda-algebras development team"
---

## <a id="equality">Equality</a>

This is the [Legacy.Base.Equality][] module of the [Agda Universal Algebra Library][].



```agda

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Legacy.Base.Equality where

open import Legacy.Base.Equality.Welldefined     public
open import Legacy.Base.Equality.Truncation      public
open import Legacy.Base.Equality.Extensionality  public
```