category theory

# Contents

## Idea

The 1lab is an online reference maintained by Amélia Liao primarily for category theory done in univalent cubical type theory implemented in Agda.

Web:

proof assistants:

based on plain type theory/set theory:

based on cubical type theory:

based on modal type theory:

projects for formalization of mathematics with proof assistants:

Other proof assistants

Historical projects that died out:

Last revised on February 2, 2023 at 19:49:13. See the history of this page for a list of all contributions to it.