6 open source projects by UniMath

This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.

Voevodsky's original development of the univalent foundations of mathematics in Coq

The mathematical study of type theories, in univalent foundations

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

No description, website, or topics provided.

Univalent mathematics in Agda