Skip to content

Logical manifestations of topological concepts, and other things. This version adopts the univalent point of view.

License

Notifications You must be signed in to change notification settings

ayberkt/TypeTopology

 
 

Repository files navigation

Various new theorems in constructive univalent mathematics written in Agda

This development was started by Martin Escardo in 2010, and transferred to github Monday 5th February 2018. A few files are authored by collaborators or external contributors, with names added at the top.

If you contribute, please add your full (legal or adopted) name and date at the place of contribution.

An html rendering of the Agda code is hosted at Martin Escardo's institutional web page.

How to cite

You can use the following BibTeX citation to cite TypeTopology:

@misc{type-topology,
  title    = {{TypeTopology}},
  author   = {Escard\'{o}, Mart\'{i}n H. and {contributors}},
  url      = {https://github.com/martinescardo/TypeTopology},
  note     = {{Agda} development},
}

Current contributors in alphabetical order of given name

  • Andrew Sneap
  • Ayberk Tosun
  • Chuangjie Xu
  • Cory Knapp
  • Ettore Aldrovandi
  • Jon Sterling
  • Keri D'Angelo
  • Marc Bezem *
  • Martin Escardo
  • Ohad Kammar
  • Paulo Oliva
  • Peter Dybjer *
  • Thierry Coquand *
  • Todd Waugh Ambridge
  • Tom de Jong

(*) These authors didn't write any single line of Agda code here, but they contributed to constructions, theorems and proofs via the hands of Martin Escardo.

About

Logical manifestations of topological concepts, and other things. This version adopts the univalent point of view.

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Agda 93.1%
  • TeX 6.8%
  • Other 0.1%