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

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

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


```agda


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

module Legacy.Base.Structures.Sigma where

open import Legacy.Base.Structures.Sigma.Basic        public
open import Legacy.Base.Structures.Sigma.Products     public
open import Legacy.Base.Structures.Sigma.Congruences  public
open import Legacy.Base.Structures.Sigma.Homs         public
open import Legacy.Base.Structures.Sigma.Isos         public
```