Formalizing universal algebra with dependent and inductive types¶

JMM Special Session on Algebras and Algorithms

William DeMeo

Denver, Colorado, Wed 15 Jan 2020

(For the latest updates, please visit ualib.org.)

  • 1. Preface
    • 1.1. Vision
    • 1.2. Objectives
    • 1.3. Intended audience
    • 1.4. Installing the library
    • 1.5. Acknowledgments
    • 1.6. References
  • 2. Datatypes for Algebras
    • 2.1. Preliminaries
    • 2.2. Signatures
    • 2.3. Operations
    • 2.4. Algebras
    • 2.5. Homomorphisms
  • 3. Datatypes for Terms
    • 3.1. Terms
    • 3.2. The term algebra
    • 3.3. The universal property
  • 4. Datatypes for Subuniverses and Subalgebras
    • 4.1. Subuniverses
    • 4.2. Subalgebras

Appendix¶

  • Note on axiom K
  • Writing definitions interactively
  • REFERENCES
Please email comments, suggestions, and corrections to williamdemeo@gmail.com

Logo

agda-ualib

Navigation

  • 1. Preface
  • 2. Datatypes for Algebras
  • 3. Datatypes for Terms
  • 4. Datatypes for Subuniverses and Subalgebras
  • Note on axiom K
  • Writing definitions interactively
  • REFERENCES

  • PDF version
  • ualib.org

Related Topics

  • Documentation overview
    • Next: 1. Preface

Quick search

Donate/support

Donate

©2019, William DeMeo. | Powered by Sphinx 2.3.1 & Alabaster 0.7.12