Homotopy type theory
Verilog
Switch branches/tags
Nothing to show
Pull request Compare This branch is 25 commits ahead, 2548 commits behind mikeshulman:master.
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
Coq
OberwolfachTutorial
.gitignore
README

README

This directory contains material in the context of 
homotopy type theory

  http://ncatlab.org/nlab/show/homotopy+type+theory ,

the internal language of infinity-toposes

  http://ncatlab.org/nlab/show/(infinity,1)-topos .

The directory "Hott/Coq" contains Coq code

  http://ncatlab.org/nlab/show/Coq

for Martin-Löf type theory

  http://ncatlab.org/nlab/Martin-Löf+type+theory .

that sets up the basic notions of homotopy type theory.

The subdirectory "HoTT/Coq/HIT" contains code that sets up
higher inductive types

  http://ncatlab.org/nlab/show/higher+inductive+types.

The subdirectory "HoTT/Coq/Cohesion" contains code that
sets up the internal language of cohesive infinity-toposes

  http://ncatlab.org/nlab/show/cohesive+(infinity,1)-topos .

You can fork this repository to your own and then be automatically
kept up to date on new developments. You can also contribute back into
it by sending a pull request.

The Coq files contain fancy UTF-8 characters. To input these you have
to set up an appropriate input method, see

  http://coq.inria.fr/cocorico/TeXInputMethodForUnicodeNotations

for help on doing so with Emacs and CoqIDE.