Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP

My old Agda code for Homotopy Type Theory. See HoTT/HoTT-Agda for the new one.

branch: master

Fetching latest commit…

Octocat-spinner-32-eaf2f5

Cannot retrieve the latest commit at this time

Octocat-spinner-32 Map
Octocat-spinner-32 Path
Octocat-spinner-32 Space
Octocat-spinner-32 Univalence
Octocat-spinner-32 .gitignore
Octocat-spinner-32 LICENSE.md
Octocat-spinner-32 Path.agda
Octocat-spinner-32 Prelude.agda
Octocat-spinner-32 README.agda
Octocat-spinner-32 README.md
Octocat-spinner-32 Univalence.agda
README.md

Introduction

This repository hosts my Agda code for homotopy type theory. Homotopy type theory is a young theory seeking the connections between (abstract) homotopy theory, type theory and category theory. For more information about this theory I recommend this blog.

Copyright

See LICENSE.md for more information. Please consider using open-source licenses in your derived work to maximize the availability and usefulness.

Documentation

For an overview of the code, please take a look at README.agda.

Something went wrong with that request. Please try again.