Skip to content

The Agda Universal Algebra Library

Sigma

ualib/agda-algebras

Legacy.Base.Structures.Sigma¶

Sigma Types for General Mathematical Structures ¶

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


{-# 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