---
layout: default
file: "src/FLRP/Closure.lagda.md"
title: "FLRP.Closure module (The Agda Universal Algebra Library)"
date: "2026-07-24"
author: "the agda-algebras development team"
---

This is the [FLRP.Closure][] module of the [Agda Universal Algebra Library][].

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

module FLRP.Closure where

open import FLRP.Closure.Basic public
open import FLRP.Closure.Product public
open import FLRP.Closure.OrdinalSum public
```