+-- {: .rightHandSide} +-- {: .toc .clickDown tabindex="0"} ### Context #### Type theory +-- {: .hide} [[!include type theory - contents]] =-- #### Category theory +-- {: .hide} [[!include category theory - contents]] =-- =-- =-- \tableofcontents ## Idea The **1lab** is an online reference maintained by [[Amélia Liao]] primarily for [[category theory]] done in [[univalent type theory|univalent]] [[cubical type theory]] implemented in [[cubical Agda]]. Web: * [1lab website](https://1lab.dev/) * [Github page for the 1lab](https://github.com/plt-amy/1lab) The name "1lab" is apparently a reference to (the name of) the "[[nLab|$n$Lab]]", with the specification $n = 1$ meant to highlight the focus on [[univalent category|type-theoretic]] [[1-categories]] (as opposed to [[higher category theory|higher categories]], whose type-theoretic formulation remains underdeveloped, generally). ## Related entries [[!include proof assistants and formalization projects -- list]]