Setoid.Congruences.Certificates

Congruence certificates

This is the Setoid.Congruences.Certificates module of the Agda Universal Algebra Library.

Machine-checked import of externally computed congruence-lattice facts: the certificate schema (normal-form parent vectors and Freese traces) and the search-free checkers that turn a certificate into a theorem.

{-# OPTIONS --without-K --exact-split --safe #-}

module Setoid.Congruences.Certificates where

open import Setoid.Congruences.Certificates.Schema      public
open import Setoid.Congruences.Certificates.Congruence  public
open import Setoid.Congruences.Certificates.Lattice     public