Mini-HoTT  

Mini-HoTT is a basic Agda library which contains basic definitions and results in Univalent type theory. There is no guarantee whatsoever of any kind. At the moment, this library suffers of many changes without any warning.

• Website documentation: https://mini-hott.readthedocs.io/

Quick start

Installation

The only prerequisite is to have installed the latest version of Agda and a text editor with Agda support, e.g., Emacs or Atom. Then, you can install the library as usual after cloning the sources by running the following command.

$ git clone http://github.com/jonaprieto/mini-hott

For newcomers, the easiest way to install a library is using agda-pkg You can run the following commands to install it:

$ pip3 install agda-pkg
$ apkg init
$ apkg install --github jonaprieto/mini-hott

After installing the sources, just include in your code at the top the following line:

open import MiniHoTT

Table of Contents

• Quick start
  • Code conventions
  • Proof relevancy
• Everything in Mini HoTT
• Types
  • Empty type
  • Unit type
  • Two-point type
  • Natural numbers
  • ∑-types
  • Π-types
  • Products
  • Coproducts
  • Finite sets
  • Equalities
• Other custom types
  • Implications
  • Bi-implications
  • Decidable type
  • Heterogeneous equality
• Basic functions
  • Path functions
  • Identity functions
  • Constant functions
  • Reasoning with negation
  • Composition
  • Application
  • Natural number operations
  • Coproduct manipulation
  • Curryfication
  • Uncurryfication
  • Finite iteration of a function
  • Coproducts functions
  • Equational reasoning
• Decidable equality
• Algebra of paths
• Properties on the groupoid
• Algebra of Pathovers
• Transport
  • Coercion
  • Pathovers
  • Compositions of Pathovers
  • Transport along pathovers
• Transport Lemmas
• Action on dependent paths
• Coproduct identities
• When ∑ and ∏ commute
• Fibre type
• Transport with fibers
• Homotopies
  • Homotopy types
  • Homotopy is an equivalence relation
• Composition with homotopies
• Naturality
• Equivalences
  • Contractible maps
  • Equivalence Type
• Quasiinverses
• Quasiinverse Lemmas
  • Equivalence composition
• Biinverses
• Half-adjoints
• Equivalence reasoning
• Basic Equivalences
• Equivalence with Pi type
• Equivalences preserved by Sigma types
• Sigma equivalences
• Voevodsky’s Univalence Axiom
• Function extensionality
• Univalence lemmas
• Univalence Lemma for Identity equivalence
• Transport and Univalence
• Function extensionality transport case
• Dependent function extensionality transport case
• Hlevel types
  • Contractible types
  • Propositions
  • Sets
  • Groupoids
• Hedberg theorem
• HLevel Lemmas
• Types of Morphisms
  • Surjections
  • Embeddings
  • Injections
  • Bijections
• Rewriting
• Set truncations
• Groupoid truncations
• Product identities
• Suspensions
• Intervals
• Propositional truncation
  • Truncation Lemmas
• Quotient type
• Circles
• Fundamental group
• Monoids
• Relation
• Integers
• Groups
• The type of natural numbers
• Connectedness
  • 0-connected type
• The Axiom Of Choice

Contributors

Collaborations are always welcomed. At the moment, me, Jonathan Prieto-Cubides, I’m using the library to type-check my proofs for my research project at the University of Bergen.

• Jonathan Prieto-Cubides

People involved in making this library better, although not directly involved are:

• Håkon Robbestad Gylterud
• Marc Bezem
• People from the Agda mailing list

References

• Theory
  • The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. 2013.
  • The Homotopy Type Theory and Univalent Foundations CAS project. Symmetry Book. 2020.
  • Escardo, M. Introduction to Univalent Foundations of Mathematics with Agda. 2019.
  • Rikje, E. Introduction to Homotopy Type Theory. 2019.
• Implementation:
  • Agda-HoTT
  • Agda-premises
  • HoTT-Agda
  • Agda-Base