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

## <a id="types-for-general-mathematical-structures">Types for General Mathematical Structures</a>

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


```agda


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

module Legacy.Base.Structures where

open import Legacy.Base.Structures.Basic            public
open import Legacy.Base.Structures.Products         public
open import Legacy.Base.Structures.Congruences      public
open import Legacy.Base.Structures.Homs             public
open import Legacy.Base.Structures.Graphs           public
open import Legacy.Base.Structures.Isos             public
open import Legacy.Base.Structures.Terms            public
open import Legacy.Base.Structures.Substructures    public
open import Legacy.Base.Structures.EquationalLogic  public
open import Legacy.Base.Structures.Sigma
```